zero_right

Mathlib.Tactic.NormNum.LegendreSymbol

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.jacobiSymNat.zero_right

Lean4

/-- Base cases: `b = 0`, `b = 1`, `a = 0`, `a = 1`. -/
theorem zero_right (a : ℕ) : jacobiSymNat a 0 = 1 := by rw [jacobiSymNat, jacobiSym.zero_right]

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

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

Разделы

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

Аффилиация

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