English
An LTE-type relation holds for p = 2 in the form: emultiplicity 2 (x^n − y^n) + 1 equals emultiplicity 2 (x + y) plus emultiplicity 2 (x − y) plus emultiplicity 2 n, under suitable parity conditions (x odd, x ≡ y mod 4).
Русский
Для p = 2 выполняется LTE-отношение: v_2(x^n − y^n) + 1 = v_2(x + y) + v_2(x − y) + v_2(n) при подходящих паритетах (x нечетно, x ≡ y mod 4).
LaTeX
$$$\\forall x,y \\in \\mathbb{Z},\\ (hxy:\\ 4 \\mid x-y) \\land (hx:\\ 2 \\nmid x) \\Rightarrow \\forall n \\in \\mathbb{N},\\ \\mathrm{emultiplicity}_2(x^n - y^n) + 1 = \\mathrm{emultiplicity}_2(x + y) + \\mathrm{emultiplicity}_2(x - y) + \\mathrm{emultiplicity}_2(n)$$$
Lean4
/-- Niven's theorem, giving the possible angles for `θ` in the range `0 .. π`. -/
theorem niven_angle_eq (hθ : ∃ r : ℚ, θ = r * π) (hcos : ∃ q : ℚ, cos θ = q) (h_bnd : θ ∈ Set.Icc 0 π) :
θ ∈ ({0, π / 3, π / 2, π * (2 / 3), π} : Set ℝ) := by
rcases niven hθ hcos with h | h | h | h | h <;>
-- define `h₂` appropriately for each proof branch
[have h₂ := cos_pi;
have h₂ : cos (π * (2 / 3)) = -1 / 2 := by
have := cos_pi_sub (π / 3)
have := cos_pi_div_three
grind; ;
have h₂ := cos_pi_div_two; have h₂ := cos_pi_div_three; have h₂ := cos_zero] <;>
simp [injOn_cos h_bnd ⟨by positivity, by linarith [pi_nonneg]⟩ (h₂ ▸ h)]
