coe_toLinearMap

Mathlib.LinearAlgebra.QuadraticForm.Isometry

URI: https://scilib.ai/kg/mathlib#QuadraticMap.Isometry.coe_toLinearMap

English

For any isometry f: Q1 →qᵢ Q2, the underlying linear map coincides with f; i.e., the map f considered as a linear map is exactly the action of f.

Русский

Для любой изометрии f: Q1 →qᵢ Q2 линейное отображение, лежащее в основе f, совпадает с самим f.

LaTeX

$$$\operatorname{toLinearMap}(f) = f$$$

Lean4

@[simp]
theorem coe_toLinearMap (f : Q₁ →qᵢ Q₂) : ⇑f.toLinearMap = f :=
  rfl

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

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

Разделы

Аффилиация

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