Reference to basic facts on non-Archimedean local fields I need a reference to the following claims which, I believe, are correct and well known to experts (I am not one of them).
Let $K$ be a non-Archimedean local field. Let  $\mathcal{O}$ be its ring of integers.
Claim 1. Any open compact $\mathcal{O}$-submodule of $K^n$ is finitely generated, free of rank $n$.
Claim 2. Let $E\subset K^n$ be a $K$-linear subspace. Let $M\subset K^n$ be an open compact $\mathcal{O}$-submodule. Then the short exact sequence
$$0\to M\cap E\to M\to M/(M\cap E)\to 0$$
splits.
 A: These are sufficiently elementary that they're not likely to have a proof that is citable.
YCor has answered 1 in the comments but I'll repeat it here for completeness.
Proof of 1: As $M$ is open it contains $\varpi^a \mathcal{O}^n$ for some $a$ ($\varpi$ is a uniformiser) and as $M$ is compact, it lies in $\varpi^b\mathcal{O}^n$ for some $b$. Thus it is finitely generated. It is torsion free as it is a submodule of something torsion-free, so by the classification of modules over a PID, is free. The two inclusions provide lower and upper bounds on the rank, hence the rank is $n$.
Proof of 2: We first prove that the quotient $M/(M\cap E)$ is torsion-free. Suppose $m\in M$ is torsion in $M/(M\cap E)$. Then $xm\in E$ for some $x\in \mathcal{O}$. As $E$ is a vector space, this implies $m\in E$. Therefore $m$ is zero in $M/(M\cap E)$ so this module is torsion-free. As it is finitely generated and torsion free, it is therefore free by the classification of modules over a PID. Therefore the quotient is projective, so the short exact sequence splits.
