toFin_zsmul — Mathlib

English

The map toFin respects natural scalar multiplication: toFin (n • x) = n • x.toFin.

Русский

toFin сохраняет умножение на константу: toFin (n • x) = n • x.toFin.

LaTeX

$$$\forall n \in \mathbb{N},\; \mathrm{toFin}(n \cdot x) = n \cdot \mathrm{toFin}(x)$$$

Lean4

theorem toFin_zsmul (z : ℤ) (x : BitVec w) : toFin (z • x) = z • x.toFin :=
  toFin_mul _ _ |>.trans <| by open scoped Fin.CommRing in simp only [zsmul_eq_mul, toFin_intCast]

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