Theorems · Theorem · number theory
Nat.chineseRemainder_modEq_unique
∀ {m n : ℕ} (co : n.Coprime m) {a b z : ℕ},
z ≡ a [MOD n] → z ≡ b [MOD m] → z ≡ ↑(Nat.chineseRemainder co a b) [MOD n * m]- Defined in
- Mathlib.Data.Nat.ModEq
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 51 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Subtype.propproof · cited by 505
- Nat.ModEqstatement and proof · cited by 225
- Nat.ModEq.symmproof · cited by 29
- Nat.ModEq.transproof · cited by 21
- Nat.chineseRemainderstatement and proof · cited by 7
- Nat.Coprime.lcm_eq_mulproof · cited by 5
- Nat.mod_lcmproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Nat.chineseRemainderOfList_modEq_uniqueproof · cited by 1