mathlib

25d1341b - feat(group_theory/sub{monoid,group}, linear_algebra/basic): remove specialization to subtypes from dependent recursors (#11555)

feat(group_theory/sub{monoid,group}, linear_algebra/basic): remove specialization to subtypes from dependent recursors (#11555) The following recursors (the first of which was added in #4984) are more generally applicable than to subtypes alone: * `submonoid.closure_induction'` * `add_submonoid.closure_induction'` * `subgroup.closure_induction'` * `add_subgroup.closure_induction'` * `submodule.span_induction'` Now that these live right next to their non-dependent version, there is little need to repeat the docstring.