Commit 2026-03-02 12:12 6ec4302b

View on Github →

feat: push lemmas for Filter.NeBot (#35261)

Estimated changes

Modified Mathlib/Order/Filter/Basic.lean

modified theorem Filter.not_neBot

Modified Mathlib/Order/Filter/Defs.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Defs.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/SummationFilter.lean