toLinearMap_injective

Mathlib.LinearAlgebra.QuadraticForm.Isometry

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

← MathLib Explorer

English

Same idea as above: the underlying linear map uniquely determines the Isometry.

Русский

Та же идея: базовое линейное отображение точно определяет изометрию.

LaTeX

$$Isometry.toLinearMap is injective$$

Lean4

theorem toLinearMap_injective : Function.Injective (Isometry.toLinearMap : (Q₁ →qᵢ Q₂) → M₁ →ₗ[R] M₂) := fun _f _g h =>
  DFunLike.coe_injective (congr_arg DFunLike.coe h :)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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