map_smul — Mathlib

English

If F and G are linear functors, their composition F ⋙ G is linear over R.

Русский

Если F и G линейные функторы, тогда их композиция F ⋙ G линейна по отношению к R.

LaTeX

$$$\\text{FunctorLinear}(F) \\land \\text{FunctorLinear}(G) \\Rightarrow \\text{FunctorLinear}(F \\circ G).$$$

Lean4

@[simp]
theorem map_smul {X Y : C} (r : R) (f : X ⟶ Y) : F.map (r • f) = r • F.map f :=
  Functor.Linear.map_smul _ _

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