Theorems · Theorem · commutative algebra

Ideal.eq_prime_pow_mul_coprime

∀ {T : Type u_4} [inst : CommRing T] [inst_1 : IsDedekindDomain T] {I : Ideal T},
  I ≠ ⊥ →
    ∀ (P : Ideal T) [hpm : P.IsMaximal],
      ∃ Q, P ⊔ Q = ⊤ ∧ I = P ^ Multiset.count P (UniqueFactorizationMonoid.normalizedFactors I) * Q

Defined in

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainIdeal.IsMaximal