diff --git a/FilteredRing/graded.lean b/FilteredRing/graded.lean
index 1e22c5f..3ec675a 100644
--- a/FilteredRing/graded.lean
+++ b/FilteredRing/graded.lean
@@ -1,6 +1,8 @@
 import FilteredRing.Basic
 
 open AddSubgroup
+open Pointwise
+
 variable {R : Type u} [Ring R]
 
 variable {ι : Type v} [OrderedAddCommMonoid ι] [DecidableEq ι] [PredOrder ι]
@@ -10,6 +12,6 @@ variable (F : ι → AddSubgroup R) [FilteredRing F]
 instance {i : ι}: F (PredOrder.pred i) ≤ F i :=
   FilteredRing.mono (PredOrder.pred i) (PredOrder.pred_le i)
 
-def gradedMap {i : ι} : Module R ((F i) ⧸ (F (PredOrder.pred i)).addSubgroupOf (F i)) := sorry
+def gradedMap {i : ι} := ((F i) ⧸ (F (PredOrder.pred i)).addSubgroupOf (F i))
 
 -- instance : GradedRing (gradedMap F) := sorry