neg_one_pow_div_two_of_three_mod_four

Mathlib.NumberTheory.LegendreSymbol.ZModChar

URI: https://scilib.ai/kg/mathlib#ZMod.neg_one_pow_div_two_of_three_mod_four

← MathLib Explorer

English

If n ≡ 3 (mod 4), then (−1)^{n/2} = −1.

Русский

Если n ≡ 3 (mod 4), то (−1)^{n/2} = −1.

LaTeX

$$$ (-1)^{\\frac{n}{2}} = -1 \\quad\\text{если } n \\equiv 3 \\pmod{4}. $$$

Lean4

/-- If `n % 4 = 3`, then `(-1)^(n/2) = -1`. -/
theorem neg_one_pow_div_two_of_three_mod_four {n : ℕ} (hn : n % 4 = 3) : (-1 : ℤ) ^ (n / 2) = -1 :=
  χ₄_eq_neg_one_pow (Nat.odd_of_mod_four_eq_three hn) ▸ χ₄_nat_three_mod_four hn

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru