Commit 2024-02-29 09:37 51b9fc49

View on Github →

chore: Generalise big operators lemmas to PosMulMono (#10875) Action a TODO

Estimated changes

modified theorem Finset.prod_add_prod_le