Commit 2023-10-10 17:21 201c8eea

View on Github →

feat: Chinese remainder for ZMod. (#7599)

Estimated changes

Modified Mathlib/Data/ZMod/Quotient.lean

added def ZMod.prodEquivPi

Modified Mathlib/RingTheory/Coprime/Basic.lean

added theorem IsCoprime.intCast

Modified Mathlib/RingTheory/Coprime/Lemmas.lean

added theorem Nat.Coprime.cast

Modified Mathlib/RingTheory/Ideal/Operations.lean

modified theorem Ideal.iInf_span_singleton

added theorem Ideal.iInf_span_singleton_natCast

Modified Mathlib/RingTheory/Ideal/Quotient.lean

Modified Mathlib/RingTheory/Ideal/QuotientOperations.lean