Lean Focused Research Organization on Mythryl: “Looking for a lemma in #LeanLang / #Mathlib but don't know its name?…”

Looking for a lemma in #LeanLang / #Mathlib but don't know its name? Use Loogle! to search: By pattern: _ * (_ ^ _) finds expressions matching the pattern By conclusion: |- tsum _ = _ * tsum _ finds specific conclusion shapes Combine searches with commas for precision! loogle.lean-lang.org

loogle.lean-lang.orgLoogle - Search Lean and MathlibLoogle is a search tool for finding definitions, theorems, and lemmas in Lean 4 and Mathlib.

23/10/25, 9:09 pm2 reposts4 likes

Post