Commit 2021-02-10 00:03 b34da002

View on Github →

feat(algebra/geom_sum): adds further variants (#6077) This adds further variants for the value of geom_series\2. Additionally, a docstring is provided. Thanks to Patrick Massot for help with the reindexing of sums.

Estimated changes

Modified src/algebra/geom_sum.lean

added theorem commute.mul_geom_sum₂

added theorem commute.mul_neg_geom_sum₂

added theorem geom_sum₂_Ico

deleted theorem geom_sum₂_mul_comm

added theorem geom₂_sum

added theorem mul_geom_sum₂_Ico

added theorem op_geom_series₂

Modified src/algebra/opposites.lean

added theorem opposite.commute.op

added theorem opposite.commute.unop

added theorem opposite.commute_op

added theorem opposite.commute_unop

added theorem opposite.semiconj_by.op

added theorem opposite.semiconj_by.unop

added theorem opposite.semiconj_by_op

added theorem opposite.semiconj_by_unop