Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-18 00:33 a3ac630e

View on Github →

feat(algebra,group_theory): add various closure properties of subgroup and is_group_hom w.r.t gsmul, prod, sum

Estimated changes

added theorem finset.gsmul_sum
added theorem finset.prod_eq_one
added theorem is_add_group_hom_sub
added theorem is_group_hom_inv
added theorem is_group_hom_mul
added theorem gsmul_neg
added theorem gsmul_sub
added theorem is_add_group_hom.gsmul
added theorem is_add_group_hom.smul
added theorem is_add_group_hom_gsmul
added theorem pi.finset_prod_apply
added theorem pi.list_prod_apply
added theorem pi.multiset_prod_apply
modified theorem is_submonoid.list_prod_mem