coe_smul

Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

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

English

The coercion commutes with scalar multiplication: ↑(k • X) = k • ↑X.

Русский

Приведение к функции commuting с умножением на скаляр: ↑(k • X) = k • ↑X.

LaTeX

$$$ \uparrow\bigl(k \cdot X\bigr) = k \cdot \uparrow X. $$$

Lean4

@[simp]
theorem coe_smul : ⇑(r • X) = r • ⇑X :=
  rfl

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

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

Разделы

Аффилиация

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