Theorem Ideal.inf_eq_mul_of_coprime
Modification history
2024-06-06 14:15
Mathlib/RingTheory/DedekindDomain/Ideal.lean
fix: remove Dedekind domain assumption from Ideal.inf_eq_mul_of_coprime (#13308)
Deleted Ideal.inf_eq_mul_of_coprimeView on Github →