isPrincipalIdealRing — Mathlib

English

In a DivisionSemiring K, every ideal is principal.

Русский

В делящемся полуприняемом кольце K каждый идеал главен.

LaTeX

$$$[DivisionSemiring K]\Rightarrow IsPrincipalIdealRing K$$$

Lean4

instance (priority := 100) isPrincipalIdealRing (K : Type u) [DivisionSemiring K] : IsPrincipalIdealRing K where
  principal
    S := by
    rcases Ideal.eq_bot_or_top S with (rfl | rfl)
    · apply bot_isPrincipal
    · apply top_isPrincipal

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