English
For the dual-number ring K[ε] over a division ring K, the ideal generated by ε is a maximal ideal; the ring is local with unique maximal ideal (ε).
Русский
В кольце двоечных чисел K[ε] над делительным кольцом K идеал, порожденный ε, является максимальным; кольцо локальное с единственным максимальным идеалом (ε).
LaTeX
$$$(\operatorname{span}\{\varepsilon\}).IsMaximal$$$
Lean4
theorem isMaximal_span_singleton_eps [DivisionRing K] : (Ideal.span {ε} : Ideal K[ε]).IsMaximal :=
by
refine ⟨?_, fun I hI ↦ ?_⟩
· simp [ne_eq, Ideal.eq_top_iff_one, Ideal.mem_span_singleton', TrivSqZeroExt.ext_iff]
·
rcases ideal_trichotomy I with rfl | rfl | rfl <;>
first
| simp at hI
| simp