term_→ₛₙₐ[_]_ — Mathlib

English

Given suitable module structures, the NonUnitalAlgHomClass F φ A B yields a SemilinearMapClass structure with map_smulₛₗ compatibility.

Русский

При наличии соответствующих структур модуля NonUnitalAlgHomClass F φ A B образует SemilinearMapClass с совместимостью map_smulₛₗ.

LaTeX

$$$ SemilinearMapClass F φ A B $ with $ map_smulₛₗ $$$

Lean4

@[inherit_doc NonUnitalAlgHom, term_parser 1000]
public meta def «term_→ₛₙₐ[_]_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `«term_→ₛₙₐ[_]_» 25 0
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " →ₛₙₐ[") (ParserDescr.cat✝ `term 0))
        (ParserDescr.symbol✝ "] "))
      (ParserDescr.cat✝ `term 0))

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