chore(linear_algebra/finsupp_vector_space): remove leftover pp.univer…

…ses (#3081) See also #1608.
leanprover-community · Jun 15, 2020 · 4843bb1 · 4843bb1
1 parent 758806e
commit 4843bb1
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/src/linear_algebra/finsupp_vector_space.lean b/src/linear_algebra/finsupp_vector_space.lean
@@ -160,7 +160,6 @@ open vector_space
 
 variables {K V : Type u} [field K] [add_comm_group V] [vector_space K V]
 
-set_option pp.universes false
 lemma cardinal_mk_eq_cardinal_mk_field_pow_dim (h : dim K V < cardinal.omega) :
   cardinal.mk V = cardinal.mk K ^ dim K V :=
 begin