instCoeToSemilinearEquiv — Mathlib

English

Under suitable ring-hom inverse pair hypotheses and EquivLike structure, F carries a SemilinearMapClass structure with respect to σ and M, M₂.

Русский

При наличии соответствующих предпосылок о парах обратных отображений колец и структуры EquivLike, F образует структуру SemilinearMapClass по отношению к σ и M, M₂.

LaTeX

$$$ \text{SemilinearMapClass } F \sigma M M_2 $$$

Lean4

/-- Reinterpret an element of a type of semilinear equivalences as a semilinear equivalence. -/
instance instCoeToSemilinearEquiv [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [EquivLike F M M₂]
    [SemilinearEquivClass F σ M M₂] : CoeHead F (M ≃ₛₗ[σ] M₂) where coe f := semilinearEquiv f

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