kbuzzard

import Mathlib.Tactic

/-!

# The integers

In this file we assume all standard facts about the naturals, and then build
the integers from scratch.

The strategy is to observe that every integer can be written as `a - b`

kbuzzard

universe u

class Zero (α : Type u) where
  zero : α

instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
  zero := 0

kbuzzard

import data.real.irrational
import tactic

open real

example : irrational (sqrt 2) :=
begin
  rintro ⟨q, hq⟩,
  have hqnum : 0 ≤ q.num,
  { rw rat.num_nonneg_iff_zero_le,

kbuzzard

-- See https://github.com/leanprover-community/mathlib4/blob/489f10454a7ae53fdc6a95d2ac237cbc20e69b36/Mathlib/Algebra/Order/Positive/Field.lean#L42-L46
-- for the actual mathlib problem, which is even slower

universe u

class Preorder (α : Type u) extends LE α, LT α where
  le_refl : ∀ a : α, a ≤ a
  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
  lt := λ a b => a ≤ b ∧ ¬ b ≤ a
  lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) := by intros; rfl

kbuzzard

-- see https://github.com/leanprover-community/mathlib4/pull/1099#discussion_r1051747996
import Mathlib.Mathport.Notation -- I don't understand this file well enough to remove it, but it's only notation

set_option autoImplicit false

universe u v

instance {ι : Type u} {α : ι → Type v} [∀ i, LE (α i)] : LE (∀ i, α i) where
  le x y := ∀ i, x i ≤ y i

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 :=