Theorems · Theorem · commutative algebra

Ideal.count_span_normalizedFactors_eq_of_normUnit

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NormalizationMonoid R] [inst_4 : DecidableEq R] {r X : R},
  r ≠ 0 →
    normUnit X = 1 →
      Prime X →
        Multiset.count (Ideal.span {X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})) =
          Multiset.count X (UniqueFactorizationMonoid.normalizedFactors r)

Defined in: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Cited by: 2 results in Mathlib
Foundations: Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing IsDomain IsPrincipalIdealRing NormalizationMonoid DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites17

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

Setstatement · cited by 53,352
CommRingstatement and proof · cited by 17,173
Idealstatement · cited by 4,748
mul_oneproof · cited by 3,885
Unitsstatement · cited by 2,804
IsDomainstatement and proof · cited by 2,196
Units.valproof · cited by 1,966
Ideal.spanstatement and proof · cited by 948
Multiset.countstatement and proof · cited by 302
Primestatement and proof · cited by 277
NormalizationMonoidstatement and proof · cited by 165
UniqueFactorizationMonoid.normalizedFactorsstatement and proof · cited by 151

Cited by2

Results whose statement or proof uses this declaration.

PowerSeries.intValuation_eq_of_coeproof · cited by 2
count_span_normalizedFactors_eq_of_normUnitproof · cited by 0