toLinearMap_eq_coe — Mathlib

English

The linear map associated to a semilinear equivalence equals the semilinear map determined by that equivalence.

Русский

Линейное отображение, соответствующее семилинейной эквивалентности, равно семилинейному отображению, заданному этой эквивалентностью.

LaTeX

$$toLinearMap e = SemilinearMapClass.semilinearMap e$$

Lean4

theorem toLinearMap_eq_coe {e : M ≃ₛₗ[σ] M₂} : e.toLinearMap = SemilinearMapClass.semilinearMap e :=
  rfl

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