Theorems · Theorem · commutative algebra

FractionalIdeal.constant_factor_ne_zero

∀ {R : Type u_6} [inst : CommRing R] {K : Type u_5} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 →
    ∀ {a : R} {J : Ideal R},
      I = FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * ↑J → Ideal.span {a} ≠ 0

If I is a nonzero fractional ideal, a ∈ R, and J is an ideal of R such that I = a⁻¹J, then a is nonzero.

Defined in

Mathlib.RingTheory.FractionalIdeal.Operations

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsFractionRing