mathlib

ea22ce39 - chore(data/list): move lemmas from data.list.basic that require algebra.group_power to a new file (#9728)

chore(data/list): move lemmas from data.list.basic that require algebra.group_power to a new file (#9728) Hopefully ease the dependencies on anyone importing data.list.basic, if your code broke after this change adding `import data.list.prod_monoid` should fix it. Lemmas moved: - `list.prod_repeat` - `list.sum_repeat` - `list.prod_le_of_forall_le` - `list.sum_le_of_forall_le`