map_neg

Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

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

English

There is a linear map structure on LeftInvariantDerivation compatible with the ambient derivation-calculus on model-with-corners self maps.

Русский

Для LeftInvariantDerivation существует линейная структура совместимо с вычислением выводов на моделях с углами.

LaTeX

$$LinearMapClass: LeftInvariantDerivation → ContMDiffMap$$

Lean4

protected theorem map_neg : X (-f) = -X f := by simp

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

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

Разделы

Аффилиация

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