Summing projections over an injective finite cover of the nonzero degrees

theorem MagnitudeConjecture.Graded.VectorGrading.sum_projection_of_cover {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] (G : VectorGrading k M) {ν : Type u_3} [Fintype ν] (δ : ν → ℤ) (hδ : Function.Injective δ) (hcover : ∀ (d : ℤ), G.component d ≠ ⊥ → ∃ (q : ν), δ q = d) (x : M) : ∑ q : ν, (G.projection (δ q)) x = x

Only the nonzero degrees need to be covered, so extra zero coordinates cause no difficulty.