ofDigits_one_cons — Mathlib

English

If the base is 1, then adding a head digit changes the value by that digit plus the rest evaluated at the same base.

Русский

Если основание равно 1, то добавление головы списка цифр изменяет значение на головной элемент плюс значение остатка по основанию 1.

LaTeX

$$$\\operatorname{ofDigits}(1, (h :: L)) = h + \\operatorname{ofDigits}(1,L).$$$

Lean4

@[simp]
theorem ofDigits_one_cons {α : Type*} [Semiring α] (h : ℕ) (L : List ℕ) :
    ofDigits (1 : α) (h :: L) = h + ofDigits 1 L := by simp [ofDigits]

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