Adjoin_root `f` is a domain for prime `f`

Stream: Is there code for X?

[Paul Lezeau]

Do we have any result saying that adjoin_root f is a domain when f is prime and R is a domain?

[Paul Lezeau]

I couldn't find anything in ring_theory.adjoin_root or ring_theory.is_adjoin_root, where such a result should be

[Junyan Xu]

We have docs#ideal.quotient.is_domain_iff_prime and docs#ideal.span_singleton_prime, and docs#adjoin_root is just quotient by the ideal generated by a singleton.

[Paul Lezeau]

Yeah that's what I ended up using ! I was just checking in case I had missed it - I was quite surprised we didn't already have that somewhere

[Junyan Xu]

This combination comes up in src#weierstrass_curve.coordinate_ring.is_domain as well. So probably a good idea to add it!