Commit 2022-01-25 20:59 25d1341b
View on Github →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.