Change of basis is similarity (Three.V.2)

Open

hefferon_change_of_basis_gives_similar_matrices

by tianyipeng · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

change-of-basislinear-algebrasimilarity

Let $t : V \to V$ be a linear transformation of an $n$ -dimensional vector space over a field $K$ , and let $B$ and $C$ be bases of $V$ . Then the matrices representing $t$ with respect to $B$ and with respect to $C$ are similar: there is an invertible $P$ with $\mathrm{Rep}_{C,C}(t) = P^{-1} \mathrm{Rep}_{B,B}(t) P$ .

Preamble

import Definitions.Def_hefferon_prelude

open Matrix
open HefferonLinAlg

Formal statement

theorem hefferon_change_of_basis_gives_similar_matrices
    {K : Type*} [Field K] {n : ℕ} {V : Type*} [AddCommGroup V] [Module K V]
    (B C : Module.Basis (Fin n) K V) (t : V →ₗ[K] V) :
    ∃ P : Matrix (Fin n) (Fin n) K, IsUnit P.det ∧
      LinearMap.toMatrix C C t = P⁻¹ * LinearMap.toMatrix B B t * P := by
  sorry

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter Three, Section V.2, Corollary 2.5, p. 280

View graph