term∑ᶠ_,_ — Mathlib

Lean4
/-- `∑ᶠ x, f x` is notation for `finsum f`. It is the sum of `f x`, where `x` ranges over the
support of `f`, if it's finite, zero otherwise. Taking the sum 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))
Похожие утверждения