Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-10 13:13 ec185633

View on Github →

feat(group_theory): add subtype instanes for group and monoid; monoid closure

Estimated changes

Modified group_theory/subgroup.lean

Modified group_theory/submonoid.lean

added def monoid.closure

added inductive monoid.in_closure

added theorem monoid.is_submonoid_closure