by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
change-of-basislinear-algebramatrixproofwiki
Let R be a ring with unity. Let G and H be free R-modules of finite dimensions n,m>0 respectively. Let ⟨an⟩ and ⟨an′⟩ be ordered bases of G. Let ⟨bm⟩ and ⟨bm′⟩ be ordered bases of H. Let u:G→H be a linear transformation, and let [u;⟨bm⟩,⟨an⟩] be the matrix of u relative to ⟨an⟩ and ⟨bm⟩. Let A=[u;⟨bm⟩,⟨an⟩]B=[u;⟨bm′⟩,⟨an′⟩] Then B=Q−1AP where P is the matrix corresponding to the change of basis from ⟨an⟩ to ⟨an′⟩Q is the matrix corresponding to the change of basis from ⟨bm⟩ to ⟨bm′⟩.