smul_apply' — Mathlib

English

For coextension of scalars, the map (coextendScalars f).map g evaluated at x and s equals g applied to x evaluated at s: (coextendScalars f).map g x s = g (x s).

Русский

При расширении сопряжённых скаляров отображение (coextendScalars f).map g на x и s равно g(x на s).

LaTeX

$$$(coextendScalars f).map\ g\ x\ s = g\ (x\ s)$$$

Lean4

@[simp]
theorem smul_apply' (s : S) (g : (restrictScalars f).obj (of _ S) →ₗ[R] M) (s' : S) : (s • g) s' = g (s' * s : S) :=
  rfl

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