Theorems · Theorem · commutative algebra

Ideal.finite_mulSupport

Deprecated since 2026-03-03Use Ideal.hasFiniteMulSupport instead.

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

Alias of Ideal.hasFiniteMulSupport. 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

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomain