Direct sums with shifted gradings

def MagnitudeConjecture.Graded.VectorGrading.shiftedProduct {k : Type u_1} {M : Type u_2} {N : Type u_3} [Field k] [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] [FiniteDimensional k M] [FiniteDimensional k N] (G : VectorGrading k M) (H : VectorGrading k N) (s t : ℤ) : VectorGrading k (M × N)

The componentwise product with degree offsets s and t.

def MagnitudeConjecture.Graded.ModuleGrading.shiftedProduct {k : Type u_1} {M : Type u_2} {N : Type u_3} [Field k] [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] [FiniteDimensional k M] [FiniteDimensional k N] {A : Type u_4} [Ring A] [Algebra k A] [Module A M] [Module A N] {R : VectorGrading k A} (G : ModuleGrading R) (H : ModuleGrading R) (s t : ℤ) : ModuleGrading R

Shifted products retain the graded algebra action.