hasCoeToLinearEquiv — Mathlib

English

There is a canonical coercion from LieModuleEquiv to LinearEquiv, via the associated linear equivalence.

Русский

Существует каноническое приведение из LieModuleEquiv к LinearEquiv через соответствующее линейное эквивалентное отображение.

LaTeX

$$$e \mapsto e.toLinearEquiv$$$

Lean4

instance hasCoeToLinearEquiv : CoeOut (M ≃ₗ⁅R,L⁆ N) (M ≃ₗ[R] N) :=
  ⟨toLinearEquiv⟩

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