mathlib3

dfa98e0e - chore(algebra/opposites): split out lemmas about rings and groups (#10457)

chore(algebra/opposites): split out lemmas about rings and groups (#10457) All these lemmas are just moved. The advantage of this is that `algebra.opposites` becomes a much lighter-weight import, allowing us to use the `has_mul` and `has_scalar` instance on opposite types earlier in the import hierarchy. It also matches how we structure the instances on `prod` and `pi` types. This follows on from #10383