Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-30 16:32 065f083b

View on Github →

feat(group_theory): monoid / group closure of union

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem add_group.closure_eq_mclosure

added theorem add_group.closure_mono

added theorem add_group.exists_list_of_mem_closure

added theorem add_group.mclosure_inv_subset

added theorem add_group.mclosure_subset

added theorem add_group.mem_closure_union_iff

added theorem group.closure_eq_mclosure

added theorem group.closure_mono

added theorem group.exists_list_of_mem_closure

added theorem group.mclosure_inv_subset

added theorem group.mclosure_subset

added theorem group.mem_closure_union_iff

Modified src/group_theory/submonoid.lean

added theorem add_monoid.closure_mono

added theorem add_monoid.mem_closure_union_iff

added theorem monoid.closure_mono

added theorem monoid.mem_closure_union_iff