mathlib3

9540b8cf - feat(ring_theory/ideals/operations): add induction lemma (#16945)

feat(ring_theory/ideals/operations): add induction lemma (#16945) Add `submodule.smul_induction_on'` which is a dependent version of `submodule.smul_induction_on` Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>