Merge branch 'main' of https://github.com/Blackfeather007/Filtered_Ring

Blackfeather007 · Oct 5, 2024 · ec9e77b · ec9e77b
2 parents 55450ce + 15589f5
commit ec9e77b
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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