ofLinearEquiv — Mathlib

English

An linear equivalence f: M ≃ M gives a corresponding element of GeneralLinearGroup R M.

Русский

Линейная эквивалентность f:M≃M порождает элемент GeneralLinearGroup R M.

LaTeX

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

Lean4

/-- An equivalence from `M` to itself determines an invertible linear map. -/
def ofLinearEquiv (f : M ≃ₗ[R] M) : GeneralLinearGroup R M
    where
  val := f
  inv := (f.symm : M →ₗ[R] M)
  val_inv := LinearMap.ext fun _ ↦ f.apply_symm_apply _
  inv_val := LinearMap.ext fun _ ↦ f.symm_apply_apply _

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