chore(linear_algebra/basis): missing namespace (#17622)

leanprover-community · Nov 20, 2022 · c832472 · c832472
1 parent 74921b8
commit c832472
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/linear_algebra/basis.lean b/src/linear_algebra/basis.lean
@@ -825,7 +825,7 @@ lemma basis.mem_submodule_iff' {P : submodule R M} (b : basis ι R P) {x : M} :
 b.mem_submodule_iff.trans $ finsupp.equiv_fun_on_fintype.exists_congr_left.trans $ exists_congr $
 λ c, by simp [finsupp.sum_fintype]
 
-lemma coord_equiv_fun_symm (i : ι) (f : ι → R) : b.coord i (b.equiv_fun.symm f) = f i :=
+lemma basis.coord_equiv_fun_symm (i : ι) (f : ι → R) : b.coord i (b.equiv_fun.symm f) = f i :=
 b.coord_repr_symm i (finsupp.equiv_fun_on_fintype.symm f)
 
 end fintype