Theorems · Definition · commutative algebra

FractionalIdeal.count

{R : Type u_1} →
  [inst : CommRing R] →
    (K : Type u_2) →
      [inst_1 : Field K] →
        [inst_2 : Algebra R K] →
          [IsFractionRing R K] →
            [IsDedekindDomain R] → IsDedekindDomain.HeightOneSpectrum R → FractionalIdeal (nonZeroDivisors R) K → ℤ

If I is a nonzero fractional ideal, a ∈ R, and J is an ideal of R such that I = a⁻¹J, then we define val_v(I) as (val_v(J) - val_v(a)). If I = 0, we set val_v(I) = 0.

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

25 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsFractionRingIsDedekindDomain