Theorems · Theorem · commutative algebra

irreducible_pow_sup

Deprecated since 2026-04-16Use Ideal.irreducible_pow_sup instead.

∀ {T : Type u_4} [inst : CommRing T] [inst_1 : IsDedekindDomain T] {I J : Ideal T},
  I ≠ ⊥ →
    Irreducible J → ∀ (n : ℕ), J ^ n ⊔ I = J ^ min (Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)) n

Alias of Ideal.irreducible_pow_sup.

Defined in: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Cited by: 0 results in Mathlib
Foundations: Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing IsDedekindDomain

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement · cited by 17,173
Idealstatement · cited by 4,748
Bot.botstatement · cited by 4,720
IsDedekindDomainstatement · cited by 668
Irreduciblestatement · cited by 496
Multiset.countstatement · cited by 302
UniqueFactorizationMonoid.normalizedFactorsstatement · cited by 151
Ideal.irreducible_pow_supproof · cited by 5

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.