mathlib3

abaabc8c - chore(algebra/group_power/lemmas): turn `[zn]smul` lemmas into instances (#13002)

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. Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>