Theorems · Theorem · commutative algebra

FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top

∀ {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Submonoid R}
  [IsLocalization S A] (I : (FractionalIdeal S A)ˣ) {v : A},
  v ∈ ↑I⁻¹ → Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v)) = ⊤ → (↑↑I).IsPrincipal

Defined in

Mathlib.RingTheory.DedekindDomain.PID

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsLocalization