Theorems · Theorem · number theory
ZMod.sum_mul_div_add_sum_mul_div_eq_mul
∀ (p q : ℕ) [hp : Fact (Nat.Prime p)], ↑q ≠ 0 → ∑ a ∈ Finset.Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Finset.Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2)
Each of the sums in this lemma is the cardinality of the set of integer points in each of the
two triangles formed by the diagonal of the rectangle (0, p/2) × (0, q/2). Adding them
gives the number of points in the rectangle.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fact
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites29
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Finsetproof · cited by 13,712
- Finset.sumstatement and proof · cited by 5,195
- Factstatement and proof · cited by 2,726
- Finset.cardproof · cited by 2,327
- Disjointproof · cited by 2,201
- MulZeroClass.mul_zeroproof · cited by 2,091
- le_antisymmproof · cited by 2,068
- Nat.Primestatement and proof · cited by 2,059
- SProd.sprodproof · cited by 1,750
- ZModstatement and proof · cited by 1,024
- Finset.filterproof · cited by 949
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.