isMaximal_span_singleton_eps — Mathlib

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

Похожие утверждения