mathlib3

feat(algebra/ring): generalize mul_ite

#2223

Merged