Commit 2023-05-25 11:24 037038de

feat: port Algebra.Module.GradedModule (#4228)

• In Algebra.DirectSum.Decomposition, a simps was commented because it was causing a recurrence loop. However, one of the lemma that it generates is needed in this file, so I put the simps back (and fixed the loop)
• At the end of the file, the local instance GradedModule.isModule was causing a lot of troubles. (It was in fact marked as a dangerous instance in Mathlib3). I removed it and declared it directly in the only result using it, see this Zulip thread