linearMap_comp — Mathlib

English

The linear map corresponding to the composition g ∘ f equals the composition of the linear maps corresponding to g and f.

Русский

Линейное отображение, соответствующее композиции g ∘ f, равно композиции линейных отображений, соответствующих g и f.

LaTeX

$$$\operatorname{linearMap} R\ M\ (g \circ f) = (\operatorname{linearMap} R\ M\ g) \circ (\operatorname{linearMap} R\ M\ f)$$$

Lean4

theorem linearMap_comp [Finite X] [Finite Y] [Finite Z] (f : X → Y) (g : Y → Z) :
    linearMap R M (g.comp f) = (linearMap R M g).comp (linearMap R M f) := by classical aesop

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