sq_one

Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

URI: https://scilib.ai/kg/mathlib#jacobiSym.sq_one

← MathLib Explorer

English

If a and b are coprime, then J(a | b)^2 = 1.

Русский

Если a и b взаимно просты, то J(a | b)^2 = 1.

LaTeX

$$$ J(a | b)^2 = 1 $$$

Lean4

/-- The square of `J(a | b)` is `1` when `a` and `b` are coprime. -/
theorem sq_one {a : ℤ} {b : ℕ} (h : a.gcd b = 1) : J(a | b) ^ 2 = 1 := by
  rcases eq_one_or_neg_one h with h₁ | h₁ <;> rw [h₁] <;> rfl

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

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

Разделы

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

Аффилиация

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