term_→ₐc_ — Mathlib

English

The underlying linear map of an AlgEquiv structure within a BialgEquiv is the same map as the AlgEquiv's own underlying linear map.

Русский

Внутреннее линейное отображение AlgEquiv внутри BialgEquiv совпадает с линейным отображением самого AlgEquiv.

LaTeX

$$$\\text{coe_ofAlgEquiv } (e : A \\equiv_{bialg} B) : (e: A \\to B) = e$$$

Lean4

@[inherit_doc BialgHom, term_parser 1000]
public meta def «term_→ₐc_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `«term_→ₐc_» 25 26
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " →ₐc ") (ParserDescr.cat✝ `term 25))

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