map_zero

Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

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

English

Coe from LeftInvariantDerivation to Derivation is injective; different choices yield different derivations.

Русский

Отображение приведения из LeftInvariantDerivation к Derivation инъективно; разные варианты порождают разные выводимости.

LaTeX

$$Injective(toDerivation: LeftInvariantDerivation I G → Derivation 𝕜 ... )$$

Lean4

protected theorem map_zero : X 0 = 0 := by simp

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

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

Разделы

Аффилиация

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