Theorem principal_ideal_domain.is_maximal_of_irreducible
Modification history
2020-06-22 07:22
src/ring_theory/principal_ideal_domain.lean
refactor(ring_theory/*): make PID class a predicate (#3114)
Deleted principal_ideal_domain.is_maximal_of_irreducibleView on Github →