mapDomain_smul — Mathlib

English

Mapping domain commutes with scalar multiplication: mapDomain f (b • v) = b • mapDomain f v for AddCommMonoid M with DistribSMul.

Русский

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

LaTeX

$$$[AddCommMonoid M][DistribSMul R M] \\; {f : \\alpha \\to \\beta} \\, (b : R) \\, (v : \\alpha \\to_0 M) : \\; mapDomain f (b \\cdot v) = b \\cdot mapDomain f v$$$

Lean4

theorem mapDomain_smul [AddCommMonoid M] [DistribSMul R M] {f : α → β} (b : R) (v : α →₀ M) :
    mapDomain f (b • v) = b • mapDomain f v :=
  mapDomain_mapRange _ _ _ _ (smul_add b)

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