smul_monoidHom_apply

Mathlib.GroupTheory.GroupAction.DomAct.Basic

URI: https://scilib.ai/kg/mathlib#DomMulAct.smul_monoidHom_apply

English

For c ∈ DomMulAct M and f ∈ A →* B and a ∈ A, (c • f) a = f(mk.symm c • a).

Русский

Для c ∈ DomMulAct M и f ∈ A →* B и a ∈ A выполняется (c • f) a = f(mk.symm c • a).

LaTeX

$$$(c \cdot f)(a) = f(mk.symm c \cdot a)$$$

Lean4

theorem smul_monoidHom_apply (c : Mᵈᵐᵃ) (f : A →* B) (a : A) : (c • f) a = f (mk.symm c • a) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru