Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-11 15:17 5f360e3e

View on Github →

feat(group_theory): add group.closure, the subgroup generated by a set

Estimated changes

Modified group_theory/subgroup.lean

added def group.closure

added theorem group.closure_subset

added theorem group.gpowers_eq_closure

added inductive group.in_closure

added theorem group.mem_closure

added theorem group.subset_closure

added theorem is_subgroup.trivial_eq_closure

added theorem mem_gpowers

Modified group_theory/submonoid.lean