toDigitsCore_lens_eq — Mathlib

English

For any b, f, n and any digit-list tail tl, the length of toDigitsCore b f n (c :: tl) is one more than the length of toDigitsCore b f n tl.

Русский

Для любых b, f, n и любого хвоста цифр tl, длина toDigitsCore b f n (c :: tl) на 1 больше длины toDigitsCore b f n tl.

LaTeX

$$$ \forall b\, f\, n\, c\, tl:\ (\mathrm{toDigitsCore}\ b\ f\ n\ (c :: tl)).length = (\mathrm{toDigitsCore}\ b\ f\ n\ tl).length + 1 $$$

Lean4

theorem toDigitsCore_lens_eq (b f : Nat) :
    ∀ (n : Nat) (c : Char) (tl : List Char),
      (Nat.toDigitsCore b f n (c :: tl)).length = (Nat.toDigitsCore b f n tl).length + 1 :=
  by
  induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length])
  | succ f ih => grind

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