# Why does $\mathfrak{o}_L \cong \mathfrak{o}_K^n$ imply that $\mathfrak{o}_L/\pi_k\mathfrak{o}_L$ is a $k_K$ vector space of dimension $n$?

I'm trying to read a proof of the following proposition:

Let $L/K$ be a finite, separable extension of a complete discretely valued field. Then $e(L/K)f(L/K)=[L:K]$.

I'm stuck on the step:

We know $\mathfrak{o}_l \cong \mathfrak{o}_K^n$ as $\mathfrak{o}_K$ modules. So $\mathfrak{o}_L/\pi_K\mathfrak{o}_L$ is a $k_K$-vector space of dimension $n$

where $\pi_K$ is a uniformiser for $K$ (a generator of the maximal ideal of $\mathfrak{o}_K$) and $k_K=\mathfrak{o}_K/(\pi_K\mathfrak{o}_K$.

I see that the dimension must be at most $n$, since the images of the generators of $\mathfrak{o}_L$ in $\mathfrak{o}_L/\pi_K\mathfrak{o}_L$ span $\mathfrak{o}_L/\pi_K\mathfrak{o}_L$, but I don't see why they are still linearly independent.

-

Consider the exact sequence $$0 \to \pi_K\mathfrak{o}_L \cong \pi_K\mathfrak{o}_K^n \to \mathfrak{o}_K^n \to \mathfrak{o}_K^n/\pi_K \mathfrak{o}_K^n \to 0$$
Elements from different summands (remember that this is a direct sum) are linearly independent, and continues to be so after modding out by the maximal ideal. (you can't get any more relations after modding out, because we're considering the quotient as a $\mathfrak{o}_K/\pi_K\mathfrak{o}_K$-vector space, and any relation must come from the maximal ideal).