diff --git a/Physlib.lean b/Physlib.lean
index d9ff07fc0..55a3e6d8b 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -138,6 +138,9 @@ public import Physlib.Mathematics.ForMathlib.SchurTriangulation
 public import Physlib.Mathematics.ForMathlib.Trigonometry.SinSq
 public import Physlib.Mathematics.ForMathlib.Trigonometry.Tanh
 public import Physlib.Mathematics.Groups.SO3.Basic
+public import Physlib.Mathematics.Groups.SpecialUnitary.Adjoint
+public import Physlib.Mathematics.Groups.SpecialUnitary.Algebra
+public import Physlib.Mathematics.Groups.SpecialUnitary.GellMann
 public import Physlib.Mathematics.InnerProductSpace.Adjoint
 public import Physlib.Mathematics.InnerProductSpace.Basic
 public import Physlib.Mathematics.InnerProductSpace.Calculus
diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/Adjoint.lean b/Physlib/Mathematics/Groups/SpecialUnitary/Adjoint.lean
new file mode 100644
index 000000000..f0df996bb
--- /dev/null
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/Adjoint.lean
@@ -0,0 +1,275 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import Physlib.Mathematics.Groups.SpecialUnitary.GellMann
+public import Mathlib.LinearAlgebra.BilinearForm.Properties
+public import Mathlib.RepresentationTheory.Intertwining
+/-!
+# The adjoint representation of `SU(N)`
+
+## i. Overview
+
+The adjoint representation of `SU(N)` acts on the complexified Lie algebra
+`SUAlgebraComplexified N = ℂ ⊗[ℝ] su(N)` as the complexification of the conjugation action
+`X ↦ g X g⁻¹` on `su(N)` (A). The generalized Gell-Mann matrices, a real basis of `su(N)`, give the
+basis `adjBasis N` of the complexified Lie algebra. Sending `z ⊗ X` to the matrix `z X` identifies
+the complexified Lie algebra with the traceless complex matrices (`adjMat`), injectively
+(`adjMat_injective`) and onto (`adjMat_ofTraceless`), and on matrices the adjoint action is
+conjugation (`adjMat_adjRep`). The coordinates in the Gell-Mann basis are the trace pairings
+`tr (λ_a A) / 2`.
+
+In the Gell-Mann basis the adjoint action of `g` has the matrix `adjMatrix g`, with entries
+`tr (λ_a g λ_b g⁻¹) / 2`: real, the Gell-Mann matrices being hermitian, and orthogonal, the matrix
+of `g⁻¹` being the transpose (B).
+
+The trace form `A ⊗ B ↦ tr (A B)` is symmetric and nondegenerate, the trace pairing with a Gell-Mann
+matrix being twice the coordinate, and it is invariant under the adjoint action, so it is the
+contraction `adjContr` of two adjoint indices (C).
+
+## ii. Key results
+
+- `suTensor.adjRep` : the adjoint representation on the complexified Lie algebra.
+- `suTensor.adjMat` : the complexified Lie algebra as traceless complex matrices.
+- `suTensor.adjMatrix` : the matrix of the adjoint action in the Gell-Mann basis.
+- `suTensor.adjMatrix_inv` : the matrix of `g⁻¹` is the transpose of that of `g`.
+- `suTensor.traceForm_nondegenerate` : the trace form is nondegenerate.
+- `suTensor.adjContr` : the contraction of two adjoint indices.
+
+## iii. Table of contents
+
+- A. The adjoint representation on the complexified Lie algebra
+- B. The matrix of the adjoint action
+- C. The trace form and the contraction
+
+-/
+
+@[expose] public section
+
+open Matrix Module TensorProduct
+
+namespace suTensor
+
+/-!
+
+## A. The adjoint representation on the complexified Lie algebra
+
+-/
+
+variable (N : ℕ)
+
+/-- The generalized Gell-Mann basis `1 ⊗ λ_a` of the complexified Lie algebra `ℂ ⊗[ℝ] su(N)`. -/
+noncomputable def adjBasis : Basis (GellMann.Index N) ℂ (SUAlgebraComplexified N) :=
+  GellMann.realBasis.baseChange ℂ
+
+lemma adjBasis_apply (a : GellMann.Index N) :
+    adjBasis N a = (1 : ℂ) ⊗ₜ[ℝ] GellMann.realBasis a :=
+  Module.Basis.baseChange_apply _ _ a
+
+variable {N}
+
+lemma val_inv_mul_val (g : SU N) : (g⁻¹).1 * g.1 = 1 := by
+  rw [← Submonoid.coe_mul, inv_mul_cancel]
+  rfl
+
+lemma val_inv (g : SU N) : (g⁻¹).1 = star g.1 := by
+  have h : g.1 * star g.1 = 1 :=
+    mem_unitaryGroup_iff.mp (mem_specialUnitaryGroup_iff.mp g.2).1
+  calc (g⁻¹).1 = (g⁻¹).1 * (g.1 * star g.1) := by rw [h, Matrix.mul_one]
+    _ = star g.1 := by rw [← Matrix.mul_assoc, val_inv_mul_val, Matrix.one_mul]
+
+/-- The adjoint action `X ↦ g X g†` of `SU(N)` on the real Lie algebra `su(N)`. -/
+noncomputable def realAdjRep : Representation ℝ (SU N) (SUAlgebra N) :=
+  (SUAlgebraOver.conj (R := ℂ)).comp
+    (Submonoid.inclusion specialUnitaryGroup_le_unitaryGroup)
+
+@[simp]
+lemma realAdjRep_val (g : SU N) (X : SUAlgebra N) :
+    (realAdjRep g X).1 = g.1 * X.1 * star g.1 := rfl
+
+variable (N)
+
+/-- The adjoint representation on the complexified Lie algebra: the complexification of the
+  adjoint action `X ↦ g X g⁻¹` on `su(N)`. -/
+noncomputable def adjRep : Representation ℂ (SU N) (SUAlgebraComplexified N) where
+  toFun g := (realAdjRep g).baseChange ℂ
+  map_one' := by
+    rw [map_one]
+    exact LinearMap.baseChange_id
+  map_mul' g h := by
+    rw [map_mul]
+    exact LinearMap.baseChange_comp _ _
+
+/-- The matrix of an element of the complexified Lie algebra, `z ⊗ X ↦ z X`: a traceless complex
+  matrix. -/
+noncomputable def adjMat : SUAlgebraComplexified N →ₗ[ℂ] Matrix (Fin N) (Fin N) ℂ :=
+  (SUAlgebraOver.submodule ℂ N).subtype.liftBaseChange ℂ
+
+variable {N}
+
+@[simp]
+lemma adjMat_tmul (z : ℂ) (X : SUAlgebra N) : adjMat N (z ⊗ₜ X) = z • X.1 := rfl
+
+@[simp]
+lemma adjMat_adjBasis (a : GellMann.Index N) : adjMat N (adjBasis N a) = GellMann.matrix a := by
+  rw [adjBasis_apply, adjMat_tmul, one_smul, GellMann.realBasis_apply_val]
+
+/-- The matrix of an element of the complexified Lie algebra is traceless. -/
+lemma trace_adjMat (A : SUAlgebraComplexified N) : (adjMat N A).trace = 0 := by
+  induction A using TensorProduct.inductionOn with
+  | tmul z X => rw [adjMat_tmul, trace_smul, X.trace_val, smul_zero]
+  | add A B hA hB => rw [map_add, trace_add, hA, hB, add_zero]
+
+/-- The adjoint representation moves the matrix by conjugation. -/
+@[simp]
+lemma adjMat_adjRep (g : SU N) (A : SUAlgebraComplexified N) :
+    adjMat N (adjRep N g A) = g.1 * adjMat N A * (g⁻¹).1 := by
+  induction A using TensorProduct.inductionOn with
+  | tmul z X =>
+    change adjMat N (z ⊗ₜ realAdjRep g X) = _
+    rw [adjMat_tmul, adjMat_tmul, realAdjRep_val, val_inv, Matrix.mul_smul,
+      Matrix.smul_mul]
+  | add A B hA hB => rw [map_add, map_add, hA, hB, map_add, Matrix.mul_add, Matrix.add_mul]
+
+/-- The coordinates in the Gell-Mann basis are read off by the trace form,
+  `A = ∑ (tr (λ_a A) / 2) λ_a`. -/
+lemma adjBasis_repr_apply (A : SUAlgebraComplexified N) (a : GellMann.Index N) :
+    (adjBasis N).repr A a = (GellMann.matrix a * adjMat N A).trace / 2 := by
+  conv_rhs => rw [← (adjBasis N).sum_repr A]
+  simp only [map_sum, map_smul, adjMat_adjBasis, Matrix.mul_sum, Matrix.mul_smul, trace_sum,
+    trace_smul, GellMann.trace_matrix_mul_matrix, smul_eq_mul, mul_ite, mul_zero,
+    Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]
+  ring
+
+/-- An element of the complexified Lie algebra is determined by its matrix. -/
+lemma adjMat_injective : Function.Injective (adjMat N) := fun A B h =>
+  (adjBasis N).ext_elem fun a => by rw [adjBasis_repr_apply, adjBasis_repr_apply, h]
+
+/-- The element of the complexified Lie algebra with a given traceless matrix. -/
+noncomputable def ofTraceless (M : Matrix (Fin N) (Fin N) ℂ) : SUAlgebraComplexified N :=
+  ∑ a, ((GellMann.matrix a * M).trace / 2) • adjBasis N a
+
+/-- Every traceless matrix is the matrix of an element of the complexified Lie algebra. -/
+@[simp]
+lemma adjMat_ofTraceless {M : Matrix (Fin N) (Fin N) ℂ} (hM : M.trace = 0) :
+    adjMat N (ofTraceless M) = M := by
+  have h := congrArg Subtype.val
+    (GellMann.basis.sum_repr (⟨M, hM⟩ : ↥(LinearMap.ker (Matrix.traceLinearMap (Fin N) ℂ ℂ))))
+  simp only [Submodule.coe_sum, Submodule.coe_smul, GellMann.basis_apply_val,
+    GellMann.basis_repr_apply] at h
+  simp only [ofTraceless, map_sum, map_smul, adjMat_adjBasis]
+  exact h
+
+/-!
+
+## B. The matrix of the adjoint action
+
+-/
+
+/-- The matrix of the adjoint action of `g` in the Gell-Mann basis. -/
+noncomputable abbrev adjMatrix (g : SU N) : Matrix (GellMann.Index N) (GellMann.Index N) ℂ :=
+  LinearMap.toMatrix (adjBasis N) (adjBasis N) (adjRep N g)
+
+/-- The entries of the matrix of the adjoint action, `tr (λ_a g λ_b g⁻¹) / 2`. -/
+lemma adjMatrix_apply (g : SU N) (a b : GellMann.Index N) :
+    adjMatrix g a b = (GellMann.matrix a * (g.1 * GellMann.matrix b * (g⁻¹).1)).trace / 2 := by
+  rw [adjMatrix, LinearMap.toMatrix_apply, adjBasis_repr_apply, adjMat_adjRep, adjMat_adjBasis]
+
+/-- The matrix of the adjoint action is real, the Gell-Mann matrices being hermitian. -/
+lemma star_adjMatrix_apply (g : SU N) (a b : GellMann.Index N) :
+    star (adjMatrix g a b) = adjMatrix g a b := by
+  rw [adjMatrix_apply, star_div₀, ← trace_conjTranspose]
+  simp only [conjTranspose_mul, GellMann.conjTranspose_matrix, val_inv, star_eq_conjTranspose,
+    conjTranspose_conjTranspose, Matrix.mul_assoc]
+  rw [show star (2 : ℂ) = 2 by simp, trace_mul_comm g.1]
+  simp only [Matrix.mul_assoc]
+  rw [← Matrix.mul_assoc (GellMann.matrix b), trace_mul_comm]
+  simp only [Matrix.mul_assoc]
+
+/-- The matrix of the adjoint action of `g⁻¹` is the transpose of that of `g`, by the cyclicity
+  of the trace. -/
+lemma adjMatrix_inv (g : SU N) : adjMatrix g⁻¹ = (adjMatrix g)ᵀ := by
+  ext a b
+  rw [transpose_apply, adjMatrix_apply, adjMatrix_apply, inv_inv]
+  congr 1
+  rw [trace_mul_comm]
+  simp only [Matrix.mul_assoc]
+  rw [trace_mul_comm]
+  simp only [Matrix.mul_assoc]
+
+/-- The matrix of the adjoint action of `g⁻¹` times that of `g` is the identity. -/
+lemma adjMatrix_inv_mul (g : SU N) : adjMatrix g⁻¹ * adjMatrix g = 1 := by
+  rw [adjMatrix, adjMatrix, ← LinearMap.toMatrix_mul, ← map_mul, inv_mul_cancel, map_one,
+    LinearMap.toMatrix_one]
+
+/-!
+
+## C. The trace form and the contraction
+
+-/
+
+variable (N)
+
+/-- The trace form `A ⊗ B ↦ tr (A B)` on the complexified Lie algebra. -/
+noncomputable def traceForm : LinearMap.BilinForm ℂ (SUAlgebraComplexified N) :=
+  LinearMap.mk₂ ℂ (fun A B => (adjMat N A * adjMat N B).trace)
+    (fun A A' B => by simp [add_mul, trace_add])
+    (fun a A B => by simp)
+    (fun A B B' => by simp [mul_add, trace_add])
+    (fun a A B => by simp)
+
+@[simp]
+lemma traceForm_apply (A B : SUAlgebraComplexified N) :
+    traceForm N A B = (adjMat N A * adjMat N B).trace := rfl
+
+/-- The trace form is symmetric. -/
+lemma traceForm_isSymm : (traceForm N).IsSymm :=
+  ⟨fun A B => by rw [traceForm_apply, traceForm_apply, trace_mul_comm]⟩
+
+/-- The trace form against a Gell-Mann basis vector is twice the coordinate. -/
+lemma traceForm_adjBasis (A : SUAlgebraComplexified N) (a : GellMann.Index N) :
+    traceForm N A (adjBasis N a) = 2 * (adjBasis N).repr A a := by
+  rw [traceForm_apply, adjMat_adjBasis, adjBasis_repr_apply, trace_mul_comm]
+  ring
+
+/-- An element orthogonal to every element under the trace form vanishes: its coordinates are its
+  trace pairings with the Gell-Mann basis. -/
+lemma traceForm_separatingLeft (A : SUAlgebraComplexified N) (hA : ∀ B, traceForm N A B = 0) :
+    A = 0 :=
+  (adjBasis N).ext_elem fun a => by
+    have h := hA (adjBasis N a)
+    rw [traceForm_adjBasis] at h
+    simpa using h
+
+/-- The trace form is nondegenerate on the complexified Lie algebra. -/
+lemma traceForm_nondegenerate : (traceForm N).Nondegenerate :=
+  ⟨traceForm_separatingLeft N, fun B hB => traceForm_separatingLeft N B fun A => by
+    rw [(traceForm_isSymm N).eq]
+    exact hB A⟩
+
+/-- The contraction of two adjoint indices, the trace form `A ⊗ B ↦ tr (A B)`. -/
+noncomputable def adjContr : ((adjRep N).tprod (adjRep N)).IntertwiningMap
+    (Representation.trivial ℂ (SU N) ℂ) where
+  toLinearMap := TensorProduct.lift (traceForm N)
+  isIntertwining' g := TensorProduct.ext' fun A B => by
+    change (adjMat N (adjRep N g A) * adjMat N (adjRep N g B)).trace
+      = (adjMat N A * adjMat N B).trace
+    rw [adjMat_adjRep, adjMat_adjRep, show g.1 * adjMat N A * (g⁻¹).1 * (g.1 * adjMat N B * (g⁻¹).1)
+        = g.1 * (adjMat N A * adjMat N B) * (g⁻¹).1 by
+      simp only [Matrix.mul_assoc]
+      rw [← Matrix.mul_assoc (g⁻¹).1, val_inv_mul_val, Matrix.one_mul]]
+    rw [Matrix.trace_mul_cycle, val_inv_mul_val, one_mul]
+
+/-- The trace form separates the complexified Lie algebra. -/
+lemma adjContr_flip_injective :
+    Function.Injective (TensorProduct.curry (adjContr N).toLinearMap).flip := fun w w' h => by
+  refine sub_eq_zero.1 ((traceForm_nondegenerate N).2 _ fun x => ?_)
+  have hx := LinearMap.congr_fun h x
+  simp only [LinearMap.flip_apply, TensorProduct.curry_apply] at hx
+  rw [map_sub, sub_eq_zero]
+  exact hx
+
+end suTensor
diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/Algebra.lean b/Physlib/Mathematics/Groups/SpecialUnitary/Algebra.lean
new file mode 100644
index 000000000..489a5397a
--- /dev/null
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/Algebra.lean
@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2026 Jinzheng Li. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jinzheng Li
+-/
+module
+
+public import Mathlib.Algebra.Lie.Basic
+public import Mathlib.Algebra.Star.SelfAdjoint
+public import Mathlib.LinearAlgebra.Matrix.Trace
+public import Mathlib.LinearAlgebra.UnitaryGroup
+public import Mathlib.RepresentationTheory.Basic
+public import Mathlib.Analysis.Complex.Basic
+/-!
+# The Lie algebra `su(n)` over a `*`-algebra
+
+## i. Overview
+
+The Lie algebra of `SU(n)` is the real Lie algebra of traceless hermitian `n × n` matrices,
+with bracket `⁅a, b⁆ = i (a b − b a)` — the factor of `i` keeps the bracket of two hermitian
+matrices hermitian. Nothing in this description depends on the entries being complex
+numbers: it makes sense over any commutative `*`-algebra `R` over `ℂ`, and the two cases the
+theory of jets needs are `R = ℂ` (the Lie algebra itself) and `R` the ring of formal power
+series in the spacetime coordinates (its jets). `SUAlgebraOver R n` is this Lie algebra,
+together with the conjugation action `a ↦ U a U†` of the unitary group of `R`.
+
+Over `R = ℂ` the Lie algebra is real, since `i` times a hermitian matrix is anti-hermitian. Its
+complexification `ℂ ⊗[ℝ] su(n)` is `SUAlgebraComplexified n`, the complex vector space on which
+the adjoint representation of `SU(n)` acts in the complex tensors of `SU(n)`.
+
+## ii. Key results
+
+- `SUAlgebraOver` : the traceless hermitian matrices as a real Lie algebra.
+- `SUAlgebraOver.conj` : the conjugation representation of the unitary group.
+- `SU`, `SUAlgebra` : the group `SU(n)` and its Lie algebra over `ℂ`.
+- `SUAlgebraComplexified` : the complexification of `su(n)`.
+
+## iii. Table of contents
+
+- A. Traceless hermitian matrices
+- B. The conjugation representation
+- C. The bracket
+- D. The group `SU(n)` and the complexification
+
+-/
+
+@[expose] public section
+
+open Matrix
+
+/-!
+
+## A. Traceless hermitian matrices
+
+-/
+
+/-- The submodule of traceless hermitian matrices. -/
+abbrev SUAlgebraOver.submodule (R : Type) [CommRing R] [StarRing R] [Algebra ℝ R]
+    [StarModule ℝ R] (n : ℕ) : Submodule ℝ (Matrix (Fin n) (Fin n) R) :=
+  selfAdjoint.submodule ℝ (Matrix (Fin n) (Fin n) R) ⊓
+    LinearMap.ker (Matrix.traceLinearMap (Fin n) ℝ R)
+
+/-- **The Lie algebra `su(n)` over `R`**: traceless hermitian `n × n` matrices with entries in
+  `R`, a real Lie algebra with bracket `i (a b − b a)`. -/
+abbrev SUAlgebraOver (R : Type) [CommRing R] [StarRing R] [Algebra ℝ R] [StarModule ℝ R]
+    (n : ℕ) : Type :=
+  ↥(SUAlgebraOver.submodule R n)
+
+namespace SUAlgebraOver
+
+variable {R : Type} [CommRing R] [StarRing R] [Algebra ℝ R] [StarModule ℝ R] {n : ℕ}
+
+lemma mem_iff (A : Matrix (Fin n) (Fin n) R) :
+    A ∈ submodule R n ↔ star A = A ∧ A.trace = 0 := Iff.rfl
+
+/-- An element from a traceless hermitian matrix. -/
+def ofMatrix (A : Matrix (Fin n) (Fin n) R) (hA : star A = A) (hT : A.trace = 0) :
+    SUAlgebraOver R n :=
+  ⟨A, hA, hT⟩
+
+@[simp]
+lemma ofMatrix_val (A : Matrix (Fin n) (Fin n) R) (hA : star A = A) (hT : A.trace = 0) :
+    (ofMatrix A hA hT).1 = A := rfl
+
+lemma star_val (a : SUAlgebraOver R n) : star a.1 = a.1 := a.2.1
+
+lemma trace_val (a : SUAlgebraOver R n) : a.1.trace = 0 := a.2.2
+
+@[ext]
+lemma ext {a b : SUAlgebraOver R n} (h : a.1 = b.1) : a = b := Subtype.ext h
+
+/-!
+
+## B. The conjugation representation
+
+-/
+
+/-- **The conjugation representation** of the unitary group on `su(n)`: `a ↦ U a U†`. -/
+noncomputable def conj : Representation ℝ (unitaryGroup (Fin n) R) (SUAlgebraOver R n) where
+  toFun U :=
+    { toFun a := ofMatrix (U.1 * a.1 * star U.1)
+        (by rw [star_mul, star_mul, star_star, a.star_val, mul_assoc])
+        (by
+          rw [Matrix.trace_mul_comm, ← mul_assoc, show star U.1 * U.1 = 1 from
+            (Unitary.mem_iff.mp U.2).1, one_mul, a.trace_val])
+      map_add' a b := Subtype.ext (by simp [mul_add, add_mul])
+      map_smul' r a := Subtype.ext (by simp) }
+  map_one' := LinearMap.ext fun a => Subtype.ext (by simp)
+  map_mul' U V := LinearMap.ext fun a => Subtype.ext (by simp [star_mul, mul_assoc])
+
+@[simp]
+lemma conj_apply_val (U : unitaryGroup (Fin n) R) (a : SUAlgebraOver R n) :
+    (conj U a).1 = U.1 * a.1 * star U.1 := rfl
+
+/-!
+
+## C. The bracket
+
+-/
+
+variable [Algebra ℂ R] [StarModule ℂ R]
+
+/-- The bracket `i (a b − b a)`. -/
+noncomputable instance : Bracket (SUAlgebraOver R n) (SUAlgebraOver R n) where
+  bracket a b := ofMatrix (Complex.I • (a.1 * b.1 - b.1 * a.1))
+    (by
+      rw [star_smul, star_sub, star_mul, star_mul, a.star_val, b.star_val, Complex.star_def,
+        Complex.conj_I, neg_smul, ← smul_neg, neg_sub])
+    (by rw [Matrix.trace_smul, Matrix.trace_sub, Matrix.trace_mul_comm, sub_self, smul_zero])
+
+@[simp]
+lemma bracket_val (a b : SUAlgebraOver R n) :
+    ⁅a, b⁆.1 = Complex.I • (a.1 * b.1 - b.1 * a.1) := rfl
+
+noncomputable instance : LieRing (SUAlgebraOver R n) where
+  add_lie a b c := Subtype.ext (by
+    simp only [bracket_val, Submodule.coe_add, add_mul, mul_add, smul_add, smul_sub]
+    abel)
+  lie_add a b c := Subtype.ext (by
+    simp only [bracket_val, Submodule.coe_add, add_mul, mul_add, smul_add, smul_sub]
+    abel)
+  lie_self a := Subtype.ext (by simp)
+  leibniz_lie a b c := Subtype.ext (by
+    simp only [bracket_val, Submodule.coe_add, mul_smul_comm, smul_mul_assoc, smul_smul,
+      Complex.I_mul_I, smul_sub, mul_sub, sub_mul, mul_assoc]
+    module)
+
+variable [IsScalarTower ℝ ℂ R]
+
+noncomputable instance : LieAlgebra ℝ (SUAlgebraOver R n) where
+  lie_smul r a b := Subtype.ext (by
+    ext i j
+    simp only [bracket_val, Submodule.coe_smul, Matrix.smul_apply, Matrix.sub_apply,
+      Matrix.mul_apply]
+    simp only [Algebra.smul_def, mul_sub, Finset.mul_sum]
+    congr 1 <;> exact Finset.sum_congr rfl fun k _ => by ring)
+
+end SUAlgebraOver
+
+/-!
+
+## D. The group `SU(n)` and the complexification
+
+-/
+
+/-- The group `SU(n)` of special unitary complex `n × n` matrices. -/
+abbrev SU (n : ℕ) : Type := specialUnitaryGroup (Fin n) ℂ
+
+/-- The Lie algebra `su(n)`: traceless hermitian complex `n × n` matrices. -/
+abbrev SUAlgebra (n : ℕ) : Type := SUAlgebraOver ℂ n
+
+open TensorProduct in
+/-- **The complexified Lie algebra `su(n)_ℂ = ℂ ⊗[ℝ] su(n)`**, a complex vector space. -/
+abbrev SUAlgebraComplexified (n : ℕ) : Type := ℂ ⊗[ℝ] SUAlgebraOver ℂ n
diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/GellMann.lean b/Physlib/Mathematics/Groups/SpecialUnitary/GellMann.lean
new file mode 100644
index 000000000..1d9c63dae
--- /dev/null
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/GellMann.lean
@@ -0,0 +1,481 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import Mathlib.Analysis.SpecialFunctions.Pow.Real
+public import Physlib.Mathematics.Groups.SpecialUnitary.Algebra
+/-!
+# The generalized Gell-Mann matrices
+
+## i. Overview
+
+The generalized Gell-Mann matrices are the standard basis of the traceless complex `N × N`
+matrices, the complexified Lie algebra of `SU(N)`, generalizing the Pauli matrices (`N = 2`) and
+the Gell-Mann matrices (`N = 3`). There are `N² - 1` of them, of three kinds:
+
+- for `j < k` the symmetric matrix `E_jk + E_kj`,
+- for `j < k` the antisymmetric matrix `-i E_jk + i E_kj`,
+- for `1 ≤ n ≤ N - 1` the diagonal matrix `√(2 / (n (n + 1))) (E_00 + ⋯ + E_(n-1)(n-1) - n E_nn)`.
+
+They are hermitian and traceless, and orthogonal under the trace form, `tr (λ_a λ_b) = 2 δ_ab`.
+Orthogonality makes them linearly independent, and there are as many as the dimension of the
+traceless matrices, so they form a basis, `GellMann.basis`, whose coordinates are read off by the
+trace form, `GellMann.basis_repr_apply`. Being hermitian they lie in the real Lie algebra `su(N)`
+of traceless hermitian matrices, and there they form a real basis, `GellMann.realBasis`: the
+coordinates `tr (λ_a H) / 2` of a traceless hermitian matrix `H` are real (E).
+
+## ii. Key results
+
+- `GellMann.Index` : the labels of the generalized Gell-Mann matrices.
+- `GellMann.matrix` : the generalized Gell-Mann matrices.
+- `GellMann.trace_matrix_mul_matrix` : `tr (λ_a λ_b) = 2 δ_ab`.
+- `GellMann.basis` : the basis of the traceless matrices they form.
+- `GellMann.realBasis` : the basis of the real Lie algebra `su(N)` they form.
+
+## iii. Table of contents
+
+- A. The matrices
+- B. The diagonal profiles
+- C. Orthogonality
+- D. The basis
+- E. The real basis of `su(N)`
+
+-/
+
+@[expose] public section
+
+open Matrix Module
+
+namespace GellMann
+
+/-!
+
+## A. The matrices
+
+-/
+
+/-- The labels of the generalized Gell-Mann matrices: a pair `j < k` for each symmetric and each
+  antisymmetric matrix, and `l : Fin (N - 1)` for the diagonal matrix of size `n = l + 1`. -/
+abbrev Index (N : ℕ) : Type :=
+  {p : Fin N × Fin N // p.1 < p.2} ⊕ {p : Fin N × Fin N // p.1 < p.2} ⊕ Fin (N - 1)
+
+variable {N : ℕ}
+
+/-- The diagonal profile of size `n = l + 1`: `1` on the first `n` entries, `-n` on the next, and
+  `0` beyond. -/
+def diagProfile (l : Fin (N - 1)) (m : Fin N) : ℂ :=
+  if m.val < l.val + 1 then 1 else if m.val = l.val + 1 then -((l.val + 1 : ℕ) : ℂ) else 0
+
+/-- The normalization `√(2 / (n (n + 1)))` of the diagonal matrix of size `n = l + 1`. -/
+noncomputable def diagNorm (l : Fin (N - 1)) : ℂ :=
+  (Real.sqrt (2 / (((l.val + 1 : ℕ) : ℝ) * ((l.val + 2 : ℕ) : ℝ))) : ℂ)
+
+/-- The generalized Gell-Mann matrices. -/
+noncomputable def matrix : Index N → Matrix (Fin N) (Fin N) ℂ
+  | .inl p => single p.1.1 p.1.2 1 + single p.1.2 p.1.1 1
+  | .inr (.inl p) => single p.1.1 p.1.2 (-Complex.I) + single p.1.2 p.1.1 Complex.I
+  | .inr (.inr l) => diagNorm l • diagonal (diagProfile l)
+
+/-!
+
+## B. The diagonal profiles
+
+-/
+
+/-- The profile as a function of the position, `1` below `n`, `-n` at `n`, `0` above. -/
+private def profile (n m : ℕ) : ℂ := if m < n then 1 else if m = n then -(n : ℂ) else 0
+
+private lemma sum_range_profile {n : ℕ} :
+    ∀ M, n < M → ∑ m ∈ Finset.range M, profile n m = 0 := by
+  intro M hM
+  induction M, hM using Nat.le_induction with
+  | base =>
+    rw [Finset.sum_range_succ, Finset.sum_congr rfl fun m hm => (show profile n m = 1 by
+      simp [profile, Finset.mem_range.1 hm])]
+    simp [profile]
+  | succ M hM ih =>
+    rw [Finset.sum_range_succ, ih]
+    simp [profile, show ¬ M < n by omega, show M ≠ n by omega]
+
+lemma sum_diagProfile (l : Fin (N - 1)) : ∑ m, diagProfile l m = 0 := by
+  change ∑ m : Fin N, profile (l.val + 1) m.val = 0
+  rw [Fin.sum_univ_eq_sum_range (fun m => profile (l.val + 1) m)]
+  exact sum_range_profile N (by omega)
+
+private lemma profile_mul_of_lt {n n' : ℕ} (h : n < n') (m : ℕ) :
+    profile n m * profile n' m = profile n m := by
+  unfold profile
+  by_cases h1 : m < n
+  · simp [h1, show m < n' by omega]
+  · by_cases h2 : m = n
+    · simp [h2, h]
+    · simp [h1, h2]
+
+private lemma profile_mul_self (n m : ℕ) :
+    profile n m * profile n m = (if m < n then 1 else 0) + (if m = n then (n : ℂ) ^ 2 else 0) := by
+  unfold profile
+  by_cases h1 : m < n
+  · simp [h1, show m ≠ n by omega]
+  · by_cases h2 : m = n
+    · simp [h2]
+      ring
+    · simp [h1, h2]
+
+private lemma sum_range_indicator_lt {n : ℕ} :
+    ∀ M, n ≤ M → ∑ m ∈ Finset.range M, (if m < n then (1 : ℂ) else 0) = n := by
+  intro M hM
+  induction M, hM using Nat.le_induction with
+  | base =>
+    rw [Finset.sum_congr rfl (g := fun _ => (1 : ℂ)) fun m hm => by
+      simp [Finset.mem_range.1 hm]]
+    simp
+  | succ M hM ih =>
+    rw [Finset.sum_range_succ, ih]
+    simp [show ¬ M < n by omega]
+
+/-- The diagonal profiles are orthogonal, with `∑ d_l (m)² = n (n + 1)` for `n = l + 1`. -/
+lemma sum_diagProfile_mul (l l' : Fin (N - 1)) :
+    ∑ m, diagProfile l m * diagProfile l' m
+      = if l = l' then ((l.val + 1 : ℕ) : ℂ) * ((l.val + 2 : ℕ) : ℂ) else 0 := by
+  change ∑ m : Fin N, profile (l.val + 1) m.val * profile (l'.val + 1) m.val = _
+  rw [Fin.sum_univ_eq_sum_range (fun m => profile (l.val + 1) m * profile (l'.val + 1) m)]
+  have hl := l.isLt
+  have hl' := l'.isLt
+  rcases lt_trichotomy l l' with h | rfl | h
+  · have h' := Fin.lt_def.1 h
+    simp only [h.ne, ↓reduceIte]
+    simp_rw [profile_mul_of_lt (show l.val + 1 < l'.val + 1 by omega)]
+    exact sum_range_profile N (by omega)
+  · simp only [↓reduceIte]
+    simp_rw [profile_mul_self, Finset.sum_add_distrib,
+      sum_range_indicator_lt (n := l.val + 1) N (by omega), Finset.sum_ite_eq',
+      Finset.mem_range, (show l.val + 1 < N by omega)]
+    simp only [↓reduceIte]
+    push_cast
+    ring
+  · have h' := Fin.lt_def.1 h
+    simp only [h.ne', ↓reduceIte]
+    simp_rw [mul_comm (profile (l.val + 1) _),
+      profile_mul_of_lt (show l'.val + 1 < l.val + 1 by omega)]
+    exact sum_range_profile N (by omega)
+
+/-- The square of the normalization of the diagonal matrix of size `n = l + 1` is
+  `2 / (n (n + 1))`. -/
+lemma diagNorm_mul_self (l : Fin (N - 1)) :
+    diagNorm l * diagNorm l * (((l.val + 1 : ℕ) : ℂ) * ((l.val + 2 : ℕ) : ℂ)) = 2 := by
+  rw [diagNorm, ← Complex.ofReal_mul, Real.mul_self_sqrt (by positivity)]
+  have h1 : ((l.val : ℂ) + 1) ≠ 0 := by norm_cast
+  have h2 : ((l.val : ℂ) + 2) ≠ 0 := by norm_cast
+  push_cast
+  field_simp
+
+/-!
+
+## C. Orthogonality
+
+-/
+
+/-- The trace of a symmetric Gell-Mann matrix against `X`. -/
+lemma trace_matrix_inl_mul (p : {p : Fin N × Fin N // p.1 < p.2}) (X : Matrix (Fin N) (Fin N) ℂ) :
+    (matrix (.inl p) * X).trace = X p.1.2 p.1.1 + X p.1.1 p.1.2 := by
+  simp [matrix, Matrix.add_mul, trace_add, trace_single_mul]
+
+/-- The trace of an antisymmetric Gell-Mann matrix against `X`. -/
+lemma trace_matrix_inr_inl_mul (p : {p : Fin N × Fin N // p.1 < p.2})
+    (X : Matrix (Fin N) (Fin N) ℂ) :
+    (matrix (.inr (.inl p)) * X).trace
+      = -Complex.I * X p.1.2 p.1.1 + Complex.I * X p.1.1 p.1.2 := by
+  simp [matrix, Matrix.add_mul, trace_add, trace_single_mul]
+
+/-- The trace of a diagonal Gell-Mann matrix against `X`. -/
+lemma trace_matrix_inr_inr_mul (l : Fin (N - 1)) (X : Matrix (Fin N) (Fin N) ℂ) :
+    (matrix (.inr (.inr l)) * X).trace = diagNorm l * ∑ m, diagProfile l m * X m m := by
+  simp [matrix, trace, diagonal_mul, Finset.mul_sum]
+
+/-- The entries of a symmetric Gell-Mann matrix. -/
+lemma matrix_inl_apply (p : {p : Fin N × Fin N // p.1 < p.2}) (m n : Fin N) :
+    matrix (.inl p) m n
+      = (if p.1.1 = m ∧ p.1.2 = n then 1 else 0) + (if p.1.2 = m ∧ p.1.1 = n then 1 else 0) := by
+  simp [matrix, single_apply]
+
+/-- The entries of an antisymmetric Gell-Mann matrix. -/
+lemma matrix_inr_inl_apply (p : {p : Fin N × Fin N // p.1 < p.2}) (m n : Fin N) :
+    matrix (.inr (.inl p)) m n = (if p.1.1 = m ∧ p.1.2 = n then -Complex.I else 0)
+      + (if p.1.2 = m ∧ p.1.1 = n then Complex.I else 0) := by
+  simp [matrix, single_apply]
+
+/-- The entries of a diagonal Gell-Mann matrix. -/
+lemma matrix_inr_inr_apply (l : Fin (N - 1)) (m n : Fin N) :
+    matrix (.inr (.inr l)) m n = if m = n then diagNorm l * diagProfile l m else 0 := by
+  simp [matrix, diagonal_apply]
+
+/-- Two ordered pairs `j < k` and `j' < k'` never match crosswise. -/
+private lemma not_cross {j k j' k' : Fin N} (h : j < k) (h' : j' < k') :
+    ¬ (j' = k ∧ k' = j) ∧ ¬ (k' = j ∧ j' = k) :=
+  ⟨by rintro ⟨rfl, rfl⟩; exact lt_asymm h h', by rintro ⟨rfl, rfl⟩; exact lt_asymm h h'⟩
+
+/-- The symmetric Gell-Mann matrices are orthogonal to all others and have norm `2`. -/
+lemma trace_matrix_inl_mul_matrix (p : {p : Fin N × Fin N // p.1 < p.2}) (b : Index N) :
+    (matrix (.inl p) * matrix b).trace = if .inl p = b then 2 else 0 := by
+  obtain ⟨⟨j, k⟩, hjk⟩ := p
+  rcases b with ⟨⟨j', k'⟩, hjk'⟩ | ⟨⟨j', k'⟩, hjk'⟩ | l' <;>
+  simp only [trace_matrix_inl_mul, matrix_inl_apply, matrix_inr_inl_apply,
+    matrix_inr_inr_apply, Sum.inl.injEq, reduceCtorEq, Subtype.mk.injEq, Prod.mk.injEq,
+    ↓reduceIte]
+  · simp only at hjk hjk'
+    obtain ⟨e1, e2⟩ := not_cross hjk hjk'
+    by_cases h : j = j' ∧ k = k'
+    · obtain ⟨rfl, rfl⟩ := h
+      simp only [e1, e2, and_self, ↓reduceIte]
+      ring_nf
+    · have h3 : ¬ (k' = k ∧ j' = j) := fun h' => h ⟨h'.2.symm, h'.1.symm⟩
+      have h4 : ¬ (j' = j ∧ k' = k) := fun h' => h ⟨h'.1.symm, h'.2.symm⟩
+      simp [e1, e2, h3, h4]
+      exact fun h1 h2 => h ⟨h1, h2⟩
+  · simp only at hjk hjk'
+    obtain ⟨e1, e2⟩ := not_cross hjk hjk'
+    by_cases h : j = j' ∧ k = k'
+    · obtain ⟨rfl, rfl⟩ := h
+      simp only [e1, e2, and_self, ↓reduceIte]
+      ring_nf
+    · have h3 : ¬ (k' = k ∧ j' = j) := fun h' => h ⟨h'.2.symm, h'.1.symm⟩
+      have h4 : ¬ (j' = j ∧ k' = k) := fun h' => h ⟨h'.1.symm, h'.2.symm⟩
+      simp [e1, e2, h3, h4]
+  · simp only at hjk
+    simp [hjk.ne, hjk.ne']
+
+/-- The antisymmetric Gell-Mann matrices are orthogonal to all others and have norm `2`. -/
+lemma trace_matrix_inr_inl_mul_matrix (p : {p : Fin N × Fin N // p.1 < p.2}) (b : Index N) :
+    (matrix (.inr (.inl p)) * matrix b).trace = if .inr (.inl p) = b then 2 else 0 := by
+  obtain ⟨⟨j, k⟩, hjk⟩ := p
+  rcases b with ⟨⟨j', k'⟩, hjk'⟩ | ⟨⟨j', k'⟩, hjk'⟩ | l' <;>
+  simp only [trace_matrix_inr_inl_mul, matrix_inl_apply, matrix_inr_inl_apply,
+    matrix_inr_inr_apply, Sum.inl.injEq, Sum.inr.injEq, reduceCtorEq, Subtype.mk.injEq,
+    Prod.mk.injEq, ↓reduceIte]
+  · simp only at hjk hjk'
+    obtain ⟨e1, e2⟩ := not_cross hjk hjk'
+    by_cases h : j = j' ∧ k = k'
+    · obtain ⟨rfl, rfl⟩ := h
+      simp only [e1, e2, and_self, ↓reduceIte]
+      ring_nf
+    · have h3 : ¬ (k' = k ∧ j' = j) := fun h' => h ⟨h'.2.symm, h'.1.symm⟩
+      have h4 : ¬ (j' = j ∧ k' = k) := fun h' => h ⟨h'.1.symm, h'.2.symm⟩
+      simp [e1, e2, h3, h4]
+  · simp only at hjk hjk'
+    obtain ⟨e1, e2⟩ := not_cross hjk hjk'
+    by_cases h : j = j' ∧ k = k'
+    · obtain ⟨rfl, rfl⟩ := h
+      simp only [e1, e2, and_self, ↓reduceIte]
+      ring_nf
+      simp
+    · have h3 : ¬ (k' = k ∧ j' = j) := fun h' => h ⟨h'.2.symm, h'.1.symm⟩
+      have h4 : ¬ (j' = j ∧ k' = k) := fun h' => h ⟨h'.1.symm, h'.2.symm⟩
+      simp [e1, e2, h3, h4]
+      exact fun h1 h2 => h ⟨h1, h2⟩
+  · simp only at hjk
+    simp [hjk.ne, hjk.ne']
+
+/-- The diagonal Gell-Mann matrices are orthogonal to all others and have norm `2`. -/
+lemma trace_matrix_inr_inr_mul_matrix (l : Fin (N - 1)) (b : Index N) :
+    (matrix (.inr (.inr l)) * matrix b).trace = if .inr (.inr l) = b then 2 else 0 := by
+  rcases b with ⟨⟨j', k'⟩, hjk'⟩ | ⟨⟨j', k'⟩, hjk'⟩ | l' <;>
+  simp only [trace_matrix_inr_inr_mul, matrix_inl_apply, matrix_inr_inl_apply,
+    matrix_inr_inr_apply, Sum.inr.injEq, reduceCtorEq, ↓reduceIte]
+  · simp only at hjk'
+    rw [Finset.sum_eq_zero fun x _ => ?_, mul_zero]
+    by_cases h1 : j' = x
+    · subst h1
+      simp [hjk'.ne']
+    · simp [h1]
+  · simp only at hjk'
+    rw [Finset.sum_eq_zero fun x _ => ?_, mul_zero]
+    by_cases h1 : j' = x
+    · subst h1
+      simp [hjk'.ne']
+    · simp [h1]
+  · have hs : ∑ x, diagProfile l x * (diagNorm l' * diagProfile l' x)
+        = diagNorm l' * ∑ x, diagProfile l x * diagProfile l' x := by
+      rw [Finset.mul_sum]
+      exact Finset.sum_congr rfl fun x _ => by ring
+    rw [hs, sum_diagProfile_mul]
+    by_cases h : l = l'
+    · subst h
+      simp only [↓reduceIte]
+      rw [← diagNorm_mul_self l]
+      ring
+    · simp [h]
+
+/-- The generalized Gell-Mann matrices are orthogonal under the trace form:
+  `tr (λ_a λ_b) = 2 δ_ab`. -/
+lemma trace_matrix_mul_matrix (a b : Index N) :
+    (matrix a * matrix b).trace = if a = b then 2 else 0 := by
+  rcases a with p | p | l
+  · exact trace_matrix_inl_mul_matrix p b
+  · exact trace_matrix_inr_inl_mul_matrix p b
+  · exact trace_matrix_inr_inr_mul_matrix l b
+
+/-!
+
+## D. The basis
+
+-/
+
+/-- The generalized Gell-Mann matrices are traceless. -/
+lemma trace_matrix (a : Index N) : (matrix a).trace = 0 := by
+  rcases a with ⟨⟨j, k⟩, hjk⟩ | ⟨⟨j, k⟩, hjk⟩ | l
+  · simp only at hjk
+    rw [matrix, trace_add, trace_single_eq_of_ne (h := hjk.ne),
+      trace_single_eq_of_ne (h := hjk.ne'), add_zero]
+  · simp only at hjk
+    rw [matrix, trace_add, trace_single_eq_of_ne (h := hjk.ne),
+      trace_single_eq_of_ne (h := hjk.ne'), add_zero]
+  · simp [matrix, trace_smul, trace_diagonal, sum_diagProfile]
+
+/-- The generalized Gell-Mann matrices are hermitian. -/
+lemma conjTranspose_matrix (a : Index N) : (matrix a)ᴴ = matrix a := by
+  rcases a with ⟨⟨j, k⟩, hjk⟩ | ⟨⟨j, k⟩, hjk⟩ | l
+  · simp [matrix, conjTranspose_single, add_comm]
+  · simp [matrix, conjTranspose_single, add_comm]
+  · ext m n
+    simp only [matrix, conjTranspose_apply, Matrix.smul_apply, diagonal_apply]
+    by_cases h : m = n
+    · subst h
+      simp [diagNorm, diagProfile]
+      split_ifs <;> simp
+    · simp [h, Ne.symm h]
+
+/-- The generalized Gell-Mann matrices as traceless matrices. -/
+noncomputable def traceless (a : Index N) :
+    ↥(LinearMap.ker (Matrix.traceLinearMap (Fin N) ℂ ℂ)) :=
+  ⟨matrix a, trace_matrix a⟩
+
+/-- The generalized Gell-Mann matrices are linearly independent, by orthogonality. -/
+lemma linearIndependent_traceless : LinearIndependent ℂ (traceless (N := N)) := by
+  rw [Fintype.linearIndependent_iff]
+  intro g hg a
+  have h := congrArg (fun x : ↥(LinearMap.ker (Matrix.traceLinearMap (Fin N) ℂ ℂ)) =>
+    (matrix a * x.1).trace) hg
+  simp only [Submodule.coe_sum, Submodule.coe_smul, traceless, Matrix.mul_sum,
+    Matrix.mul_smul, trace_sum, trace_smul, trace_matrix_mul_matrix, smul_eq_mul, mul_ite,
+    mul_zero, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, ZeroMemClass.coe_zero,
+    trace_zero] at h
+  simpa using h
+
+/-- There are `N² - 1` ordered pairs with `j < k`, counted twice, and `N - 1` diagonal labels:
+  `2 #{j < k} + N = N²`. -/
+lemma two_mul_card_lt_add :
+    2 * Fintype.card {p : Fin N × Fin N // p.1 < p.2} + N = N * N := by
+  have h1 : Fintype.card {p : Fin N × Fin N // p.1 < p.2}
+      = Fintype.card {p : Fin N × Fin N // p.2 < p.1} :=
+    Fintype.card_congr ((Equiv.prodComm _ _).subtypeEquiv fun _ => Iff.rfl)
+  have h2 : Fintype.card {p : Fin N × Fin N // p.1 = p.2} = N := by
+    rw [Fintype.card_subtype, show (Finset.univ.filter fun p : Fin N × Fin N => p.1 = p.2)
+      = Finset.univ.diag by ext; simp [Finset.mem_diag], Finset.diag_card, Finset.card_univ,
+      Fintype.card_fin]
+  have h3 : Fintype.card {p : Fin N × Fin N // p.1 < p.2}
+      + Fintype.card {p : Fin N × Fin N // p.2 < p.1}
+      + Fintype.card {p : Fin N × Fin N // p.1 = p.2} = N * N := by
+    simp only [Fintype.card_subtype, Finset.card_filter, ← Finset.sum_add_distrib]
+    rw [Finset.sum_congr rfl fun p _ => (show ((if p.1 < p.2 then 1 else 0) +
+      (if p.2 < p.1 then 1 else 0) + (if p.1 = p.2 then 1 else 0) : ℕ) = 1 by
+        rcases lt_trichotomy p.1 p.2 with h | h | h
+        · simp [h, lt_asymm h, h.ne]
+        · simp [h]
+        · simp [h, lt_asymm h, h.ne'])]
+    simp
+  omega
+
+/-- The traceless `N × N` matrices have dimension `N² - 1`. -/
+lemma finrank_traceless :
+    finrank ℂ ↥(LinearMap.ker (Matrix.traceLinearMap (Fin N) ℂ ℂ)) = N * N - 1 := by
+  rcases Nat.eq_zero_or_pos N with rfl | hN
+  · exact Nat.le_zero.1 ((Submodule.finrank_le _).trans (by rw [Module.finrank_matrix]; simp))
+  · have hsurj : LinearMap.range (Matrix.traceLinearMap (Fin N) ℂ ℂ) = ⊤ :=
+      LinearMap.range_eq_top.2 fun c => ⟨single ⟨0, hN⟩ ⟨0, hN⟩ c, by simp⟩
+    have h := LinearMap.finrank_range_add_finrank_ker (Matrix.traceLinearMap (Fin N) ℂ ℂ)
+    rw [hsurj, finrank_top, Module.finrank_self, Module.finrank_matrix, Module.finrank_self,
+      Fintype.card_fin] at h
+    omega
+
+lemma card_index : Fintype.card (Index N)
+    = finrank ℂ ↥(LinearMap.ker (Matrix.traceLinearMap (Fin N) ℂ ℂ)) := by
+  have h := two_mul_card_lt_add (N := N)
+  rw [finrank_traceless, Fintype.card_sum, Fintype.card_sum, Fintype.card_fin]
+  rcases Nat.eq_zero_or_pos N with rfl | hN
+  · simp
+  · omega
+
+/-- **The generalized Gell-Mann basis** of the traceless complex `N × N` matrices. -/
+noncomputable def basis : Basis (Index N) ℂ ↥(LinearMap.ker (Matrix.traceLinearMap (Fin N) ℂ ℂ)) :=
+  basisOfLinearIndependentOfCardEqFinrank' _ linearIndependent_traceless card_index
+
+@[simp]
+lemma basis_apply_val (a : Index N) : (basis a).1 = matrix a := by
+  simp [basis, traceless]
+
+/-- The coordinates of a traceless matrix in the Gell-Mann basis are read off by the trace form,
+  `x = ∑ (tr (λ_a x) / 2) λ_a`. -/
+lemma basis_repr_apply (x : ↥(LinearMap.ker (Matrix.traceLinearMap (Fin N) ℂ ℂ))) (a : Index N) :
+    basis.repr x a = (matrix a * x.1).trace / 2 := by
+  conv_rhs => rw [← basis.sum_repr x]
+  simp only [Submodule.coe_sum, Submodule.coe_smul, basis_apply_val, Matrix.mul_sum,
+    Matrix.mul_smul, trace_sum, trace_smul, trace_matrix_mul_matrix, smul_eq_mul, mul_ite,
+    mul_zero, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]
+  ring
+
+/-!
+
+## E. The real basis of `su(N)`
+
+-/
+
+/-- The generalized Gell-Mann matrices as elements of the real Lie algebra `su(N)`. -/
+noncomputable def hermitian (a : Index N) : SUAlgebraOver ℂ N :=
+  SUAlgebraOver.ofMatrix (matrix a) (conjTranspose_matrix a) (trace_matrix a)
+
+/-- The generalized Gell-Mann matrices are linearly independent over the reals. -/
+lemma linearIndependent_hermitian : LinearIndependent ℝ (hermitian (N := N)) := by
+  rw [Fintype.linearIndependent_iff]
+  intro g hg a
+  have h := congrArg (fun x : SUAlgebraOver ℂ N => (matrix a * x.1).trace) hg
+  simp only [Submodule.coe_sum, Submodule.coe_smul, hermitian, SUAlgebraOver.ofMatrix_val,
+    Matrix.mul_sum, Matrix.mul_smul, trace_sum, trace_smul, trace_matrix_mul_matrix, smul_ite,
+    smul_zero, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, ZeroMemClass.coe_zero,
+    Matrix.mul_zero, trace_zero] at h
+  simpa [Complex.real_smul] using h
+
+/-- The trace pairing of two hermitian matrices is real. -/
+lemma trace_mul_ofReal_re {A H : Matrix (Fin N) (Fin N) ℂ} (hA : Aᴴ = A) (hH : Hᴴ = H) :
+    (((A * H).trace.re : ℝ) : ℂ) = (A * H).trace := by
+  refine Complex.conj_eq_iff_re.1 ?_
+  change star (A * H).trace = _
+  rw [← trace_conjTranspose, conjTranspose_mul, hA, hH, trace_mul_comm]
+
+/-- A traceless hermitian matrix is the real combination `∑ (tr (λ_a H) / 2) λ_a` of the
+  generalized Gell-Mann matrices. -/
+lemma eq_sum_re_trace_smul_hermitian (H : SUAlgebraOver ℂ N) :
+    ∑ a, ((matrix a * H.1).trace.re / 2) • hermitian a = H := by
+  refine SUAlgebraOver.ext ?_
+  have hH : H.1 ∈ LinearMap.ker (Matrix.traceLinearMap (Fin N) ℂ ℂ) := H.trace_val
+  have h := congrArg Subtype.val (basis.sum_repr ⟨H.1, hH⟩)
+  simp only [Submodule.coe_sum, Submodule.coe_smul, basis_apply_val, basis_repr_apply] at h
+  simp only [Submodule.coe_sum, Submodule.coe_smul, hermitian, SUAlgebraOver.ofMatrix_val]
+  conv_rhs => rw [← h]
+  refine Finset.sum_congr rfl fun a _ => ?_
+  rw [← Complex.coe_smul, Complex.ofReal_div, trace_mul_ofReal_re (conjTranspose_matrix a)
+    H.star_val]
+  rfl
+
+/-- **The generalized Gell-Mann basis** of the real Lie algebra `su(N)`. -/
+noncomputable def realBasis : Basis (Index N) ℝ (SUAlgebraOver ℂ N) :=
+  Basis.mk linearIndependent_hermitian fun H _ =>
+    (Submodule.mem_span_range_iff_exists_fun ℝ).2 ⟨_, eq_sum_re_trace_smul_hermitian H⟩
+
+@[simp]
+lemma realBasis_apply_val (a : Index N) : (realBasis a).1 = matrix a := by
+  simp [realBasis, hermitian]
+
+end GellMann