inv_left_mul_aux — Mathlib

English

For any A in the symplectic group, the identity -(J A^T J A) = 1 holds, i.e., J A^T J A = -I.

Русский

Для любой A из симплектической группы выполняется тождество -(J A^T J A) = 1, то есть J A^T J A = -I.

LaTeX

$$-(J(l,R) * A^T * J(l,R) * A) = I$$

Lean4

theorem inv_left_mul_aux (hA : A ∈ symplecticGroup l R) : -(J l R * Aᵀ * J l R * A) = 1 :=
  calc
    -(J l R * Aᵀ * J l R * A) = (-J l R) * (Aᵀ * J l R * A) := by simp only [Matrix.mul_assoc, Matrix.neg_mul]
    _ = (-J l R) * J l R := by
      rw [mem_iff'] at hA
      rw [hA]
    _ = (-1 : R) • (J l R * J l R) := by simp only [Matrix.neg_mul, neg_smul, one_smul]
    _ = (-1 : R) • (-1 : Matrix _ _ _) := by rw [J_squared]
    _ = 1 := by simp only [neg_smul_neg, one_smul]

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