Underlying indecomposability implies graded indecomposability

theorem MagnitudeConjecture.Graded.FiniteGradedModule.indecomposable_of_underlying {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (X : FiniteGradedModule R) (s : ℤ) (hX : CategoryTheory.Indecomposable X.module) : CategoryTheory.Indecomposable { obj := X, degree := s }

A grading and any shift of it preserve indecomposability of an underlying module.