Commit 2024-06-06 14:15 1af205b4

View on Github →

fix: remove Dedekind domain assumption from Ideal.inf_eq_mul_of_coprime (#13308)

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

deleted theorem Ideal.inf_eq_mul_of_coprime

Modified Mathlib/RingTheory/Ideal/Norm.lean

modified theorem cardQuot_mul_of_coprime

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.inf_eq_mul_of_isCoprime

Modified Mathlib/RingTheory/Ideal/QuotientOperations.lean

added theorem Ideal.fst_comp_quotientMulEquivQuotientProd

added theorem Ideal.quotientMulEquivQuotientProd_fst

added theorem Ideal.quotientMulEquivQuotientProd_snd

added theorem Ideal.snd_comp_quotientMulEquivQuotientProd