Commit 2021-08-01 21:03 b0991037
View on Github →feat(group_theory/subgroup): add subgroup.forall_gpowers
etc (#8470)
- add
subgroup.forall_gpowers
,subgroup.exists_gpowers
,subgroup.forall_mem_gpowers
, andsubgroup.exists_mem_gpowers
; - add their additive counterparts;
- drop some explicit lemmas about
add_subgroup.gmultiples
:to_additive
can generate them now.