Exterior powers and choice Under the assumption that any vector space has a basis (so under the assumption of the axiom of choice), we can prove the following algebraic statements : 
1) If $\varphi:V\to W$ is an injective linear map between vector spaces, then the exterior powers $\Lambda^k \varphi : \Lambda^k V\to \Lambda^k W$ are injective. (See Corollary 5.9 here)
2) If $v_1,\cdots,v_k$ are linearly independent vectors in a vector space $V$ then $v_1\wedge \cdots\wedge v_k\neq 0$. (See Theorem 7.1 here)
My question is (similar to this question about tensor products) : 
Are those statements (1 and 2) still true without the help of the axiom of choice? Or do they imply a form of choice in some sense ?
 A: As YCor notes in comments, (2) is a special case of (1), so I'll only address (1).
Suppose $\Lambda^k\varphi:\Lambda^kV\to\Lambda^kW$ is not injective, and let $x\neq0$ be in the kernel.
Then $x$ can be written in the form 
$$x=\sum_{i=1}^mv_{i1}\wedge\dots\wedge v_{ik}.$$ 
Let $V'$ be the finite dimensional subspace of $V$ spanned by $\{v_{ij}\mid1\leq i\leq m,1\leq j\leq k\}$, and $\varphi':V'\to W$ the restriction of $\varphi$ to $V'$.
Let 
$$x'=\sum_{i=1}^mv_{i1}\wedge\dots\wedge v_{ik},$$ 
considered as an element of $\Lambda^kV'$. Then $x'\neq0$, since it is sent to $x$ by the map induced by the inclusion of $V’$ into $V$. Also
$$\Lambda^k\varphi'(x')=\Lambda^k\varphi(x)=0,$$
so $x'$ is a nonzero element of the kernel of $\Lambda^k\varphi'$.
Hence we may as well assume that $V$ is finite dimensional.
The fact that $\Lambda^k\varphi(x)=0$ follows from a finite number of the relations defining the exterior power $\Lambda^kW$, involving only finitely many elements of $W$. If we replace $W$ by the finite dimensional subspace $W''$ spanned by the image of $\varphi$ and these finitely many elements, then $\varphi$ induces a map $\varphi'':V\to W''$, and $\Lambda^k\varphi''(x)=0$, since the same relations that implied $\Lambda^k\varphi(x)=0$ in $\Lambda^kW$ also imply that $\Lambda^k\varphi''(x)=0$ in $\Lambda^kW''$.
Hence we can also assume that $W$ is finite dimensional, and what remains is a problem about finite dimensional vector spaces that can easily be answered without choice by choosing bases.
