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.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

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.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

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

{ "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

{ "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

/-
TODO: it's not clear to me (jmc) whether the following items can be easily included,
      maybe they depend on theory of etale algebras, just like the items further below

  ∀ (f : polynomial R) (a₀ : R) (h₁ : f.eval a₀ ∈ maximal_ideal R)
    (h₂ : f.derivative.eval a₀ ∉ maximal_ideal R),
    ∃ a : R, f.is_root a ∧ (a - a₀ ∈ maximal_ideal R),
  ∀ (f : polynomial R) (a₀ : residue_field R) (h₁ : aeval a₀ f = 0)
    (h₂ : aeval a₀ f.derivative ≠ 0),
    ∃ a : R, f.is_root a ∧ (residue R a = a₀),

jcommelin

AddCommGroup.Ab.category_theory.limits.has_colimits_of_size
AddCommGroup.colimit_comparison
AddCommGroup.direct_sum_bicone
AddCommGroup.direct_sum_punit_iso
AddCommGroup.hom_product_comparison
AddCommGroup.is_bilimit_direct_sum_bicone
AddCommGroup.is_iso_hom_product_comparison
AddCommGroup.is_limit_pi_fan
AddCommGroup.pi_fan
AddCommGroup.pi_lift

jcommelin

import tactic.find_unused
import challenge

open tactic

meta def file_list : list (option string) :=
["backup/delta_functor.lean", "backup/extr.lean",
"backup/extr_backup.lean", "backup/multilinear.lean",
"backup/prepresentation.lean", "backup/sheafification_mono.lean",
"scripts/lean_version.lean", "scripts/lint_project.lean",