Commit 2025-03-20 22:56 23c0c2c0
View on Github →chore(Algebra/Group): split off big operators from Pointwise/Finset/Basic.lean (#23156)
These lemmas cause a relatively big import bump and seem to be otherwise unused. The file Pointwise/Finset/Basic.lean is still too long but does not seem to have any other obvious splitting points.