Commit 2022-03-28 15:03 abaabc8c

chore(algebra/group_power/lemmas): turn [zn]smul lemmas into instances (#13002) This adds new instances such that:

• mul_[zn]smul_assoc is ←smul_mul_assoc
• mul_[zn]smul_left is ←mul_smul_comm This also makes noncomm_ring slightly smarter, and able to handle scalar actions by nat. Thanks to Christopher, this generalizes these instances to non-associative and non-unital rings.