coe_toLin

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

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

English

If g is in GL_n(R), then det(g) ≠ 0.

Русский

Если g ∈ GL_n(R), то det(g) ≠ 0.

LaTeX

$$g ∈ GL n R → g.val.det ≠ 0$$

Lean4

@[simp]
theorem coe_toLin : (toLin A : (n → R) →ₗ[R] n → R) = Matrix.mulVecLin A :=
  rfl

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

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

Разделы

Аффилиация

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