Commit 2020-08-26 17:53 2d9ab611
View on Github →feat(ring_theory/ideal/basic): R/I is an ID iff I is prime (#3951)
is_integral_domain_iff_prime (I : ideal α) : is_integral_domain I.quotient ↔ I.is_prime
feat(ring_theory/ideal/basic): R/I is an ID iff I is prime (#3951)
is_integral_domain_iff_prime (I : ideal α) : is_integral_domain I.quotient ↔ I.is_prime