basic): collect together ring lemmas (#11446)

Commit

4 years ago

chore(algebra/group_power/basic): collect together ring lemmas (#11446) This reorders the lemmas so that all the ring and comm_ring lemmas can be put in a single section.

Author

eric-wieser

Parents

df2d70d6

mathlib3 ff19c951 - chore(algebra/group_power/basic): collect together ring lemmas (#11446)

mathlib3
ff19c951 - chore(algebra/group_power/basic): collect together ring lemmas (#11446)