generalLinearEquiv — Mathlib

English

The general linear group GL(R,M) is multiplicatively equivalent to the group of linear equivalences M ≃ M.

Русский

Общая линейная группа GL(R,M) эквивалентна множества линейных эквивалентностей M ≃ M.

LaTeX

$$$\mathrm{generalLinearEquiv}: \mathrm{GeneralLinearGroup}(R,M) \simeq_* M \simeq_{R} M$$$

Lean4

/-- The general linear group on `R` and `M` is multiplicatively equivalent to the type of linear
equivalences between `M` and itself. -/
def generalLinearEquiv : GeneralLinearGroup R M ≃* M ≃ₗ[R] M
    where
  toFun := toLinearEquiv
  invFun := ofLinearEquiv
  map_mul' x y := by ext; rfl

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