map_id

Mathlib.RingTheory.Extension.Cotangent.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.Extension.CotangentSpace.map_id

English

The cotangent space map of the identity is the identity linear map.

Русский

Отображение котант пространства при тождественном отображении есть тождественное линейное отображение.

LaTeX

$$\\mathrm{CotangentSpace}.map(\\mathrm{id}) = \\mathrm{LinearMap.id}$$

Lean4

@[simp]
theorem map_id : CotangentSpace.map (.id P) = LinearMap.id := by ext; simp

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

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

Разделы

Аффилиация

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