Theorems · Theorem · commutative algebra

FractionalIdeal.finprod_heightOneSpectrum_factorization_principal

∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 →
    ∀ (k : K),
      I = FractionalIdeal.spanSingleton (nonZeroDivisors R) k →
        ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R),
            ↑v.asIdeal ^
              (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors) -
                ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑(Classical.choose ⋯)})).factors)) =
          I

For a nonzero k = r/s ∈ K, the fractional ideal (k) is equal to the product ∏_v v^(val_v(r) - val_v(s)).

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsFractionRingIsDedekindDomain