Commit 2021-10-15 22:57 ea22ce39

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