Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submonoid.closure_induction'

Modification history

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