comp_nsmul — Mathlib

English

In a preadditive category, composition distributes over left n-fold scalar on the second morphism: for all f : P → Q, g : Q → R and n ∈ ℕ, f ∘ (n • g) = n • (f ∘ g).

Русский

В преддобавительной категории композиция распределяется по левой n‑умножению второго морфизма: для любых f : P → Q, g : Q → R и n ∈ ℕ выполняется f ∘ (n • g) = n • (f ∘ g).

LaTeX

$$$ f \circ (n \cdot g) = n \cdot (f \circ g) $$$

Lean4

theorem comp_nsmul (n : ℕ) : f ≫ (n • g) = n • f ≫ g :=
  map_nsmul (leftComp R f) n g

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