instSemilinearMapClass — Mathlib

English

CongLeft is defined as the linear isomorphism between spaces of linear maps induced by a given linear isomorphism e on the domain; it acts by precomposition with e.

Русский

CongLeft определяется как линейное изоморфизм между пространствами линейных отображений, индуцируемый данным линейным изоморфизмом e на домене; действует преддекомпозицией с e.

LaTeX

$$$ (M_2 \to_{\mathbb{R}} M) \simeq_{\mathsf{S}} (M_3 \to_{\mathbb{R}} M) $$$

Lean4

instance (priority := 100) [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [EquivLike F M M₂]
    [s : SemilinearEquivClass F σ M M₂] : SemilinearMapClass F σ M M₂ :=
  { s with }

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