instIsPrincipalIdealRing — Mathlib

English

For any division ring K, every ideal of the dual-number ring K[ε] is principal; in particular the only nontrivial proper ideal is (ε).

Русский

Для любого делительного кольца K каждый идеал кольца двойственных чисел K[ε] является главной; в частности, единственный ненулевой и неполный идеал — это (ε).

LaTeX

$$$\text{IsPrincipalIdealRing}(K[\varepsilon])$$$

Lean4

instance [DivisionRing K] : IsPrincipalIdealRing K[ε] where
  principal
    I := by
    rcases ideal_trichotomy I with rfl | rfl | rfl
    · exact bot_isPrincipal
    · exact ⟨_, rfl⟩
    · exact top_isPrincipal

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