Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-10 07:04 1d5dd0d4

View on Github →

feat(group_theory): adding add_subgroup and add_submonoid

Estimated changes

Created group_theory/add_subgroup.lean

added def add_group.closure

added theorem add_group.closure_subset

added theorem add_group.gmultiples_eq_closure

added inductive add_group.in_closure

added theorem add_group.mem_closure

added theorem add_group.subset_closure

added def gmultiples

added theorem injective_add

added theorem is_add_subgroup.add_mem_cancel_left

added theorem is_add_subgroup.add_mem_cancel_right

added def is_add_subgroup.center

added theorem is_add_subgroup.gsmul_mem

added theorem is_add_subgroup.mem_center

added theorem is_add_subgroup.mem_norm_comm

added theorem is_add_subgroup.mem_norm_comm_iff

added theorem is_add_subgroup.mem_trivial

added theorem is_add_subgroup.neg_mem_iff

added theorem is_add_subgroup.of_sub

added def is_add_subgroup.trivial

added theorem is_add_subgroup.trivial_eq_closure

added theorem mem_gmultiples

Created group_theory/add_submonoid.lean

added def add_monoid.closure

added theorem add_monoid.closure_subset

added theorem add_monoid.exists_list_of_mem_closure

added inductive add_monoid.in_closure

added theorem add_monoid.subset_closure

added theorem is_add_submonoid.list_sum_mem

added theorem is_add_submonoid.multiple_subset

added theorem is_add_submonoid.smul_mem

added def multiples