Fix imports

leanprover-community · Nov 14, 2022 · 31d24e3 · 31d24e3
1 parent 295018b
commit 31d24e3
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/ring_theory/finiteness.lean b/src/ring_theory/finiteness.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 
+import algebra.algebra.restrict_scalars
 import group_theory.finiteness
 import ring_theory.adjoin.tower
 import ring_theory.mv_polynomial.tower