symm — Mathlib

English

qrSign is symmetric in both arguments when both are odd: qrSign(m, n) = qrSign(n, m) for odd m and odd n.

Русский

qrSign симметричен по обоим аргументам, если оба аргумента нечётные: qrSign(m, n) = qrSign(n, m) при m и n нечётных.

LaTeX

$$$\forall m,n \; (\text{Odd}(m) \land \ text{Odd}(n)) \implies qrSign(m, n) = qrSign(n, m)$$$

Lean4

/-- `qrSign` is symmetric when both arguments are odd. -/
protected theorem symm {m n : ℕ} (hm : Odd m) (hn : Odd n) : qrSign m n = qrSign n m := by
  rw [neg_one_pow hm hn, neg_one_pow hn hm, mul_comm (m / 2)]

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