Theorem count_span_normalizedFactors_eq_of_normUnit

Modification history

2024-05-30 15:41
Mathlib/RingTheory/DedekindDomain/Ideal.lean
feat(RingTheory/DedekindDomain/Ideal): add two lemmas about the multiplicity of normalized factors (#13065) …
Added count_span_normalizedFactors_eq_of_normUnitView on Github →