English
Two sums counting lattice points in two triangles formed by the diagonal of a rectangle add to the total lattice count in the rectangle.
Русский
Две суммы, считающие точки с целыми координатами внутри двух треугольников, образованных диагональю прямоугольника, дают общее число точек в прямоугольнике.
LaTeX
$$$\sum_{a ∈ Ico 1 (p/2).succ} a \; q/p + \sum_{a ∈ Ico 1 (q/2).succ} a \; p/q = p/2 \cdot (q/2)$$$
Lean4
/-- The Jacobi symbol takes only the values `0`, `1` and `-1`. -/
theorem trichotomy (a : ℤ) (b : ℕ) : J(a | b) = 0 ∨ J(a | b) = 1 ∨ J(a | b) = -1 :=
((MonoidHom.mrange (@SignType.castHom ℤ _ _).toMonoidHom).copy {0, 1, -1} <|
by
rw [Set.pair_comm]
exact (SignType.range_eq SignType.castHom).symm).list_prod_mem
(by
intro _ ha'
rcases List.mem_pmap.mp ha' with ⟨p, hp, rfl⟩
haveI : Fact p.Prime := ⟨prime_of_mem_primeFactorsList hp⟩
exact quadraticChar_isQuadratic (ZMod p) a)
