Theorem Ideal.inf_eq_mul_of_isCoprime

Modification history