ofDigits_reverse_zero_cons — Mathlib

English

If the first element is zero, reversing the list does not change the value of the digits.

Русский

Если первая цифра равна нулю, обращение списка не меняет значение цифр.

LaTeX

$$$\\operatorname{ofDigits}(b, (0 :: l)^{\\mathrm{rev}}) = \\operatorname{ofDigits}(b, l^{\\mathrm{rev}}).$$$

Lean4

theorem ofDigits_reverse_zero_cons {b : ℕ} (l : List ℕ) : ofDigits b (0 :: l).reverse = ofDigits b l.reverse := by
  simp only [List.reverse_cons, ofDigits_append_zero]

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