coe_inv

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

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

English

For mk'' and IsUnit det, the determinant behavior respects the GL_n structure.

Русский

Для mk'' и IsUnit det детерминант согласуется с структурой GL_n.

LaTeX

$$det (A) = det (A) for GL_n(R)$$

Lean4

theorem coe_inv : ↑A⁻¹ = (↑A : Matrix n n R)⁻¹ :=
  letI := A.invertible
  invOf_eq_nonsing_inv (↑A : Matrix n n R)

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

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

Разделы

Аффилиация

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