instEquivLike — Mathlib

English

The semilinear equivalences between M and M₂ form an EquivLike structure with coercion to functions and inverse given by the inverse map, satisfying the usual left and right inverse properties.

Русский

Множество семилинейных эквивалентностей между M и M₂ образует структуру EquivLike: привод к функциям, обратная функция задаётся обратной и выполняются стандартные свойства левой и правой обратности.

LaTeX

$$$\text{EquivLike}(M \simeq_{σ} M_2)\ M\ M_2$$$

Lean4

instance : EquivLike (M ≃ₛₗ[σ] M₂) M M₂ where
  coe e := e.toFun
  inv := LinearEquiv.invFun
  coe_injective' _ _ h _ := toLinearMap_injective (DFunLike.coe_injective h)
  left_inv := LinearEquiv.left_inv
  right_inv := LinearEquiv.right_inv

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