Commit 2024-08-27 11:16 d158637d

View on Github →

feat(Data/Finset): add singleton_inter (#16174) Two simple lemmas that are very useful for rewrites especially inside summations.

Estimated changes

added theorem Finset.inter_singleton
added theorem Finset.singleton_inter