instGroupSubtypeMatrixSumMemSubmonoidSymplecticGroup

English

The set of symplectic matrices forms a group under ordinary matrix multiplication.

Русский

Множество симплектических матриц образует группу под обычным умножением матриц.

LaTeX

$$SymplecticGroup(l,R) is a group under matrix multiplication$$

Lean4

instance : Group (symplecticGroup l R) :=
  { SymplecticGroup.hasInv, Submonoid.toMonoid _ with
    inv_mul_cancel := fun A => by
      apply Subtype.ext
      simp only [Submonoid.coe_one, Submonoid.coe_mul, Matrix.neg_mul, coe_inv]
      exact inv_left_mul_aux A.2 }

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