s_as_blocks

Mathlib.Algebra.Lie.Classical

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

← MathLib Explorer

English

The matrix S is explicitly the block form fromBlocks 1 0 0 (-1).

Русский

Матрица S имеет явный блочный вид fromBlocks 1 0 0 (-1).

LaTeX

$$$ S(l,R) = \begin{pmatrix} I_l & 0 \\ 0 & -I_l \end{pmatrix},$$$

Lean4

theorem s_as_blocks : S l R = Matrix.fromBlocks 1 0 0 (-1) :=
  by
  rw [← Matrix.diagonal_one, Matrix.diagonal_neg, Matrix.fromBlocks_diagonal]
  rfl

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

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

Разделы

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

Аффилиация

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