mathlib

8304b951 - refactor(algebra/big_operators/*): Generalize to division monoids (#14189)

refactor(algebra/big_operators/*): Generalize to division monoids (#14189) Generalize big operators lemmas to `division_comm_monoid`. Rename `comm_group.inv_monoid_hom` to `inv_monoid_hom` because it is not about`comm_group` anymore and we do not use classes as namespaces.