Theorems · Theorem · commutative algebra

FractionalIdeal.count_well_defined

∀ {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] (v : IsDedekindDomain.HeightOneSpectrum R)
  {I : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 →
    ∀ {a : R} {J : Ideal R},
      I = FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * ↑J →
        FractionalIdeal.count K v I =
          ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)

val_v(I) does not depend on the choice of a and J used to represent I.

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsFractionRingIsDedekindDomain