English
If f has a product with respect to L, then f is Multipliable with respect to L.
Русский
Если для f существует произведение по L, значит f является Multipliable по L.
LaTeX
$$$ HasProd f a L \rightarrow Multipliable f L $$$
Lean4
@[inherit_doc tprod, term_parser 1000]
public meta def «term∏'[_]_,_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `«term∏'[_]_,_» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "∏'[") (ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "]"))
Batteries.ExtendedBinder.extBinders)
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 67))
