Commit 2022-04-04 09:32 b189be76
View on Github →feat(algebra/big_operators): add commute.*_sum_{left,right} lemmas (#13035)
This moves the existing prod_commute lemmas into the commute namespace for discoverabiliy, and adds the swapped variants.
This also fixes an issue where lemmas about add_commute were misnamed using commute.