evalAt_coe

Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

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

English

Evaluation-at commutes with the derivation map: evalAt g X = X evaluated at g.

Русский

evalAt сохраняет отображение: evalAt g X = X при g.

LaTeX

$$$ \mathrm{evalAt}(g,X) = X.\mathrm{evalAt}(g) $$$

Lean4

@[simp]
theorem evalAt_coe : Derivation.evalAt g ↑X = evalAt g X :=
  rfl

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

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

Разделы

Аффилиация

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