ring): provide lemmas about powers in graded monoids (#9631)

Commit

4 years ago

feat(algebra/graded_monoid,algebra/direct_sum/ring): provide lemmas about powers in graded monoids (#9631) The key results are `direct_sum.of_pow` and `graded_monoid.mk_pow`.

Author

eric-wieser

Parents

edf07cfb

mathlib 17d8928b - feat(algebra/graded_monoid,algebra/direct_sum/ring): provide lemmas about powers in graded monoids (#9631)

mathlib
17d8928b - feat(algebra/graded_monoid,algebra/direct_sum/ring): provide lemmas about powers in graded monoids (#9631)