mk'

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

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

← MathLib Explorer

English

Given A and IsUnit(det A), we obtain an element of GL_n(R) by mk'(A).

Русский

Для A и IsUnit(det A) получаем элемент GL_n(R) через mk'(A).

LaTeX

$$def mk' (A : Matrix n n R) (h : Invertible (Matrix.det A)) : GL n R$$

Lean4

/-- Given a matrix with invertible determinant, we get an element of `GL n R`. -/
@[simps! val]
def mk' (A : Matrix n n R) (_ : Invertible (Matrix.det A)) : GL n R :=
  unitOfDetInvertible A

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

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

Разделы

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

Аффилиация

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