instSub

Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

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

English

Subtracting two left-invariant derivations yields a left-invariant derivation.

Русский

Разность двух лево-инвариантных выводителей даёт лево-инвариантный вывод.

LaTeX

$$$ \forall X,Y \in \mathrm{LeftInvariantDerivation}(I,G):\; X - Y \in \mathrm{LeftInvariantDerivation}(I,G). $$$

Lean4

instance : Sub (LeftInvariantDerivation I G) where sub X Y := ⟨X - Y, fun g => by simp [left_invariant']⟩

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

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

Разделы

Аффилиация

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