Commit 2021-11-28 22:06 dfa98e0e

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