toLin — Mathlib

English

GL_n(R) is equivalent to the group of invertible linear endomorphisms of the free module R^n; there is a multiplicative equivalence to LinearMap.GeneralLinearGroup.

Русский

GL_n(R) эквивалентна группе взаимно обратимых линейных отображений R^n; существует мультипликативное эквивалентное соответствие с LinearMap.GeneralLinearGroup.

LaTeX

$$toLin : GL n R ≃* LinearMap.GeneralLinearGroup R (n → R)$$

Lean4

/-- The groups `GL n R` (notation for `Matrix.GeneralLinearGroup n R`) and
`LinearMap.GeneralLinearGroup R (n → R)` are multiplicatively equivalent -/
def toLin : GL n R ≃* LinearMap.GeneralLinearGroup R (n → R) :=
  Units.mapEquiv toLinAlgEquiv'.toMulEquiv

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