Mathlib Changelog
v3
Changelog
About
Github
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