coe_one

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

URI: https://scilib.ai/kg/mathlib#Matrix.GeneralLinearGroup.coe_one

English

The unit element 1 in GL_n(R) corresponds to the identity matrix.

Русский

Единица в GL_n(R) соответствует единичной матрице.

LaTeX

$$↑(1 : GL n R) = (1 : Matrix n n R)$$

Lean4

@[simp]
theorem coe_one : ↑(1 : GL n R) = (1 : Matrix n n R) :=
  rfl

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

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

Разделы

Аффилиация

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