J_inv

Mathlib.LinearAlgebra.SymplecticGroup

URI: https://scilib.ai/kg/mathlib#Matrix.J_inv

English

The product J J equals minus the identity: J^2 = -I.

Русский

Произведение J J равно минус единица: J^2 = -I.

LaTeX

$$$J^2 = -I$$$

Lean4

theorem J_inv : (J l R)⁻¹ = -J l R := by
  refine Matrix.inv_eq_right_inv ?_
  rw [Matrix.mul_neg, J_squared]
  exact neg_neg 1

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

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

Разделы

Аффилиация

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