Transporting an internal grading through linear coordinates

def MagnitudeConjecture.Graded.VectorGrading.comap {k : Type u_1} {M : Type u_2} {N : Type u_3} [Field k] [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] (G : VectorGrading k N) (e : M ≃ₗ[k] N) : VectorGrading k M

Pull back an internal grading along a linear equivalence.