mathlib

79c5de9a - feat(ring_theory/ideal/operations): remove unneeded assumptions from `smul_induction_on` (#12193)