linearMap_piSingle — Mathlib

English

The linear map induced by f sends Pi.single x m to Pi.single (f x) m.

Русский

Линейное отображение, индуцированное по f, отправляет Pi.single x m в Pi.single (f x) m.

LaTeX

$$$\operatorname{linearMap} R\ M\ f\; (\Pi\text{single } x\, m) = \Pi\text{single } (f x)\, m$$$

Lean4

@[simp]
theorem linearMap_piSingle [Finite X] [Finite Y] [DecidableEq X] [DecidableEq Y] (f : X → Y) (x : X) (m : M) :
    linearMap R M f (Pi.single x m) = Pi.single (f x) m := by apply map_piSingle

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