Commit 2022-01-25 20:59 99608cc6

feat(group_theory/sub{monoid,group}, linear_algebra/basic): add supr_induction for submonoid, add_submonoid, subgroup, add_subgroup, and submodule (#11556) This also adds dependent versions, which match the style of the dependent versions of submodule.span_induction and submonoid.closure_induction in #11555. Primarily it's the group and module versions that are useful here, as they remove the inv and smul obligations that would appear if using closure_induction or span_induction.