mathlib3

372310d0 - chore(algebra/group/*): attribute copyright properly, correct instance names (#16967)

chore(algebra/group/*): attribute copyright properly, correct instance names (#16967) #16847 copied over the copyright from `algebra.group.basic` without actually attributing things properly. All the material in `algebra.group.commutator` is from #12309 and the material is mostly from #16122 with some dating back from #8564 Also fix `order_dual.has_pow` being additivized as `order_dual.has_nsmul` rather than `order_dual.has_smul`.