comapSMul — Mathlib

English

There is a domain-wise scalar action on finsupps: g • f = mapDomain (g · ·) f, i.e., precomposition by g on the domain.

Русский

Существует скалярное действие на домене: g • f = mapDomain (g • ·) f, то есть предобразование по действию g на область.

LaTeX

$$$ g \\cdot f = \\mathrm{mapDomain}(g \\cdot \\,,) f $$$

Lean4

/-- Scalar multiplication acting on the domain.

This is not an instance as it would conflict with the action on the range.
See the `instance_diamonds` test for examples of such conflicts. -/
def comapSMul : SMul G (α →₀ M) where smul g := mapDomain (g • ·)

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