toAddAction — Mathlib

English

A flow supplies an additive action on τ and α, with vadd = ϕ, add_vadd = ϕ.map_add', zero_vadd = ϕ.map_zero'.

Русский

Поток задаёт притяжение к аддитивному действию: vadd = ϕ, add_vadd = ϕ.map_add', zero_vadd = ϕ.map_zero'.

LaTeX

$$$\text{toAddAction} : \mathrm{AddAction}(\tau, \alpha)$ with $\, vadd = \varphi,\ add\_vadd = \varphi_{\mathrm{map\_add}},\ zero\_vadd = \varphi_{\mathrm{map\_zero}}$$$

Lean4

/-- Convert a flow to an additive monoid action. -/
def toAddAction : AddAction τ α where
  vadd := ϕ
  add_vadd := ϕ.map_add'
  zero_vadd := ϕ.map_zero'

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