jcommelin

{ "nodes" : 

[{ "name" : "partial_order",
"topic" : "core",
"file" : "core/init/algebra/order.lean",
"line" : 26 }
, { "name" : "has_ssubset",
"topic" : "core",
"file" : "core/init/core.lean",
"line" : 340 }

jcommelin

{ "nodes" : 

[{ "name" : "partial_order",
"topic" : "core",
"file" : "core/init/algebra/order.lean",
"line" : 26 }
, { "name" : "has_coe_t_aux",
"topic" : "core",
"file" : "core/init/coe.lean",
"line" : 123 }

jcommelin

freek:
   1:
      - title  : The Irrationality of the Square Root of 2
      - decl   : irr_sqrt_two
      - author : mathlib
   2:
      - title  : Fundamental Theorem of Algebra
      - decl   : exists_root
      - author : Chris Hughes
   3:

jcommelin

import data.list.basic

/-
Om het spel te spelen moet u helemaal naar beneden scrollen.
Daar vindt u meer uitleg.

De volgende code is een gedeeltelijke vertaling van code
die geschreven is door Mario Carneiro.
-/

jcommelin

import data.rat.basic
import tactic.linarith
import tactic.omega
import tactic.wlog

local attribute [instance] classical.prop_decidable
local attribute [simp] nat.pow_two

section for_mathlib

jcommelin

import data.finsupp order.complete_lattice algebra.ordered_group data.mv_polynomial
import algebra.order_functions

namespace multiset
variables {α : Type*} [decidable_eq α]

def to_finsupp (s : multiset α) : α →₀ ℕ :=
{ support := s.to_finset,
  to_fun := λ a, s.count a,
  mem_support_to_fun := λ a,

jcommelin

/-
Copyright (c) 2019 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin, Kenny Lau
-/

import data.finsupp order.complete_lattice algebra.ordered_group data.mv_polynomial

namespace eq
variables {α : Type*} {a b : α}

jcommelin

import data.real.basic

structure complex :=
(re : ℝ)
(im : ℝ)

-- type ℝ as \R
-- type ℂ as \com or \Com

notation `ℂ` := complex

jcommelin

-- Big thanks to Simon Hudon for dictating this file to me
-- and explaining what's going on!

import category_theory.concrete_category

namespace string

def camel_case (s : string) : string :=
(join $ split (λ c, c = '_') s) ++ "'"
  -- TODO make first char uppercase of each elem in list

jcommelin

import category_theory.examples.topological_spaces
import order.lattice order.galois_connection
import category_theory.tactics.obviously

universes u v

open category_theory
open category_theory.examples

namespace open_set