Commit 2025-05-04 00:34 d076a503
View on Github →chore: Merge the two series of lemmas on big operators in locally finite orders (#17404)
I accidentally introduced those lemmas twice: In #9386 and also in #17280 under different names. I prefer the names I gave in the former, but the file I gave in the latter. Also generalise other lemmas in Algebra.BigOperators.Intervals