Theorem unique_factorization_monoid.prime_of_factor
Modification history
2022-06-13 11:39
src/ring_theory/unique_factorization_domain.lean
chore(algebra/big_operators/associated,ring_theory/unique_factorization_domain): golf (#14671)
Modified unique_factorization_monoid.prime_of_factorView on Github →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.prime_of_factorView on Github →