Matrix multiplication represents composition (Three.IV.2)

Open

hefferon_matrix_of_composition_eq_mul

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

compositionlinear-algebramatrix-representation

Let $g : U \to V$ and $h : V \to W$ be linear maps between finite-dimensional vector spaces over a field $K$ , with bases $B$ , $C$ , $D$ of $U$ , $V$ , $W$ respectively. Then the matrix representing $h \circ g$ with respect to $B$ and $D$ is the product of the matrix representing $h$ with respect to $C$ and $D$ and the matrix representing $g$ with respect to $B$ and $C$ .

Preamble

import Definitions.Def_hefferon_prelude

open Matrix
open HefferonLinAlg

Formal statement

theorem hefferon_matrix_of_composition_eq_mul
    {K : Type*} [Field K] {n m p : ℕ}
    {U V W : Type*}
    [AddCommGroup U] [Module K U] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
    (B : Module.Basis (Fin n) K U) (C : Module.Basis (Fin m) K V)
    (D : Module.Basis (Fin p) K W)
    (g : U →ₗ[K] V) (h : V →ₗ[K] W) :
    LinearMap.toMatrix B D (h ∘ₗ g) =
      LinearMap.toMatrix C D h * LinearMap.toMatrix B C g := by
  sorry

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter Three, Section IV.2, Theorem 2.6, p. 248

View graph