one_right

Mathlib.Tactic.NormNum.LegendreSymbol

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

Lean4

theorem one_right (a : ℕ) : jacobiSymNat a 1 = 1 := by rw [jacobiSymNat, jacobiSym.one_right]

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

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

Разделы

Аффилиация

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