toGL_injective

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

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

English

Equivalence: (toGL(g) = g') iff g = g'.

Русский

Эквивалентность: (toGL(g) = g') эквивалентно g = g'.

LaTeX

$$\\bigl( \\mathrm{toGL}(g) = g' \\bigr) \\; \\iff \\; g = g'$$

Lean4

theorem toGL_injective : Function.Injective (toGL : SpecialLinearGroup n R → GL n R) := fun g g' ↦ by
  simpa [toGL] using fun h _ ↦ Subtype.ext h

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

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

Разделы

Аффилиация

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