sq_eq_one

Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

URI: https://scilib.ai/kg/mathlib#qrSign.sq_eq_one

← MathLib Explorer

English

When m and n are odd, qrSign m n^2 equals 1.

Русский

Когда m и n — нечётные, qrSign m n^2 равно 1.

LaTeX

$$$ (qrSign m n)^2 = 1 \quad \text{(m,n \text{ odd})} $$$

Lean4

/-- When `m` and `n` are odd, then the square of `qrSign m n` is `1`. -/
theorem sq_eq_one {m n : ℕ} (hm : Odd m) (hn : Odd n) : qrSign m n ^ 2 = 1 := by
  rw [neg_one_pow hm hn, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]

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

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

Разделы

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

Аффилиация

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