From 15589f526675e9d189b5145516a20535864e7c50 Mon Sep 17 00:00:00 2001
From: yuanyi-350 <kysyy1@126.com>
Date: Sat, 5 Oct 2024 16:28:31 +0800
Subject: [PATCH] Update graded.lean

---
 FilteredRing/graded.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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