go_zero

Mathlib.Data.Nat.Digits.Defs

URI: https://scilib.ai/kg/mathlib#Nat.digitsAux.go_zero

← MathLib Explorer

English

If the fuel parameter is 0, digitsAux.go returns the empty list.

Русский

Если порог (fuel) равен нулю, digitsAux.go возвращает пустой список.

LaTeX

$$$\text{digitsAux.go}(b,h,0,fuel)=\emptyset$$$

Lean4

theorem go_zero (b : ℕ) (h : 2 ≤ b) (fuel : ℕ) (hfuel : (if 0 = 0 then 0 else n + 1) < fuel) :
    digitsAux.go b h 0 fuel hfuel = [] := by rw [digitsAux.go]

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

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

Разделы

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

Аффилиация

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