mathlib3

f1d0841e - feat(ring_theory/graded_algebra/basic): lemmas about rings graded by canonically ordered monoids (#16083)

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 ℕ. Co-authored-by: Junyan Xu <junyanxumath@gmail.com>