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](https://kconrad.math.uconn.edu/blurbs/linmultialg/extmod.pdf))


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](https://kconrad.math.uconn.edu/blurbs/linmultialg/extmod.pdf))


My question is (similar to [this](https://mathoverflow.net/questions/325037/axiom-of-choice-and-algebraic-tensor-product) 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 ?



Exterior powers and choice
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.


