kbuzzard

import tactic -- a bunch of tactics
import ring_theory.noetherian -- Noetherian rings
/-

# Using ideals in Lean

Throughout, `R` is a commutative ring.

## The type of ideals of a ring

kbuzzard

import geometry.euclidean.monge_point

-- let's look at the definition of the monge point of a simplex.

/-
We don't have an explicit definition of `euler_line`, but 
`affine_span ℝ {s.circumcenter, (univ : finset (fin (n + 1))).centroid ℝ s.points}` 
seems like a reasonable definition to go in `geometry.euclidean.monge_point` 
for the Euler line of a simplex. It should then be straightforward to prove that
 this really is a line (i.e., its `direction` has `finrank` equal to 1) if the 

kbuzzard

@is_scalar_tower 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
  (@smul_with_zero.to_has_scalar 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
     (@mul_zero_class.to_has_zero 𝕜
        (@mul_zero_one_class.to_mul_zero_class 𝕜
           (@monoid_with_zero.to_mul_zero_one_class 𝕜
              (@semiring.to_monoid_with_zero 𝕜
                 (@comm_semiring.to_semiring 𝕜
                    (@comm_ring.to_comm_semiring 𝕜
                       (@semi_normed_comm_ring.to_comm_ring 𝕜
                          (@normed_comm_ring.to_semi_normed_comm_ring 𝕜

kbuzzard

universe u

set_option old_structure_cmd true

/- 0,+ -/
class add_zero_class (M : Type u) extends has_zero M, has_add M :=
(zero_add : ∀ (a : M), 0 + a = a)
(add_zero : ∀ (a : M), a + 0 = a)

class add_semigroup (G : Type u) extends has_add G :=

kbuzzard

universe u

set_option old_structure_cmd true

/- 0,+ -/
class add_zero_class (M : Type u) extends has_zero M, has_add M :=
(zero_add : ∀ (a : M), 0 + a = a)
(add_zero : ∀ (a : M), a + 0 = a)

class add_semigroup (G : Type u) extends has_add G :=

kbuzzard

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @category_theory.induced_category.has_coe_to_sort ?x_4 ?x_5 ?x_6 ?x_7 ?x_8
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @wide_subquiver_has_coe_to_sort ?x_9 ?x_10
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @set.has_coe_to_sort ?x_11
failed is_def_eq

kbuzzard

import tactic
import data.real.basic
/-

# Some puzzles.

1) (easy logic). If `P`, `Q` and `R` are true-false statements, then show
that `(P → (Q → R)) → ((P → Q) → (P → R))` (where `→` means "implies")

2) (group theory) If `G` is a group such that `∀ g, g^2 = 1`

kbuzzard

⊢ @eq.{1} nat
    (@fintype.card.{u_2}
       (@alg_equiv.{u_1 u_2 u_2} F
          (@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
             (@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
             (@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
                (@intermediate_field.insert.insert.{u_2} E
                   (@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
                   (@intermediate_field.insert_empty.{u_2} E)
                   α)))

kbuzzard

key :
  @eq.{1} nat
    (@fintype.card.{u_2}
       (@alg_equiv.{u_1 u_2 u_2} F
          (@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
             (@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
             (@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
                (@intermediate_field.insert.insert.{u_2} E
                   (@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
                   (@intermediate_field.insert_empty.{u_2} E)

kbuzzard

import tactic

/-
Making group theory in a theorem prover
-/

namespace mygroup

-- A group needs multiplication, inverse, identity
class group (G : Type) extends has_mul G, has_inv G, has_one G :=