Theorem Ideal.inf_eq_mul_of_isCoprime

Modification history

2026-10-10 09:42
Mathlib/RingTheory/Ideal/Operations.lean
chore: delete deprecated declarations to March 2026 (#44240)
Deleted Ideal.inf_eq_mul_of_isCoprimeView on Github →
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_isCoprimeView on Github →