Commit 2022-09-21 08:15 9936c3df

feat(ring_theory/graded_algebra/basic): lemmas about rings graded by canonically ordered monoids (#16083) When the canonically_ordered_add_monoid has_ordered_sub and is cancellative (equivalent to the [contravariant_class ι ι (+) (≤)] assumption):

• (decompose 𝒜 (a * b) n : A) = if i ≤ n then a * decompose 𝒜 b (n - i) else 0 for homogeneous a of degree i
• (decompose 𝒜 (a * b) n : A) = if i ≤ n then (decompose 𝒜 a (n - i)) * b else 0 for homogeneous b of degree i Examples of such monoids include ℕ and finitely supported functions to ℕ.