Eric Wieser

> I'm a bit confused: is the `has_pow` instance changing (up to defeq) or not? Yes; the new definition is "elementwise power on the cauchy sequence" > If so then...

I can restore the old has_pow then; it's the has_smul defeq change that's more useful anyway.

Apologies, my ongoing dimension refactor has created a few more conflicts, hopefully minor.

CI is failing

That commit is a commit that I made in #8274 (hence it showing me as the author), it was me pulling in the latest changes from bors

I've pushed an update to this to resolve the merge conflicts and remove the obviously duplicate lemmas. There's still some less trivial duplication between the `mem_supr` and `dfinsupp` lemmas which...

@acxxa, I think #9202 contains most of the interesting proofs from this PR; all that's left is the `decomposition` API. Did you have a motivation for bundling `factors` rather than...

Note that [`graded_algebra`](https://leanprover-community.github.io/mathlib_docs/ring_theory/graded_algebra/basic.html#graded_algebra) is now merged. I think probably to make it play well with this PR, we want to change it's definition from ```lean class graded_algebra extends set_like.graded_monoid 𝒜...

This feels like it likely overlaps with the representation theory stuff too

> I just have some formatting suggestions. > > @eric-wieser I think a point in having `modneq` as a reducible definition is that it gives a way to have `modneq`-specific...