Commit 2023-10-06 14:17 f47760be

View on Github →

chore: Refactor Chinese remainders (#7532)

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.isCoprime_biInf

added theorem Pi.ker_ringHom

Modified Mathlib/RingTheory/Ideal/Quotient.lean

deleted theorem Ideal.exists_sub_mem

deleted theorem Ideal.exists_sub_one_mem_and_mem

deleted theorem Ideal.fst_comp_quotientInfEquivQuotientProd

deleted theorem Ideal.quotientInfEquivQuotientProd_fst

deleted theorem Ideal.quotientInfEquivQuotientProd_snd

deleted def Ideal.quotientInfToPiQuotient

deleted theorem Ideal.quotientInfToPiQuotient_bijective

deleted theorem Ideal.snd_comp_quotientInfEquivQuotientProd

Modified Mathlib/RingTheory/Ideal/QuotientOperations.lean

added theorem Ideal.fst_comp_quotientInfEquivQuotientProd

added theorem Ideal.injective_lift_iff

added theorem Ideal.ker_Pi_Quotient_mk

modified theorem Ideal.mk_ker

added theorem Ideal.quotientInfEquivQuotientProd_fst

added theorem Ideal.quotientInfEquivQuotientProd_snd

added def Ideal.quotientInfToPiQuotient

added theorem Ideal.quotientInfToPiQuotient_inj

added theorem Ideal.quotientInfToPiQuotient_mk'

added theorem Ideal.quotientInfToPiQuotient_mk

added theorem Ideal.quotientInfToPiQuotient_surj

added theorem Ideal.snd_comp_quotientInfEquivQuotientProd