units_smul_comp — Mathlib

English

Composition with a fixed right argument is linear in the left argument, and composition with a fixed left argument is linear in the right argument, respecting units.

Русский

Сложение с единичными скалярами по коэффициентам совместимо: левая/правая линейность сохраняется для единиц.

LaTeX

$$$\\forall f,g, r\\in R^{\\times},\\ (r\\cdot f)\\circ g = r\\cdot(f\\circ g).$$$

Lean4

@[simp]
theorem units_smul_comp {X Y Z : C} (r : Rˣ) (f : X ⟶ Y) (g : Y ⟶ Z) : (r • f) ≫ g = r • f ≫ g := by
  apply Linear.smul_comp

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