id_linear

Mathlib.LinearAlgebra.AffineSpace.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.id_linear

English

The linear part of the identity affine map is the identity linear map.

Русский

Линейная часть тождественного аффинного отображения — тождественное линейное отображение.

LaTeX

$$$\\mathrm{id}_{P_1}.linear = \\mathrm{LinearMap.id}$$$

Lean4

@[simp]
theorem id_linear : (id k P1).linear = LinearMap.id :=
  rfl

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

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

Разделы

Аффилиация

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