mathlib3

ebbb991a - feat(ring_theory/principal_ideal_domain): add some corollaries about is_coprime (#10601)