invertiblePD

Mathlib.Algebra.Lie.Classical

URI: https://scilib.ai/kg/mathlib#LieAlgebra.Orthogonal.invertiblePD

English

PD is invertible (over a finite type l and invertible 2 in R).

Русский

PD обратима при конечном размере l и существовании обратного 2 в R.

LaTeX

$$$ PD(l,R) \text{ is invertible in } M_{2\ell}(R). $$$

Lean4

instance invertiblePD [Fintype l] [Invertible (2 : R)] : Invertible (PD l R) :=
  invertibleOfRightInverse _ _ (pd_inv l R)

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

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

Разделы

Аффилиация

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