Mathlib Changelog
v4
Changelog
About
Github
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