term∏ᶠ_,_ — Mathlib

Lean4
/-- `∏ᶠ x, f x` is notation for `finprod f`. It is the product of `f x`, where `x` ranges over the
multiplicative support of `f`, if it's finite, one otherwise. Taking the product over multiple
arguments or conditions is possible, e.g. `∏ᶠ (x) (y), f x y` and `∏ᶠ (x) (h: x ∈ s), f x` -/
@[term_parser 1000]
public meta def «term∏ᶠ_,_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `«term∏ᶠ_,_» 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "∏ᶠ") Batteries.ExtendedBinder.extBinders)
        (ParserDescr.symbol✝ ", "))
      (ParserDescr.cat✝ `term 67))
Похожие утверждения