Finite-dimensional Hom spaces of graded modules

instance MagnitudeConjecture.Graded.FiniteGradedModule.finiteHom {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (X Y : FiniteGradedModule R) : FiniteDimensional k (X ⟶ Y)

instance MagnitudeConjecture.Graded.FiniteGradedModule.finiteDegreeHom {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (X Y : GradedCategory.DegreeObject homGrading) : FiniteDimensional k (X ⟶ Y)