Mathlib Changelog
v3
Changelog
About
Github
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
Modified
algebra/group.lean
Deleted
group_theory/add_subgroup.lean
deleted
def
add_group.closure
deleted
theorem
add_group.closure_subset
deleted
theorem
add_group.gmultiples_eq_closure
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.add_mem_cancel_left
deleted
theorem
is_add_subgroup.add_mem_cancel_right
deleted
def
is_add_subgroup.center
deleted
theorem
is_add_subgroup.gsmul_mem
deleted
theorem
is_add_subgroup.mem_center
deleted
theorem
is_add_subgroup.mem_norm_comm
deleted
theorem
is_add_subgroup.mem_norm_comm_iff
deleted
theorem
is_add_subgroup.mem_trivial
deleted
theorem
is_add_subgroup.neg_mem_iff
deleted
theorem
is_add_subgroup.of_sub
deleted
def
is_add_subgroup.trivial
deleted
theorem
is_add_subgroup.trivial_eq_closure
deleted
theorem
mem_gmultiples
Deleted
group_theory/add_submonoid.lean
deleted
def
add_monoid.closure
deleted
theorem
add_monoid.closure_subset
deleted
theorem
add_monoid.exists_list_of_mem_closure
deleted
inductive
add_monoid.in_closure
deleted
theorem
add_monoid.subset_closure
deleted
theorem
is_add_submonoid.list_sum_mem
deleted
theorem
is_add_submonoid.multiple_subset
deleted
theorem
is_add_submonoid.smul_mem
deleted
def
multiples
Modified
group_theory/subgroup.lean
added
def
add_group.closure
added
theorem
add_group.closure_subset
added
theorem
add_group.gmultiples_eq_closure
added
theorem
add_group.mem_closure
added
theorem
additive.is_add_subgroup_iff
added
theorem
additive.normal_add_subgroup_iff
added
def
gmultiples
modified
theorem
group.subset_closure
added
def
is_add_subgroup.center
added
theorem
is_add_subgroup.gsmul_mem
added
theorem
is_add_subgroup.of_sub
added
def
is_add_subgroup.trivial
modified
theorem
is_subgroup.mem_center
modified
theorem
is_subgroup.mem_norm_comm
modified
theorem
is_subgroup.mem_norm_comm_iff
modified
theorem
is_subgroup.of_div
added
theorem
mem_gmultiples
modified
theorem
mem_gpowers
added
theorem
multiplicative.is_subgroup_iff
added
theorem
multiplicative.normal_subgroup_iff
Modified
group_theory/submonoid.lean
added
def
add_monoid.closure
added
theorem
add_monoid.closure_subset
added
theorem
add_monoid.exists_list_of_mem_closure
added
theorem
add_monoid.subset_closure
added
theorem
additive.is_add_submonoid_iff
added
theorem
is_add_submonoid.multiple_subset
added
theorem
is_add_submonoid.smul_mem
modified
theorem
is_submonoid.pow_mem
added
def
multiples
added
theorem
multiplicative.is_submonoid_iff