This file defines the typeclass graded_algebra 𝒜, for working with an algebra A that is
internally graded by a collection of submodules 𝒜 : ι → submodule R A.
See the docstring of that typeclass for more information.
For now, we do not have internally-graded semirings and internally-graded rings; these can be
represented with 𝒜 : ι → submodule ℕ A and 𝒜 : ι → submodule ℤ A respectively, since all
semirings are ℕ-algebras via algebra_nat, and all rings are ℤ-algebras via algebra_int.
An internally-graded R-algebra A is one that can be decomposed into a collection
of submodule R As indexed by ι such that the canonical map A → ⨁ i, 𝒜 i is bijective and
respects multiplication, i.e. the product of an element of degree i and an element of degree j
is an element of degree i + j.
Note that the fact that A is internally-graded, graded_algebra 𝒜, implies an externally-graded
algebra structure direct_sum.galgebra R (λ i, ↥(𝒜 i)), which in turn makes available an
algebra R (⨁ i, 𝒜 i) instance.
A helper to construct a graded_algebra when the set_like.graded_monoid structure is already
available. This makes the left_inv condition easier to prove, and phrases the right_inv
condition in a way that allows custom @[ext] lemmas to apply.