coe_inv' — Mathlib

English

The matrix inverse commutes with the coercion from the symplectic group to matrices: the image of the inverse equals the inverse of the image.

Русский

Образ обратной матрицы совпадает с обратной матрицей образа: преобразование обратной сохраняется под коэрценцией.

LaTeX

$$↑(A^{-1}) = (↑A)^{-1}$$

Lean4

theorem coe_inv' (A : symplecticGroup l R) : (↑A⁻¹ : Matrix (l ⊕ l) (l ⊕ l) R) = (↑A)⁻¹ :=
  by
  refine (coe_inv A).trans (inv_eq_left_inv ?_).symm
  simp [inv_left_mul_aux]

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