Read-back: HefferonLinAlg.change_of_basis_gives_similar_matrices

The declaration asserts the following, for every choice of the data below (all of $K$, $n$, $V$ are implicit arguments, $B$, $C$, $t$ explicit; nothing is fixed in advance):

• an arbitrary field $K$ (no assumption of characteristic, cardinality, or algebraic closure — finite fields and $\mathbb{F}_2$ are included);
• an arbitrary natural number $n$, including $n = 0$;
• an arbitrary type $V$ carrying the structure of an additive commutative group together with a $K$-module structure (over a field this is a $K$-vector space; no finite-dimensionality hypothesis is imposed separately);
• two bases $B$ and $C$ of $V$ over $K$, both indexed by the finite index set $\{0,1,\dots,n-1\}$ — the existence of such a basis is itself a hypothesis, and it forces $\dim_K V = n$; the two bases are unconstrained relative to each other and may be equal, or reorderings/rescalings of each other;
• an arbitrary $K$-linear map $t \colon V \to V$ from $V$ to itself (an endomorphism; the same space on both sides, with no injectivity, surjectivity, or invertibility assumed — $t = 0$ is allowed).

Under exactly these hypotheses, the claim is a pure existence statement (not uniqueness, and with no formula, construction, or characterization of the witness given):

Here the notation must be unfolded carefully. $[t]_{B}^{B}$ denotes the $n \times n$ matrix over $K$ representing $t$ with respect to the basis $B$ used simultaneously as the basis of the source and of the target — i.e. the matrix whose $(i,j)$ entry is the $i$-th coordinate of $t(B_j)$ in the basis $B$, so that $t(B_j) = \sum_{i} \big([t]_B^B\big)_{ij} B_i$; likewise $[t]_{C}^{C}$ uses the basis $C$ on both sides. No mixed-basis matrix $[t]_B^C$ appears anywhere in the statement. The condition "$\det(P)$ is a unit" is stated as invertibility of $\det(P)$ in the ring $K$; since $K$ is a field this is equivalent to $\det(P) \neq 0$, hence to $P$ being an invertible matrix. The symbol $P^{-1}$ is the total matrix-inverse operation (defined for every square matrix, returning the zero matrix when the determinant is not invertible), but under the accompanying unit hypothesis it is the genuine two-sided inverse of $P$. The order and placement of the factors is exactly as written: the $C$-matrix equals $P^{-1}$ on the left, the $B$-matrix in the middle, and $P$ on the right — the statement does not assert the reversed conjugation $P\,[t]_B^B\,P^{-1}$, nor does it assert that $P$ is (or is related in any specified way to) the change-of-basis matrix between $B$ and $C$; any invertible $P$ realizing the displayed equality suffices. Degenerate case: when $n = 0$, $V$ is the zero module, all matrices are the empty $0 \times 0$ matrix, $\det(P) = 1$, and the equality holds trivially, so the statement carries no content in that instance. The declaration is a single implication from the listed hypotheses to this existential conclusion; it makes no claim in the converse direction (it does not say that similarity of two matrices implies they represent a common $t$ in two bases), and it does not claim that every invertible $P$ works.