symplectic_det — Mathlib

English

For any symplectic matrix A, its determinant is a unit in the ring R (i.e., det(A) is invertible).

Русский

Для любой симплектической матрицы A детерминант det(A) является единицей в кольце R (обратим).

LaTeX

$$A ∈ Sp(l,R) ⇒ det(A) ∈ R^×$$

Lean4

theorem symplectic_det (hA : A ∈ symplecticGroup l R) : IsUnit <| det A :=
  by
  rw [isUnit_iff_exists_inv]
  use A.det
  refine (isUnit_det_J l R).mul_left_cancel ?_
  rw [mul_one]
  rw [mem_iff] at hA
  apply_fun det at hA
  simp only [det_mul, det_transpose] at hA
  rw [mul_comm A.det, mul_assoc] at hA
  exact hA

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