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.