toLinearEquiv — Mathlib

English

An invertible linear map determines a linear equivalence from M to M.

Русский

Обратимое линейное отображение задаёт линейное эквивалентство M к M.

LaTeX

$$$\mathrm{toLinearEquiv}: \mathrm{GeneralLinearGroup}(R,M) \to M \simeq_{R} M$$$

Lean4

/-- An invertible linear map `f` determines an equivalence from `M` to itself. -/
def toLinearEquiv (f : GeneralLinearGroup R M) : M ≃ₗ[R] M :=
  { f.val with
    invFun := f.inv.toFun
    left_inv := fun m ↦ show (f.inv * f.val) m = m by simp
    right_inv := fun m ↦ show (f.val * f.inv) m = m by simp }

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