Theorems · Theorem · commutative algebra

FractionalIdeal.isPrincipal.of_finite_maximals_of_inv

∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Submonoid R}
  [IsLocalization S A],
  S ≤ nonZeroDivisors R → {I | I.IsMaximal}.Finite → ∀ (I I' : FractionalIdeal S A), I * I' = 1 → (↑I).IsPrincipal

An invertible fractional ideal of a commutative ring with finitely many maximal ideals is principal. https://math.stackexchange.com/a/95857

Defined in

Mathlib.RingTheory.DedekindDomain.PID

Cited by

1 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraIsLocalization