Mathlib v3 is deprecated. Go to Mathlib v4

Theorem unique_factorization_monoid.normalized_factors_prod_of_prime

Modification history

2022-07-27 14:35
src/ring_theory/unique_factorization_domain.lean
chore(ring_theory/dedekind_domain/ideal): generalize a lemma (#15104)
Added unique_factorization_monoid.normalized_factors_prod_of_primeView on Github →