coe_GL_coe_matrix

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

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

English

Injection of mapGL: if mapGL S g = mapGL S g', then g = g'.

Русский

Инъекция mapGL: если mapGL S g = mapGL S g', то g = g'.

LaTeX

$$\\text{mapGL_inj} \\;:\\; g,g' \\in \\mathrm{SL}_n(R) \\Rightarrow (\\mathrm{mapGL}(S)\\,g = \\mathrm{mapGL}(S)\\,g') \\Rightarrow g = g'$$

Lean4

@[simp]
theorem coe_GL_coe_matrix (g : SpecialLinearGroup n R) : ((toGL g) : Matrix n n R) = g :=
  rfl

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

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

Разделы

Аффилиация

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