coe_smul

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#LieModuleHom.coe_smul

English

For t ∈ R, the scalar action commutes with the coe: the function underlying t • f equals t times the function f.

Русский

Для t ∈ R действие скаляра совместимо с приведение: функция подлежащая t • f равна t • f.

LaTeX

$$$\forall t \in R:\ (t \cdot f) = t \cdot f$ as functions$$

Lean4

@[norm_cast, simp]
theorem coe_smul (t : R) (f : M →ₗ⁅R,L⁆ N) : ⇑(t • f) = t • (⇑f) :=
  rfl

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

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

Разделы

Аффилиация

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