English
Every Euclidean domain is a principal ideal domain.
Русский
Каждое евклидово кольцо — это главного идела кольцо.
LaTeX
$$$IsPrincipalIdealRing(R)$$$
Lean4
instance (priority := 100) to_principal_ideal_domain : IsPrincipalIdealRing R where
principal
S := by
classical
exact
⟨if h : {x : R | x ∈ S ∧ x ≠ 0}.Nonempty then
have wf : WellFounded (EuclideanDomain.r : R → R → Prop) := EuclideanDomain.r_wellFounded
have hmin :
WellFounded.min wf {x : R | x ∈ S ∧ x ≠ 0} h ∈ S ∧ WellFounded.min wf {x : R | x ∈ S ∧ x ≠ 0} h ≠ 0 :=
WellFounded.min_mem wf {x : R | x ∈ S ∧ x ≠ 0} h
⟨WellFounded.min wf {x : R | x ∈ S ∧ x ≠ 0} h,
Submodule.ext fun x =>
⟨fun hx =>
div_add_mod x (WellFounded.min wf {x : R | x ∈ S ∧ x ≠ 0} h) ▸
(Ideal.mem_span_singleton.2 <|
dvd_add (dvd_mul_right _ _) <|
by
have : x % WellFounded.min wf {x : R | x ∈ S ∧ x ≠ 0} h ∉ {x : R | x ∈ S ∧ x ≠ 0} := fun h₁ =>
WellFounded.not_lt_min wf _ h h₁ (mod_lt x hmin.2)
have : x % WellFounded.min wf {x : R | x ∈ S ∧ x ≠ 0} h = 0 :=
by
simp only [not_and_or, Set.mem_setOf_eq, not_ne_iff] at this
exact this.neg_resolve_left <| (mod_mem_iff hmin.1).2 hx
simp [*]),
fun hx =>
let ⟨y, hy⟩ := Ideal.mem_span_singleton.1 hx
hy.symm ▸ S.mul_mem_right _ hmin.1⟩⟩
else
⟨0,
Submodule.ext fun a =>
by
rw [← @Submodule.bot_coe R R _ _ _, span_eq, Submodule.mem_bot]
exact ⟨fun haS => by_contra fun ha0 => h ⟨a, ⟨haS, ha0⟩⟩, fun h₁ => h₁.symm ▸ S.zero_mem⟩⟩⟩
