coe_zero

Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

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

English

LeftInvariantDerivation(I,G) is closed under subtraction, forming an abelian group under addition.

Русский

Лево-инвариантные выводы образуют абелеву группу относительно сложения.

LaTeX

$$$ \mathrm{LeftInvariantDerivation}(I,G) \text{ is closed under subtraction and addition forms an abelian group. }$$$

Lean4

@[simp]
theorem coe_zero : ⇑(0 : LeftInvariantDerivation I G) = 0 :=
  rfl

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

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

Разделы

Аффилиация

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