ofDigits_neg_one — Mathlib

English

For any list L of natural numbers, the value of ofDigits(-1) L equals the alternating sum of the digits mapped to integers.

Русский

Для любого списка L из натуральных чисел, значение ofDigits(-1) L равно чередующейся сумме цифр, отображённых в целые числа.

LaTeX

$$ofDigits(-1)\,L = (L.map(\x -> (x : \mathbb{Z}))).alternatingSum$$

Lean4

theorem ofDigits_neg_one : ∀ L : List ℕ, ofDigits (-1 : ℤ) L = (L.map fun n : ℕ => (n : ℤ)).alternatingSum
  | [] => rfl
  | [n] => by simp [ofDigits, List.alternatingSum]
  | a :: b :: t => by
    simp only [ofDigits, List.alternatingSum, List.map_cons, ofDigits_neg_one t]
    ring

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