zero_left

Mathlib.Tactic.NormNum.LegendreSymbol

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

Lean4

theorem zero_left (b : ℕ) (hb : Nat.beq (b / 2) 0 = false) : jacobiSymNat 0 b = 0 :=
  by
  rw [jacobiSymNat, Nat.cast_zero, jacobiSym.zero_left ?_]
  calc
    1 < 2 * 1 := by decide
    _ ≤ 2 * (b / 2) := (Nat.mul_le_mul_left _ (Nat.succ_le.mpr (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb))))
    _ ≤ b := Nat.mul_div_le b 2

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

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

Разделы

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

Аффилиация

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