mathlib

494132e1 - feat(algebra): commuting elements (#1089)

feat(algebra): commuting elements (#1089) * Not sure how this works * Small refactor of geometric sums * Properties of commuting elements * Geometric sums moved to geom_sum.lean * Geometric sums, two commuting variables * Import geom_sum.lean * Cover commuting elements of noncommutative rings * Whitespace * Add file headers * Delete stray file * Sum/prod over range 0, range 1 * Add simp lemmas * Various changes from PR review * Add semigroup case * Changes from PR review * Corrected all_commute to commute.all * Minor changes from PR review * Change line endings back to unix * `@[to_additive]` can't be a `local attribute` * Rename `add_pow_comm` to `add_pow_of_commute` as suggested by @jcommelin * Add a few missing instances * DRY * Notation for `gsmul` should go into `add_group`, not `group` * Prove `gsmul_one` * Reorder `algebra/commute`, add more lemmas * Add docs, rename `geom_sum₂_mul_add_comm` to `commute.geom_sum₂_mul_add`. * Rename, add a docstring * Fix a typo spotted by @ChrisHughes24 * Move common args to `variables` * Rename `commute.mul` to `commute.mul_right` etc. * Add some `@[simp]` attributes. * More `@[simp]` * Add some `_iff` versions