coe_zsmul

Mathlib.Algebra.Lie.Basic

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

English

For z ∈ ℤ, the underlying function of z • f equals z • (f as function).

Русский

При z ∈ ℤ, подстановка коэффициента z • f соответствует z • (f как функция).

LaTeX

$$$\forall z \in \mathbb{Z}:\ (z \cdot f) = z \cdot (f)$ as functions$$

Lean4

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

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

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

Разделы

Аффилиация

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