Theorem unique_factorization_monoid.irreducible_of_factor
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.irreducible_of_factorView on Github →