From 71da192cb5143862756874f134c3777f562f2f84 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 22 Feb 2022 15:16:21 +0000 Subject: [PATCH] chore(ring_theory/graded_algebra/basic): remove commutativity requirement (#12208) This wasn't used --- src/ring_theory/graded_algebra/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ring_theory/graded_algebra/basic.lean b/src/ring_theory/graded_algebra/basic.lean index fae06aaac6fc8..f9aff93e9ec58 100644 --- 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