English
Let p be an odd prime and a an odd natural number with a not divisible by p. Then the parity of the set {x ∈ Ico 1 (p/2).succ | p/2 < (a x.cast : ZMod p).val} equals the parity of the sum ∑ x ∈ Ico 1 (p/2).succ, x*a/p modulo 2.
Русский
Пусть p — нечетное простое число, и a — нечетное натуральное число, не делящееся на p. Тогда чётность множества {x ∈ Ico 1 (p/2).succ | p/2 < (a x.cast : ZMod p).val} равна чётности суммы ∑ x ∈ Ico 1 (p/2).succ, x*a/p по модулю 2.
LaTeX
$$$#\{x ∈ Ico 1 (p / 2).succ \mid p / 2 < (a * x.cast : ZMod p).val\} \equiv \sum_{x ∈ Ico 1 (p / 2).succ} x * a / p \,[MOD\ 2]$$$
Lean4
theorem eisenstein_lemma_aux (p : ℕ) [Fact p.Prime] [Fact (p % 2 = 1)] {a : ℕ} (ha2 : a % 2 = 1)
(hap : (a : ZMod p) ≠ 0) :
#({x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val}) ≡ ∑ x ∈ Ico 1 (p / 2).succ, x * a / p [MOD 2] :=
have ha2 : (a : ZMod 2) = (1 : ℕ) := (natCast_eq_natCast_iff _ _ _).2 ha2
(natCast_eq_natCast_iff _ _ 2).1 <|
sub_eq_zero.1 <| by
simpa [add_left_comm, sub_eq_add_neg, ← mul_sum, mul_comm, ha2, Nat.cast_sum, add_neg_eq_iff_eq_add.symm,
add_assoc] using Eq.symm (eisenstein_lemma_aux₁ p hap)
