Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-23 01:49 8304b951

View on Github →

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 aboutcomm_group anymore and we do not use classes as namespaces.

Estimated changes

modified theorem finset.prod_erase_eq_div
deleted theorem finset.prod_inv_distrib'
modified theorem finset.prod_inv_distrib
modified theorem finset.prod_sdiff_eq_div
modified theorem finset.prod_zpow
deleted theorem finset.sum_sub_distrib
modified theorem finprod_div_distrib
deleted theorem finprod_div_distrib₀
modified theorem finprod_inv_distrib
deleted theorem finprod_inv_distrib₀
modified theorem finprod_mem_div_distrib
modified theorem finprod_mem_inv_distrib
deleted theorem multiset.prod_map_div₀
modified theorem multiset.prod_map_inv'
modified theorem multiset.prod_map_inv
deleted theorem multiset.prod_map_inv₀
deleted theorem multiset.prod_map_zpow₀
modified def mul_equiv.inv
added theorem mul_equiv.inv_symm
deleted def mul_equiv.inv₀
deleted theorem mul_equiv.inv₀_symm
added theorem coe_inv_monoid_hom
added def inv_monoid_hom
added theorem inv_monoid_hom_apply
modified theorem function.mul_support_div
modified theorem function.mul_support_inv'
modified theorem function.mul_support_inv