hasCoeToGeneralLinearGroup

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

URI: https://scilib.ai/kg/mathlib#Matrix.SpecialLinearGroup.hasCoeToGeneralLinearGroup

English

The inclusion map toGL is injective: if toGL(g) = toGL(g'), then g = g'.

Русский

Включение toGL инъективно: если toGL(g) = toGL(g'), то g = g'.

LaTeX

$$Injective(\\mathrm{toGL})$$

Lean4

instance hasCoeToGeneralLinearGroup : Coe (SpecialLinearGroup n R) (GL n R) :=
  ⟨toGL⟩

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

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

Разделы

Аффилиация

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