Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-12 14:19 34215fc9

View on Github →

feat(group_theory/sub{monoid,group}): Add closure_induction' for subtypes (#4984)

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem subgroup.closure_induction'

Modified src/group_theory/submonoid/operations.lean

added theorem submonoid.closure_induction'