opcyclesMap_smul — Mathlib

English

In a linear setting, the map that assigns to a morphism φ its opcycles data is compatible with scalar multiplication: applying a scalar a to φ before mapping is the same as mapping φ first and then multiplying by a.

Русский

В линейном контексте отображение, отправляющее морфизм φ в данные опциклов, согласовано с умножением на скаляр: сначала применить скаляр a к φ, затем перейти к опциклам, или сначала перейти к опциклам и затем умножить на a.

LaTeX

$$$\\operatorname{opcyclesMap}(a \\cdot \\varphi) = a \\cdot \\operatorname{opcyclesMap}(\\varphi)$$$

Lean4

@[simp]
theorem opcyclesMap_smul : opcyclesMap (a • φ) = a • opcyclesMap φ :=
  opcyclesMap'_smul _ _ _ _

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