chore(ring_theory/graded_algebra/basic): remove commutativity require…

…ment (#12208) This wasn't used
leanprover-community · Feb 22, 2022 · 71da192 · 71da192
1 parent f0401b9
commit 71da192
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/ring_theory/graded_algebra/basic.lean b/src/ring_theory/graded_algebra/basic.lean
@@ -42,7 +42,7 @@ open_locale direct_sum big_operators
 section graded_algebra
 
 variables {ι R A : Type*}
-variables [decidable_eq ι] [add_comm_monoid ι] [comm_semiring R] [semiring A] [algebra R A]
+variables [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A]
 variables (𝒜 : ι → submodule R A)
 
 /-- An internally-graded `R`-algebra `A` is one that can be decomposed into a collection