[proofplan] We take any generator matrix $G_0$ of $C$ and transform it by (i) elementary row operations and (ii) column permutations. Row operations replace the basis of $C$ by another basis, so they do not change the code. Column permutations replace $C$ by an equivalent code via a coordinate permutation — this is what produces $C^*$. We first bring $G_0$ to reduced row-echelon form over $\mathbb{F}_2$ using elementary row operations; in reduced row-echelon form, each row has a pivot $1$ with zeros elsewhere in the same column, and pivot columns are a strictly increasing sequence of indices. We then permute the columns so that the $k$ pivot columns become the first $k$ columns: the pivot block becomes $I_k$, and the remaining columns form a $k \times (n-k)$ block $B$. This yields $G = (I_k \mid B)$, the generator matrix of the equivalent code $C^*$. [/proofplan]

[step:Start with an arbitrary generator matrix and record the effect of row operations]By hypothesis $\dim_{\mathbb{F}_2}(C) = k$. Choose any basis $g_1^{(0)}, \ldots, g_k^{(0)}$ of $C$ and stack these as rows to form a generator matrix \begin{align*} G_0 := \begin{pmatrix} g_1^{(0)} \\ \vdots \\ g_k^{(0)} \end{pmatrix} \in \mathbb{F}_2^{k \times n}. \end{align*} The rows of $G_0$ form a basis of $C$. Recall that the elementary row operations over $\mathbb{F}_2$ are: - (R1) swap two rows; - (R2) add one row to another (in $\mathbb{F}_2$, this is the same as subtracting since $-1 = 1$); - (R3) multiply a row by a nonzero scalar (vacuous over $\mathbb{F}_2$ since the only nonzero scalar is $1$). Each operation corresponds to left-multiplication by an invertible $k \times k$ matrix over $\mathbb{F}_2$. If $G_1 = E G_0$ with $E \in \mathrm{GL}_k(\mathbb{F}_2)$, then the rows of $G_1$ are $\mathbb{F}_2$-linear combinations of the rows of $G_0$, and vice versa (using $E^{-1}$). So the rows of $G_1$ span the same subspace as the rows of $G_0$, namely $C$, and the number of linearly independent rows (hence the rank) is preserved. In particular, $G_1$ is also a generator matrix for $C$.[/step]

[guided]Why insist on tracking that row operations preserve $C$? Because the whole proof hinges on alternating two kinds of operations: row operations (which act on the basis of $C$ but leave the code unchanged) and column permutations (which leave the span structure inside $C$ unchanged but permute coordinates, producing an equivalent code $C^*$ rather than $C$ itself). Confusing the two would either break the code or break the "equivalent code" clause. The fact that elementary row operations correspond to left-multiplication by elements of $\mathrm{GL}_k(\mathbb{F}_2)$ is the algebraic expression of "change of basis in the row space": the row space is an invariant of the matrix modulo left-multiplication by invertible matrices.[/guided]

[step:Reduce $G_0$ to row-echelon form via Gaussian elimination]Apply Gaussian elimination to $G_0$, producing a sequence $G_0 \to G_1 \to G_2 \to \cdots$ of matrices where each transition is an elementary row operation. After finitely many steps, we reach a matrix $G_r$ in **row-echelon form**: there exist column indices \begin{align*} 1 \le l(1) < l(2) < \cdots < l(k) \le n, \end{align*} the **pivot columns**, such that for each $i \in \{1, \ldots, k\}$, the $i$-th row of $G_r$ satisfies - $(G_r)_{i, l(i)} = 1$ (pivot entry); - $(G_r)_{i, j} = 0$ for $j < l(i)$ (all entries to the left of the pivot are zero); - $(G_r)_{i', l(i)} = 0$ for all $i' > i$ (no pivot entries below in the same column). The strict inequality $l(1) < l(2) < \cdots < l(k)$ — rather than $\le$ — holds because having two rows with pivots in the same column would force one row to be a multiple of the other after further reduction, contradicting that the $k$ rows remain linearly independent (rank is preserved, by Step 1). By the procedure of Gaussian elimination, all $k$ rows of $G_r$ are nonzero (otherwise the matrix would have rank $< k$, but row operations preserve rank), so each row has a well-defined leading $1$, and these leading positions are the pivot columns $l(1) < \cdots < l(k)$. Next, apply further row operations of type (R2) to clear all entries *above* each pivot: for each pivot column $l(i)$ and each row $i' < i$ with $(G_r)_{i', l(i)} = 1$, add row $i$ to row $i'$. Over $\mathbb{F}_2$, this changes the $(i', l(i))$-entry from $1$ to $0$ and potentially alters entries to the right of $l(i)$ in row $i'$, but does not alter the pivot structure. After finitely many such operations, we obtain a matrix $G_{rr}$ in **reduced row-echelon form**: pivots are at positions $(i, l(i))$ with $1$'s, and every pivot column $l(i)$ has a $1$ in row $i$ and $0$'s in all other rows. Concretely, the pivot columns of $G_{rr}$ are the standard basis columns $e_1, \ldots, e_k \in \mathbb{F}_2^k$ (the $i$-th pivot column being $e_i$), positioned at indices $l(1), \ldots, l(k)$ within the $n$ columns of $G_{rr}$.[/step]

[guided]Gaussian elimination is a standard procedure; the key facts we use are (a) it terminates in finitely many steps, (b) it uses only elementary row operations, and (c) the result is in (reduced) row-echelon form. The slightly non-standard aspect over $\mathbb{F}_2$ is that scaling rows is vacuous — the only nonzero scalar is $1$ — so normalising pivots to $1$ is automatic; they are $1$ from the moment they appear. The strict increase $l(1) < l(2) < \cdots$ is the content of row-echelon form: pivots march strictly to the right as we go down the rows. If two pivots were in the same column, we could subtract one row from the other and reduce the rank, contradicting that all $k$ rows remain independent. Reduced row-echelon form further requires pivots to be the *only* $1$ in their columns, achieved by the back-substitution pass. Reaching reduced row-echelon form sets up the column permutation in the next step: each pivot column is a standard basis column of $\mathbb{F}_2^k$, so permuting them to the front creates the block $I_k$.[/guided]

[step:Permute columns to move pivot columns to the first $k$ positions]Define the permutation $\pi \in S_n$ of $\{1, \ldots, n\}$ by \begin{align*} \pi(i) = l(i) \quad \text{for } i \in \{1, \ldots, k\}, \end{align*} and extend $\pi$ to a bijection on $\{1, \ldots, n\}$ by sending the remaining indices $\{1, \ldots, k\} \setminus \{l(1), \ldots, l(k)\}$... wait — let us restate this carefully. We want a permutation $\pi$ such that applying $\pi$ to the columns of $G_{rr}$ moves the pivot columns at positions $l(1), \ldots, l(k)$ to positions $1, \ldots, k$ respectively, and the remaining $n - k$ columns are placed at positions $k+1, \ldots, n$ in any fixed order. Concretely, let $\{j_1, \ldots, j_{n-k}\} := \{1, \ldots, n\} \setminus \{l(1), \ldots, l(k)\}$ in increasing order, and define the permutation $\sigma \in S_n$ by \begin{align*} \sigma(l(i)) = i \text{ for } i \in \{1, \ldots, k\}, \qquad \sigma(j_t) = k + t \text{ for } t \in \{1, \ldots, n-k\}. \end{align*} Then $\sigma$ permutes the coordinate indices so that the pivot positions go to the front. Let $G^* := G_{rr} P$, where $P \in \mathbb{F}_2^{n \times n}$ is the permutation matrix with $P_{ab} = 1$ iff $\sigma(b) = a$, so that right-multiplication by $P$ rearranges columns of $G_{rr}$: the column at position $\sigma^{-1}(a)$ in $G_{rr}$ becomes the column at position $a$ in $G_{rr} P$. In $G^*$, the first $k$ columns (positions $1, \ldots, k$) are the pivot columns of $G_{rr}$, which are the standard basis vectors $e_1, \ldots, e_k$ of $\mathbb{F}_2^k$. Stacking them gives the identity matrix $I_k$. The remaining $n - k$ columns (positions $k+1, \ldots, n$) form some $k \times (n-k)$ block $B \in \mathbb{F}_2^{k \times (n-k)}$. Hence \begin{align*} G^* = (I_k \mid B). \end{align*} Let $C^* \subseteq \mathbb{F}_2^n$ be the linear code whose generator matrix is $G^*$, i.e.\ the row space of $G^*$. We claim $C^*$ is equivalent to $C$ via the coordinate permutation $\sigma^{-1}$: for any $c \in C$ (written as a row vector), the vector obtained by permuting its entries according to $\sigma$ lies in $C^*$, and vice versa. Explicitly, if $c = \lambda^\top G_{rr}$ for some coefficient vector $\lambda \in \mathbb{F}_2^k$ (using that $G_{rr}$ is also a generator matrix of $C$, by Step 1), then \begin{align*} \lambda^\top G^* = \lambda^\top G_{rr} P = c P \end{align*} is the element of $C^*$ corresponding to $c$, with entries permuted by the column-permutation matrix $P$. Hence $C^* = \{c P : c \in C\}$, which is the image of $C$ under coordinate permutation $\sigma$ (in the sense of the equivalence of codes: permuting the $n$ coordinates by $\sigma$). This exhibits $C^*$ as equivalent to $C$.[/step]

[guided]The column-permutation step is a slight bookkeeping exercise. What we have after Step 2 is a matrix $G_{rr}$ whose pivot columns are the standard basis vectors $e_1, \ldots, e_k$, but sitting at positions $l(1) < l(2) < \cdots < l(k)$ inside the $n$-column matrix — not necessarily at the front. The rest of the columns (the non-pivot columns) sit at the positions $\{1, \ldots, n\} \setminus \{l(1), \ldots, l(k)\}$, carrying arbitrary entries. To bring this to the form $(I_k \mid B)$, we need to permute the columns so that the pivot columns come first in order and the non-pivot columns follow. This is exactly what $\sigma$ does. Column permutation on a generator matrix corresponds to coordinate permutation on the code: if $G$ generates $C$, then $GP$ generates $\{cP : c \in C\}$, which is the code obtained from $C$ by permuting the coordinate positions according to $\sigma$. This is the definition of *equivalent codes* in the sense of this theorem. The dimensions, minimum distances, and all intrinsic invariants of the code are preserved; only the labeling of positions changes.[/guided]

[step:Conclude] By Step 3, $C^*$ is a linear code equivalent to $C$ (via coordinate permutation $\sigma$), with generator matrix $G^* = (I_k \mid B)$ in standard form. This completes the proof. [/step]