term_→ₙₐ[_]_ — Mathlib

English

There is a canonical way to turn an element f of a type F with NonUnitalAlgHomClass into a concrete NonUnitalAlgHom φ A B, via a universal coercion using MonoidHom.id.

Русский

Существует канонический способ перевести элемент f типа F со своим NonUnitalAlgHomClass в конкретный NonUnitalAlgHom φ A B через единичный моноид-гомоморфизм.

LaTeX

$$$ toNonUnitalAlgHom(f) : A \\toₙₐ[R] B $$$

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))

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