Theorems · Definition · commutative algebra

normalizedFactorsEquivSpanNormalizedFactors

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

{R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [inst_2 : IsPrincipalIdealRing R] →
        [inst_3 : NormalizationMonoid R] →
          {r : R} →
            r ≠ 0 →
              ↑{d | d ∈ UniqueFactorizationMonoid.normalizedFactors r} ≃
                ↑{I | I ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})}

Alias of Ideal.normalizedFactorsEquivSpanNormalizedFactors. The bijection between the (normalized) prime factors of r and the (normalized) prime factors of span {r}

Defined in

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainIsPrincipalIdealRingNormalizationMonoid