chore(ring_theory/polynomial/tower): weaken comm_semiring hypothesis …

…to semiring (#11712) …to semiring
leanprover-community · Jan 29, 2022 · f51d6bf · f51d6bf
1 parent 601ea91
commit f51d6bf
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/ring_theory/polynomial/tower.lean b/src/ring_theory/polynomial/tower.lean
@@ -34,7 +34,7 @@ by rw [polynomial.aeval_def, polynomial.aeval_def, polynomial.eval₂_map, algeb
 end semiring
 
 section comm_semiring
-variables [comm_semiring R] [comm_semiring A] [comm_semiring B]
+variables [comm_semiring R] [comm_semiring A] [semiring B]
 variables [algebra R A] [algebra A B] [algebra R B] [is_scalar_tower R A B]
 
 lemma algebra_map_aeval (x : A) (p : polynomial R) :