zero_left

Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

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

← MathLib Explorer

English

J(0|b) = 0 for b > 1.

Русский

J(0|b) = 0 при b > 1.

LaTeX

$$$J(0\mid b) = 0 \quad\text{если } 1 < b$$$

Lean4

/-- The symbol `J(0 | b)` vanishes when `b > 1`. -/
theorem zero_left {b : ℕ} (hb : 1 < b) : J(0 | b) = 0 :=
  (@eq_zero_iff_not_coprime 0 b ⟨ne_zero_of_lt hb⟩).mpr <| by rw [Int.gcd_zero_left, Int.natAbs_natCast]; exact hb.ne'

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

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

Разделы

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

Аффилиация

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