coe_ofDigits — Mathlib

English

In any semiring α, the natural embedding commutes with interpreting a digit list: casting ofDigits(b,L) equals ofDigits(b cast, L).

Русский

Во всякой полугруппе-полуколона α натуральное отображение коммутирует с интерпретацией списка цифр: cast(ofDigits(b,L)) = ofDigits(b_cast, L).

LaTeX

$$$(\\operatorname{ofDigits}(b,L) : \\alpha) = \\operatorname{ofDigits}(b:\\alpha,L).$$$

Lean4

@[norm_cast]
theorem coe_ofDigits (α : Type*) [Semiring α] (b : ℕ) (L : List ℕ) : ((ofDigits b L : ℕ) : α) = ofDigits (b : α) L := by
  induction L with
  | nil => simp [ofDigits]
  | cons d L ih => dsimp [ofDigits]; push_cast; rw [ih]

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