term_→⋆ₐ[_]_ — Mathlib

English

Any F with algebra and star-hom structures yields a StarAlgHom by forgetting extra structure.

Русский

Любой F со структурами алгоморфизма и звездности порождает StarAlgHom, забывая лишнюю структуру.

LaTeX

$$toStarAlgHom(f) : A →⋆ₐ[R] B$$

Lean4

@[inherit_doc StarAlgHom, 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))

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