instCoeToLinearMap — Mathlib

English

There is a canonical coercion from any f ∈ F to a linear map M1 →ₗ[R] M2, defined by sending f to the semilinear map associated to f.

Русский

Существует каноническое приведение из любого элемента f ∈ F к линейному отображению M1 →ₗ[R] M2, заданное отображением f в связанный с ним полулинейный отображатель.

LaTeX

$$$\mathrm{coe}(f) = \mathrm{SemilinearMapClass.semilinearMap}(f)$$$

Lean4

/-- Reinterpret an element of a type of linear maps as a linear map. -/
instance instCoeToLinearMap : CoeHead F (M₁ →ₗ[R] M₂) where coe f := SemilinearMapClass.semilinearMap f

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