Theorem unique_factorization_monoid.factors_prod
Modification history
2021-10-05 10:10
src/ring_theory/unique_factorization_domain.lean
refactor(algebra/gcd_monoid): don't require normalization (#9443) …
Added unique_factorization_monoid.factors_prodView on Github →