Theorems · Theorem · commutative algebra

Ideal.hasFiniteMulSupport

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R},
  I ≠ 0 → Function.HasFiniteMulSupport fun v => v.maxPowDividing I

For every nonzero ideal I of v, there are finitely many maximal ideals v such that v^(val_v(I)) is not the unit ideal.

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomain