smul_apply — Mathlib

English

In the coextended setting, for s, s' ∈ S and g a linear map, (s • g) at s' equals g at (s' s): (s • g) s' = g (s' s).

Русский

В корасширенной настройке, для скаляров s, s' и линейного отображения g, (s • g) на s' равно g на (s' s).

LaTeX

$$$(s \cdot g)\,s' = g\,(s' \cdot s)$$$

Lean4

theorem smul_apply (M : ModuleCat R) (g : (coextendScalars f).obj M) (s s' : S) : (s • g) s' = g (s' * s) :=
  rfl

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