chore(algebra/jordan/basic): remove unused imports (leanprover-commun…

…ity#15686) We don't need any linear algebra or the real numbers here
bottine · Jul 30, 2022 · d3e4aed · d3e4aed
1 parent ce251b3
commit d3e4aed
Showing 1 changed file with 1 addition and 3 deletions.
diff --git a/src/algebra/jordan/basic.lean b/src/algebra/jordan/basic.lean
@@ -3,10 +3,8 @@ Copyright (c) 2021 Christopher Hoskin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin
 -/
-import algebra.ring.basic
 import algebra.lie.of_associative
-import data.real.basic
-import linear_algebra.basic
+import algebra.ring.basic
 
 /-!
 # Jordan rings