invertiblePB

Mathlib.Algebra.Lie.Classical

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

English

PB(l,R) is invertible whenever 2 is invertible in R.

Русский

PB(l,R) обратима тогда, когда 2 обратимо в R.

LaTeX

$$$ PB(l,R) \text{ is invertible for invertible } 2 \text{ in } R. $$$

Lean4

instance invertiblePB [Invertible (2 : R)] : Invertible (PB l R) :=
  invertibleOfRightInverse _ _ (pb_inv l R)

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

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

Разделы

Аффилиация

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