Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-27 14:35 03172b6b

View on Github →

chore(ring_theory/dedekind_domain/ideal): generalize a lemma (#15104)

Estimated changes

Modified src/ring_theory/dedekind_domain/ideal.lean

deleted theorem normalized_factors_prod

Modified src/ring_theory/unique_factorization_domain.lean

added theorem unique_factorization_monoid.normalized_factors_prod_of_prime