Theorems · Definition · commutative algebra

Ideal.normalizedFactorsEquivSpanNormalizedFactors

{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})}

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

5 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainIsPrincipalIdealRingNormalizationMonoid