Uniqueness of shifts of actual graded modules

theorem MagnitudeConjecture.Graded.FiniteGradedModule.shift_eq_of_iso {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (X : FiniteGradedModule R) [Nontrivial ↑X.module] (s t : ℤ) (e : { obj := X, degree := s } ≅ { obj := X, degree := t }) : s = t

Distinct shifts of a nonzero finite-dimensional graded module are not isomorphic by homogeneous degree-preserving maps.