Mathlib Changelog
v4
Changelog
About
Github
Theorem
Ideal.inf_eq_mul_of_isCoprime
Modification history
2024-06-06 14:15
Mathlib/RingTheory/Ideal/Operations.lean
fix: remove Dedekind domain assumption from Ideal.inf_eq_mul_of_coprime (#13308)
Added
Ideal.inf_eq_mul_of_isCoprime
View on Github →