Theorems · Definition · commutative algebra
ZMod.equivPi
(n : ℕ) → n ≠ 0 → ZMod n ≃+* ((p : ↥n.primeFactors) → ZMod (↑p ^ n.factorization ↑p))
The Chinese remainder theorem, version for ZMod n.
- Defined in
- Mathlib.Data.ZMod.QuotientRing
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Finsetstatement · cited by 13,712
- Finsuppstatement · cited by 5,255
- RingEquivstatement · cited by 1,147
- ZModstatement · cited by 1,024
- Nat.factorizationstatement and proof · cited by 215
- Nat.primeFactorsstatement and proof · cited by 129
- RingEquiv.transproof · cited by 54
- ZMod.ringEquivCongrproof · cited by 11
- Nat.prod_primeFactors_coe_pow_factorizationproof · cited by 2
- Nat.pairwise_coprime_pow_primeFactors_factorizationproof · cited by 1
- ZMod.prodEquivPiproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.