Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-10 07:04 0f42b279

View on Github →

feat(group_theory/submonoid,subgroup): merge with add_* versions

Estimated changes

deleted def add_group.closure
deleted theorem add_group.closure_subset
deleted inductive add_group.in_closure
deleted theorem add_group.mem_closure
deleted theorem add_group.subset_closure
deleted def gmultiples
deleted theorem injective_add
deleted theorem is_add_subgroup.gsmul_mem
deleted theorem is_add_subgroup.of_sub
deleted theorem mem_gmultiples
deleted def add_monoid.closure
deleted theorem add_monoid.closure_subset
deleted inductive add_monoid.in_closure
deleted theorem add_monoid.subset_closure
deleted theorem is_add_submonoid.smul_mem
deleted def multiples
added theorem add_group.mem_closure
added def gmultiples
modified theorem group.subset_closure
added theorem is_add_subgroup.of_sub
modified theorem is_subgroup.mem_center
modified theorem is_subgroup.mem_norm_comm
modified theorem is_subgroup.of_div
added theorem mem_gmultiples
modified theorem mem_gpowers
modified theorem is_submonoid.pow_mem
added def multiples