map_smulₛₗ — Mathlib

English

An instance asserts that any F with MulSemiringActionSemiHomClass admits a canonical coercion to a MulSemiringActionHom.

Русский

Инстанс утверждает существование канонического приведения типа для любого F с MulSemiringActionSemiHomClass к MulSemiringActionHom.

LaTeX

$$$[MulSemiringActionSemiHomClass F (\phi) (R) (S)] \Rightarrow F \to (R \to_{\phi}^{*} S)$$$

Lean4

protected theorem map_smulₛₗ (f : R →ₑ+*[φ] S) (m : M) (x : R) : f (m • x) = φ m • f x :=
  map_smulₛₗ f m x

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