mul_ofDigits — Mathlib

English

Multiplication distributes over ofDigits: multiplying the ofDigits b l by n equals ofDigits b applied to the list l with every element multiplied by n.

Русский

Умножение распределяется по операции ofDigits: n · ofDigits(b,l) = ofDigits(b, map (n·) l).

LaTeX

$$$ n \cdot \mathrm{ofDigits}(b,l) = \mathrm{ofDigits}\big(b,\, l.map( (\lambda x. n \cdot x))\big) $$$

Lean4

theorem mul_ofDigits (n : ℕ) {b : ℕ} {l : List ℕ} : n * ofDigits b l = ofDigits b (l.map (n * ·)) := by
  induction l with
  | nil => rfl
  | cons hd tl ih =>
    rw [List.map_cons, ofDigits_cons, ofDigits_cons, ← ih]
    ring

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