# Commit 2022-09-21 08:15 9936c3df

View on Github →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 ℕ.