mapDomain_smul — Mathlib

English

Map domain commutes with scalar multiplication: mapDomain f (b • v) equals b • mapDomain f v.

Русский

MapDomain коммутирует скалярное умножение: mapDomain f (b • v) = b • mapDomain f v.

LaTeX

$$$$ mapDomain f (b \cdot v) = b \cdot mapDomain f v $$$$

Lean4

theorem mapDomain_smul {R : Type*} [Monoid R] [DistribMulAction R k] {b : R} :
    mapDomain f (b • v) = b • mapDomain f v :=
  by
  simp_rw [← toFinsupp_inj, toFinsupp_smul, toFinsupp_mapDomain]
  simp [Finsupp.mapDomain_smul]

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