map_smul — Mathlib

English

Two functions are equal if they agree on all inputs; extensionality principle for MulSemiringActionHom.

Русский

Две функции равны, если они совпадают на всех входах; экстенциональность для MulSemiringActionHom.

LaTeX

$$$\forall x, f(x)=g(x) \Rightarrow f=g$$$

Lean4

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

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