neg_one_pow — Mathlib

English

For odd m,n, qrSign m n equals (-1)^{(m/2) ⋅ (n/2)}.

Русский

Для нечётных m и n, qrSign m n равно (-1)^{(m/2)·(n/2)}.

LaTeX

$$$ \forall m,n, \text{ if } m,n \text{ odd } \Rightarrow qrSign m n = (-1)^{(m/2)(n/2)} $$$

Lean4

/-- We can express `qrSign m n` as a power of `-1` when `m` and `n` are odd. -/
theorem neg_one_pow {m n : ℕ} (hm : Odd m) (hn : Odd n) : qrSign m n = (-1) ^ (m / 2 * (n / 2)) :=
  by
  rw [qrSign, pow_mul, ← χ₄_eq_neg_one_pow (odd_iff.mp hm)]
  rcases odd_mod_four_iff.mp (odd_iff.mp hm) with h | h
  · rw [χ₄_nat_one_mod_four h, jacobiSym.one_left, one_pow]
  · rw [χ₄_nat_three_mod_four h, ← χ₄_eq_neg_one_pow (odd_iff.mp hn), jacobiSym.at_neg_one hn]

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