Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.closure_induction'

Modification history

2022-01-25 20:59
src/group_theory/subgroup/basic.lean
feat(group_theory/sub{monoid,group}, linear_algebra/basic): remove specialization to subtypes from dependent recursors (#11555) …
Modified subgroup.closure_induction'View on Github →
2020-11-12 14:19
src/group_theory/subgroup.lean
feat(group_theory/sub{monoid,group}): Add `closure_induction'` for subtypes (#4984)
Added subgroup.closure_induction'View on Github →