instSMul

Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

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

English

Evaluation-at map satisfies evalAt g X f = (X f) g.

Русский

Оценка в точке g применима к X на f так: evalAt g X f = (X f) g.

LaTeX

$$$ \text{evalAt } g X f = (X f) g. $$$

Lean4

instance : SMul 𝕜 (LeftInvariantDerivation I G) where
  smul r X := ⟨r • X.1, fun g => by simp_rw [LinearMap.map_smul, left_invariant']⟩

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

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

Разделы

Аффилиация

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