toLinearEquiv — Mathlib

English

If e: M ≃ M2 is an equivalence and its underlying function is linear, then it is a linear equivalence: there exists a LinearEquiv (id_R) M M2 with e as its underlying equivalence.

Русский

Если e: M ≃ M2 — это эквивелентность, и как функция она линейна, то она является линейной эквивалентностью: существует LinearEquiv (id_R) M M2 с e как тождественным эквивалентом.

LaTeX

$$$ \text{toLinearEquiv}(e,h) : M \simeq_{\ell[R]} M_2 $$$

Lean4

/-- An equivalence whose underlying function is linear is a linear equivalence. -/
def toLinearEquiv (e : M ≃ M₂) (h : IsLinearMap R (e : M → M₂)) : M ≃ₗ[R] M₂ :=
  { e, h.mk' e with }

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