of_finite_maximals — Mathlib

English

A Dedekind domain is principal if it has finitely many maximal ideals.

Русский

Дедекинд домен является главным, если число максимальных идеалов конечно.

LaTeX

$$$$\\text{IsPrincipalIdealRing}(R)$$$$

Lean4

/-- A Dedekind domain is a PID if its set of maximal ideals is finite. -/
theorem of_finite_maximals [IsDedekindDomain R] (h : {I : Ideal R | I.IsMaximal}.Finite) : IsPrincipalIdealRing R :=
  ⟨fun I => by
    obtain rfl | hI := eq_or_ne I ⊥
    · exact bot_isPrincipal
    apply Ideal.IsPrincipal.of_finite_maximals_of_isUnit h
    exact isUnit_of_mul_eq_one _ _ (FractionalIdeal.coe_ideal_mul_inv I hI)⟩

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