I is an ID iff I is prime (#3951)

Commit

5 years ago

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`

References

#4925 - Make prime-avoidance branch build

Author

kbuzzard

Parents

2b6924d5

mathlib3 2d9ab611 - feat(ring_theory/ideal/basic): R/I is an ID iff I is prime (#3951)

mathlib3
2d9ab611 - feat(ring_theory/ideal/basic): R/I is an ID iff I is prime (#3951)