Theorems · Theorem · commutative algebra

Ideal.hasFiniteMulSupport_coe

∀ {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 : Ideal R},
  I ≠ 0 →
    Function.HasFiniteMulSupport fun v => ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors)

For every nonzero ideal I of v, there are finitely many maximal ideals v such that v^(val_v(I)), regarded as a fractional ideal, is not (1).

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsFractionRingIsDedekindDomain