instGroup — Mathlib

English

SL(n, R) is a group under multiplication with inversion given by standard matrix inverse.

Русский

SL(n, R) образует группу относительно умножения, обратное — обычная обратная матрица.

LaTeX

$$SL_n(R) \text{ is a group under } \cdot, \ A^{-1} \in SL_n(R)$$

Lean4

instance : Group (SpecialLinearGroup n R) :=
  { SpecialLinearGroup.monoid, SpecialLinearGroup.hasInv with
    inv_mul_cancel := fun A => by
      ext1
      simp [adjugate_mul] }

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