mathlib3

0ca77959 - feat(algebra/algebra/operations): remove two hypotheses from `submodule.mul_induction_on` (#11533)

feat(algebra/algebra/operations): remove two hypotheses from `submodule.mul_induction_on` (#11533) `h0 : C 0` followed trivially from `hm 0 _ 0 _`. `hs : ∀ (r : R) x, C x → C (r • x)` follows nontrivially from an analogy to the `add_submonoid` case. This also adds: * a `pow_induction` variant. * primed variants for when the motive depends on the proof term (such as the proof field in a subtype)