1. Physlib
  2. Relativity
  3. PauliMatrices
  4. SelfAdjoint
Imports
/- Copyright (c) 2024 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.Relativity.PauliMatrices.Basic public import Physlib.Relativity.MinkowskiMatrix

Interaction of Pauli matrices with self-adjoint matrices

@[expose] public section

The trace of a pauli-matrix multiplied by a self-adjoint 2×2 matrix is real.

All goals completed! 🐙

Two 2×2 self-adjoint matrices are equal if the (complex) traces of each matrix multiplied by each of the Pauli-matrices are equal.

A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))B:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))h0:(σ (Sum.inl 0) * !![↑A 0 0, ↑A 0 1; ↑A 1 0, ↑A 1 1]).trace = (σ (Sum.inl 0) * !![↑B 0 0, ↑B 0 1; ↑B 1 0, ↑B 1 1]).traceh1:(σ (Sum.inr 0) * !![↑A 0 0, ↑A 0 1; ↑A 1 0, ↑A 1 1]).trace = (σ (Sum.inr 0) * !![↑B 0 0, ↑B 0 1; ↑B 1 0, ↑B 1 1]).traceh2:(σ (Sum.inr 1) * !![↑A 0 0, ↑A 0 1; ↑A 1 0, ↑A 1 1]).trace = (σ (Sum.inr 1) * !![↑B 0 0, ↑B 0 1; ↑B 1 0, ↑B 1 1]).traceh3:(σ (Sum.inr 2) * !![↑A 0 0, ↑A 0 1; ↑A 1 0, ↑A 1 1]).trace = (σ (Sum.inr 2) * !![↑B 0 0, ↑B 0 1; ↑B 1 0, ↑B 1 1]).tracei:Fin 2j:Fin 2⊢ ↑A i j = ↑B i j A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))B:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))h1:(σ (Sum.inr 0) * !![↑A 0 0, ↑A 0 1; ↑A 1 0, ↑A 1 1]).trace = (σ (Sum.inr 0) * !![↑B 0 0, ↑B 0 1; ↑B 1 0, ↑B 1 1]).traceh2:(σ (Sum.inr 1) * !![↑A 0 0, ↑A 0 1; ↑A 1 0, ↑A 1 1]).trace = (σ (Sum.inr 1) * !![↑B 0 0, ↑B 0 1; ↑B 1 0, ↑B 1 1]).traceh3:(σ (Sum.inr 2) * !![↑A 0 0, ↑A 0 1; ↑A 1 0, ↑A 1 1]).trace = (σ (Sum.inr 2) * !![↑B 0 0, ↑B 0 1; ↑B 1 0, ↑B 1 1]).tracei:Fin 2j:Fin 2h0:↑A 0 0 + ↑A 1 1 = ↑B 0 0 + ↑B 1 1⊢ ↑A i j = ↑B i j A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))B:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))h2:(σ (Sum.inr 1) * !![↑A 0 0, ↑A 0 1; ↑A 1 0, ↑A 1 1]).trace = (σ (Sum.inr 1) * !![↑B 0 0, ↑B 0 1; ↑B 1 0, ↑B 1 1]).traceh3:(σ (Sum.inr 2) * !![↑A 0 0, ↑A 0 1; ↑A 1 0, ↑A 1 1]).trace = (σ (Sum.inr 2) * !![↑B 0 0, ↑B 0 1; ↑B 1 0, ↑B 1 1]).tracei:Fin 2j:Fin 2h0:↑A 0 0 + ↑A 1 1 = ↑B 0 0 + ↑B 1 1h1:↑A 1 0 + ↑A 0 1 = ↑B 1 0 + ↑B 0 1⊢ ↑A i j = ↑B i j A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))B:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))h3:(σ (Sum.inr 2) * !![↑A 0 0, ↑A 0 1; ↑A 1 0, ↑A 1 1]).trace = (σ (Sum.inr 2) * !![↑B 0 0, ↑B 0 1; ↑B 1 0, ↑B 1 1]).tracei:Fin 2j:Fin 2h0:↑A 0 0 + ↑A 1 1 = ↑B 0 0 + ↑B 1 1h1:↑A 1 0 + ↑A 0 1 = ↑B 1 0 + ↑B 0 1h2:-(I * ↑A 1 0) + I * ↑A 0 1 = -(I * ↑B 1 0) + I * ↑B 0 1⊢ ↑A i j = ↑B i j A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))B:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))i:Fin 2j:Fin 2h0:↑A 0 0 + ↑A 1 1 = ↑B 0 0 + ↑B 1 1h1:↑A 1 0 + ↑A 0 1 = ↑B 1 0 + ↑B 0 1h2:-(I * ↑A 1 0) + I * ↑A 0 1 = -(I * ↑B 1 0) + I * ↑B 0 1h3:↑A 0 0 + -↑A 1 1 = ↑B 0 0 + -↑B 1 1⊢ ↑A i j = ↑B i j match i, j with A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))B:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))i:Fin 2j:Fin 2h0:↑A 0 0 + ↑A 1 1 = ↑B 0 0 + ↑B 1 1h1:↑A 1 0 + ↑A 0 1 = ↑B 1 0 + ↑B 0 1h2:-(I * ↑A 1 0) + I * ↑A 0 1 = -(I * ↑B 1 0) + I * ↑B 0 1h3:↑A 0 0 + -↑A 1 1 = ↑B 0 0 + -↑B 1 1⊢ ↑A 0 0 = ↑B 0 0 linear_combination (norm := All goals completed! 🐙) (h0 + h3) / 2 A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))B:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))i:Fin 2j:Fin 2h0:↑A 0 0 + ↑A 1 1 = ↑B 0 0 + ↑B 1 1h1:↑A 1 0 + ↑A 0 1 = ↑B 1 0 + ↑B 0 1h2:-(I * ↑A 1 0) + I * ↑A 0 1 = -(I * ↑B 1 0) + I * ↑B 0 1h3:↑A 0 0 + -↑A 1 1 = ↑B 0 0 + -↑B 1 1⊢ ↑A 0 1 = ↑B 0 1 linear_combination (norm := A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))B:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))i:Fin 2j:Fin 2h0:↑A 0 0 + ↑A 1 1 = ↑B 0 0 + ↑B 1 1h1:↑A 1 0 + ↑A 0 1 = ↑B 1 0 + ↑B 0 1h2:-(I * ↑A 1 0) + I * ↑A 0 1 = -(I * ↑B 1 0) + I * ↑B 0 1h3:↑A 0 0 + -↑A 1 1 = ↑B 0 0 + -↑B 1 1⊢ ↑A 0 1 * (1 / 2) + ↑A 0 1 * I ^ 2 * (1 / 2) + ↑B 1 0 * (1 / 2) + ↑B 1 0 * I ^ 2 * (1 / 2) + ↑B 0 1 * (-1 / 2) + ↑B 0 1 * I ^ 2 * (-1 / 2) + I ^ 2 * ↑A 1 0 * (-1 / 2) + ↑A 1 0 * (-1 / 2) = 0) (h1 - I * h2) / 2 All goals completed! 🐙 A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))B:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))i:Fin 2j:Fin 2h0:↑A 0 0 + ↑A 1 1 = ↑B 0 0 + ↑B 1 1h1:↑A 1 0 + ↑A 0 1 = ↑B 1 0 + ↑B 0 1h2:-(I * ↑A 1 0) + I * ↑A 0 1 = -(I * ↑B 1 0) + I * ↑B 0 1h3:↑A 0 0 + -↑A 1 1 = ↑B 0 0 + -↑B 1 1⊢ ↑A 1 0 = ↑B 1 0 linear_combination (norm := A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))B:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))i:Fin 2j:Fin 2h0:↑A 0 0 + ↑A 1 1 = ↑B 0 0 + ↑B 1 1h1:↑A 1 0 + ↑A 0 1 = ↑B 1 0 + ↑B 0 1h2:-(I * ↑A 1 0) + I * ↑A 0 1 = -(I * ↑B 1 0) + I * ↑B 0 1h3:↑A 0 0 + -↑A 1 1 = ↑B 0 0 + -↑B 1 1⊢ ↑A 1 0 * (1 / 2) + ↑A 1 0 * I ^ 2 * (1 / 2) + ↑B 1 0 * (-1 / 2) + ↑B 1 0 * I ^ 2 * (-1 / 2) + ↑B 0 1 * (1 / 2) + ↑B 0 1 * I ^ 2 * (1 / 2) + I ^ 2 * ↑A 0 1 * (-1 / 2) + ↑A 0 1 * (-1 / 2) = 0) (h1 + I * h2) / 2 All goals completed! 🐙 A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))B:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))i:Fin 2j:Fin 2h0:↑A 0 0 + ↑A 1 1 = ↑B 0 0 + ↑B 1 1h1:↑A 1 0 + ↑A 0 1 = ↑B 1 0 + ↑B 0 1h2:-(I * ↑A 1 0) + I * ↑A 0 1 = -(I * ↑B 1 0) + I * ↑B 0 1h3:↑A 0 0 + -↑A 1 1 = ↑B 0 0 + -↑B 1 1⊢ ↑A 1 1 = ↑B 1 1 linear_combination (norm := All goals completed! 🐙) (h0 - h3) / 2

Two 2×2 self-adjoint matrices are equal if the real traces of each matrix multiplied by each of the Pauli-matrices are equal.

A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))B:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))h0:(σ (Sum.inl 0) * ↑A).trace.re = (σ (Sum.inl 0) * ↑B).trace.reh1:(σ (Sum.inr 0) * ↑A).trace.re = (σ (Sum.inr 0) * ↑B).trace.reh2:(σ (Sum.inr 1) * ↑A).trace.re = (σ (Sum.inr 1) * ↑B).trace.reh3:(σ (Sum.inr 2) * ↑A).trace.re = (σ (Sum.inr 2) * ↑B).trace.reh0':(σ (Sum.inl 0) * ↑A).trace = (σ (Sum.inl 0) * ↑B).traceh1':(σ (Sum.inr 0) * ↑A).trace = (σ (Sum.inr 0) * ↑B).traceh2':(σ (Sum.inr 1) * ↑A).trace = (σ (Sum.inr 1) * ↑B).traceh3':(σ (Sum.inr 2) * ↑A).trace = (σ (Sum.inr 2) * ↑B).trace⊢ A = B All goals completed! 🐙

An auxiliary function which on i : Fin 1 ⊕ Fin 3 returns the corresponding Pauli-matrix as a self-adjoint matrix.

def pauliSelfAdjoint (i : Fin 1 ⊕ Fin 3) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) := ⟨pauliMatrix i, pauliMatrix_selfAdjoint i⟩

The Pauli matrices are linearly independent.

g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • pauliSelfAdjoint (Sum.inl 0) + (g (Sum.inr 0) • pauliSelfAdjoint (Sum.inr 0) + g (Sum.inr 1) • pauliSelfAdjoint (Sum.inr 1) + g (Sum.inr 2) • pauliSelfAdjoint (Sum.inr 2)) = 0⊢ ∀ (i : Fin 1 ⊕ Fin 3), g i = 0 g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), ⋯⟩ + (g (Sum.inr 0) • ⟨σ (Sum.inr 0), ⋯⟩ + g (Sum.inr 1) • ⟨σ (Sum.inr 1), ⋯⟩ + g (Sum.inr 2) • ⟨σ (Sum.inr 2), ⋯⟩) = 0⊢ ∀ (i : Fin 1 ⊕ Fin 3), g i = 0 g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), ⋯⟩ + (g (Sum.inr 0) • ⟨σ (Sum.inr 0), ⋯⟩ + g (Sum.inr 1) • ⟨σ (Sum.inr 1), ⋯⟩ + g (Sum.inr 2) • ⟨σ (Sum.inr 2), ⋯⟩) = 0i:Fin 1 ⊕ Fin 3⊢ g i = 0 g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), ⋯⟩ + (g (Sum.inr 0) • ⟨σ (Sum.inr 0), ⋯⟩ + g (Sum.inr 1) • ⟨σ (Sum.inr 1), ⋯⟩ + g (Sum.inr 2) • ⟨σ (Sum.inr 2), ⋯⟩) = 0i:Fin 1 ⊕ Fin 3h1:(σ i * ↑(g (Sum.inl 0) • ⟨σ (Sum.inl 0), ⋯⟩ + (g (Sum.inr 0) • ⟨σ (Sum.inr 0), ⋯⟩ + g (Sum.inr 1) • ⟨σ (Sum.inr 1), ⋯⟩ + g (Sum.inr 2) • ⟨σ (Sum.inr 2), ⋯⟩))).trace = (σ i * ↑0).trace⊢ g i = 0 g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), ⋯⟩ + (g (Sum.inr 0) • ⟨σ (Sum.inr 0), ⋯⟩ + g (Sum.inr 1) • ⟨σ (Sum.inr 1), ⋯⟩ + g (Sum.inr 2) • ⟨σ (Sum.inr 2), ⋯⟩) = 0i:Fin 1 ⊕ Fin 3h1:g (Sum.inl 0) • (σ i * σ (Sum.inl 0)).trace + (g (Sum.inr 0) • (σ i * σ (Sum.inr 0)).trace + g (Sum.inr 1) • (σ i * σ (Sum.inr 1)).trace + g (Sum.inr 2) • (σ i * σ (Sum.inr 2)).trace) = 0⊢ g i = 0 g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), ⋯⟩ + (g (Sum.inr 0) • ⟨σ (Sum.inr 0), ⋯⟩ + g (Sum.inr 1) • ⟨σ (Sum.inr 1), ⋯⟩ + g (Sum.inr 2) • ⟨σ (Sum.inr 2), ⋯⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inl 0)).trace + (g (Sum.inr 0) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 0)).trace + g (Sum.inr 1) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 1)).trace + g (Sum.inr 2) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 2)).trace) = 0⊢ g (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) = 0g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), ⋯⟩ + (g (Sum.inr 0) • ⟨σ (Sum.inr 0), ⋯⟩ + g (Sum.inr 1) • ⟨σ (Sum.inr 1), ⋯⟩ + g (Sum.inr 2) • ⟨σ (Sum.inr 2), ⋯⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inl 0)).trace + (g (Sum.inr 0) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 0)).trace + g (Sum.inr 1) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 1)).trace + g (Sum.inr 2) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 2)).trace) = 0⊢ g (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) = 0g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), ⋯⟩ + (g (Sum.inr 0) • ⟨σ (Sum.inr 0), ⋯⟩ + g (Sum.inr 1) • ⟨σ (Sum.inr 1), ⋯⟩ + g (Sum.inr 2) • ⟨σ (Sum.inr 2), ⋯⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inl 0)).trace + (g (Sum.inr 0) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inr 0)).trace + g (Sum.inr 1) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inr 1)).trace + g (Sum.inr 2) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inr 2)).trace) = 0⊢ g (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) = 0g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), ⋯⟩ + (g (Sum.inr 0) • ⟨σ (Sum.inr 0), ⋯⟩ + g (Sum.inr 1) • ⟨σ (Sum.inr 1), ⋯⟩ + g (Sum.inr 2) • ⟨σ (Sum.inr 2), ⋯⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inl 0)).trace + (g (Sum.inr 0) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inr 0)).trace + g (Sum.inr 1) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inr 1)).trace + g (Sum.inr 2) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inr 2)).trace) = 0⊢ g (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) = 0 g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), ⋯⟩ + (g (Sum.inr 0) • ⟨σ (Sum.inr 0), ⋯⟩ + g (Sum.inr 1) • ⟨σ (Sum.inr 1), ⋯⟩ + g (Sum.inr 2) • ⟨σ (Sum.inr 2), ⋯⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inl 0)).trace + (g (Sum.inr 0) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 0)).trace + g (Sum.inr 1) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 1)).trace + g (Sum.inr 2) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 2)).trace) = 0⊢ g (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) = 0g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), ⋯⟩ + (g (Sum.inr 0) • ⟨σ (Sum.inr 0), ⋯⟩ + g (Sum.inr 1) • ⟨σ (Sum.inr 1), ⋯⟩ + g (Sum.inr 2) • ⟨σ (Sum.inr 2), ⋯⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inl 0)).trace + (g (Sum.inr 0) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 0)).trace + g (Sum.inr 1) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 1)).trace + g (Sum.inr 2) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 2)).trace) = 0⊢ g (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) = 0g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), ⋯⟩ + (g (Sum.inr 0) • ⟨σ (Sum.inr 0), ⋯⟩ + g (Sum.inr 1) • ⟨σ (Sum.inr 1), ⋯⟩ + g (Sum.inr 2) • ⟨σ (Sum.inr 2), ⋯⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inl 0)).trace + (g (Sum.inr 0) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inr 0)).trace + g (Sum.inr 1) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inr 1)).trace + g (Sum.inr 2) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inr 2)).trace) = 0⊢ g (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) = 0g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), ⋯⟩ + (g (Sum.inr 0) • ⟨σ (Sum.inr 0), ⋯⟩ + g (Sum.inr 1) • ⟨σ (Sum.inr 1), ⋯⟩ + g (Sum.inr 2) • ⟨σ (Sum.inr 2), ⋯⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inl 0)).trace + (g (Sum.inr 0) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inr 0)).trace + g (Sum.inr 1) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inr 1)).trace + g (Sum.inr 2) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inr 2)).trace) = 0⊢ g (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) = 0 All goals completed! 🐙

The Pauli matrices span all self-adjoint matrices.

lemma pauliSelfAdjoint_span : ⊤ ≤ Submodule.span ℝ (Set.range pauliSelfAdjoint) := ⊢ ⊤ ≤ Submodule.span ℝ (Set.range pauliSelfAdjoint) ⊢ ∀ (x : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))), ∃ c, ∑ i, c i • pauliSelfAdjoint i = x A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ ∃ c, ∑ i, c i • pauliSelfAdjoint i = A A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ ∃ c, ∑ i, c i • pauliSelfAdjoint i = A A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ ∑ i, c i • pauliSelfAdjoint i = A A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inl 0) + ((2⁻¹ * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 0) + (2⁻¹ * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 1) + (2⁻¹ * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 2)) = A A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inl 0) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inl 0) + ((2⁻¹ * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 0) + (2⁻¹ * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 1) + (2⁻¹ * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 2)))).trace.re = (σ (Sum.inl 0) * ↑A).trace.reA:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inr 0) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inl 0) + ((2⁻¹ * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 0) + (2⁻¹ * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 1) + (2⁻¹ * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 2)))).trace.re = (σ (Sum.inr 0) * ↑A).trace.reA:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inr 1) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inl 0) + ((2⁻¹ * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 0) + (2⁻¹ * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 1) + (2⁻¹ * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 2)))).trace.re = (σ (Sum.inr 1) * ↑A).trace.reA:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inr 2) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inl 0) + ((2⁻¹ * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 0) + (2⁻¹ * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 1) + (2⁻¹ * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 2)))).trace.re = (σ (Sum.inr 2) * ↑A).trace.re A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inl 0) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inl 0) + ((2⁻¹ * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 0) + (2⁻¹ * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 1) + (2⁻¹ * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 2)))).trace.re = (σ (Sum.inl 0) * ↑A).trace.re A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ 2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re * 2 = (σ (Sum.inl 0) * ↑A).trace.re All goals completed! 🐙 A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inr 0) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inl 0) + ((2⁻¹ * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 0) + (2⁻¹ * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 1) + (2⁻¹ * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 2)))).trace.re = (σ (Sum.inr 0) * ↑A).trace.re A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ 2⁻¹ * (σ (Sum.inr 0) * ↑A).trace.re * 2 = (σ (Sum.inr 0) * ↑A).trace.re All goals completed! 🐙 A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inr 1) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inl 0) + ((2⁻¹ * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 0) + (2⁻¹ * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 1) + (2⁻¹ * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 2)))).trace.re = (σ (Sum.inr 1) * ↑A).trace.re A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ 2⁻¹ * (σ (Sum.inr 1) * ↑A).trace.re * 2 = (σ (Sum.inr 1) * ↑A).trace.re All goals completed! 🐙 A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inr 2) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inl 0) + ((2⁻¹ * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 0) + (2⁻¹ * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 1) + (2⁻¹ * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint (Sum.inr 2)))).trace.re = (σ (Sum.inr 2) * ↑A).trace.re A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => 1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => 1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => 1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ 2⁻¹ * (σ (Sum.inr 2) * ↑A).trace.re * 2 = (σ (Sum.inr 2) * ↑A).trace.re All goals completed! 🐙

The basis of selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) formed by Pauli matrices.

def pauliBasis : Basis (Fin 1 ⊕ Fin 3) ℝ (selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) := Basis.mk pauliSelfAdjoint_linearly_independent pauliSelfAdjoint_span

An auxiliary function which on i : Fin 1 ⊕ Fin 3 returns the corresponding Pauli-matrix as a self-adjoint matrix with a minus sign for Sum.inr _.

i:Fin 1 ⊕ Fin 3⊢ σ (Sum.inr 2) ∈ selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ); All goals completed! 🐙⟩

The Pauli matrices where σi are negated are linearly independent.

g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • pauliSelfAdjoint' (Sum.inl 0) + (g (Sum.inr 0) • pauliSelfAdjoint' (Sum.inr 0) + g (Sum.inr 1) • pauliSelfAdjoint' (Sum.inr 1) + g (Sum.inr 2) • pauliSelfAdjoint' (Sum.inr 2)) = 0⊢ ∀ (i : Fin 1 ⊕ Fin 3), g i = 0 g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), pauliSelfAdjoint'._proof_2⟩ + (g (Sum.inr 0) • ⟨-σ (Sum.inr 0), pauliSelfAdjoint'._proof_4⟩ + g (Sum.inr 1) • ⟨-σ (Sum.inr 1), pauliSelfAdjoint'._proof_5⟩ + g (Sum.inr 2) • ⟨-σ (Sum.inr 2), pauliSelfAdjoint'._proof_6⟩) = 0⊢ ∀ (i : Fin 1 ⊕ Fin 3), g i = 0 g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), pauliSelfAdjoint'._proof_2⟩ + (g (Sum.inr 0) • ⟨-σ (Sum.inr 0), pauliSelfAdjoint'._proof_4⟩ + g (Sum.inr 1) • ⟨-σ (Sum.inr 1), pauliSelfAdjoint'._proof_5⟩ + g (Sum.inr 2) • ⟨-σ (Sum.inr 2), pauliSelfAdjoint'._proof_6⟩) = 0i:Fin 1 ⊕ Fin 3⊢ g i = 0 g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), pauliSelfAdjoint'._proof_2⟩ + (g (Sum.inr 0) • ⟨-σ (Sum.inr 0), pauliSelfAdjoint'._proof_4⟩ + g (Sum.inr 1) • ⟨-σ (Sum.inr 1), pauliSelfAdjoint'._proof_5⟩ + g (Sum.inr 2) • ⟨-σ (Sum.inr 2), pauliSelfAdjoint'._proof_6⟩) = 0i:Fin 1 ⊕ Fin 3h1:(σ i * ↑(g (Sum.inl 0) • ⟨σ (Sum.inl 0), pauliSelfAdjoint'._proof_2⟩ + (g (Sum.inr 0) • ⟨-σ (Sum.inr 0), pauliSelfAdjoint'._proof_4⟩ + g (Sum.inr 1) • ⟨-σ (Sum.inr 1), pauliSelfAdjoint'._proof_5⟩ + g (Sum.inr 2) • ⟨-σ (Sum.inr 2), pauliSelfAdjoint'._proof_6⟩))).trace = (σ i * ↑0).trace⊢ g i = 0 g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), pauliSelfAdjoint'._proof_2⟩ + (g (Sum.inr 0) • ⟨-σ (Sum.inr 0), pauliSelfAdjoint'._proof_4⟩ + g (Sum.inr 1) • ⟨-σ (Sum.inr 1), pauliSelfAdjoint'._proof_5⟩ + g (Sum.inr 2) • ⟨-σ (Sum.inr 2), pauliSelfAdjoint'._proof_6⟩) = 0i:Fin 1 ⊕ Fin 3h1:g (Sum.inl 0) • (σ i * σ (Sum.inl 0)).trace + (-(g (Sum.inr 0) • (σ i * σ (Sum.inr 0)).trace) + -(g (Sum.inr 1) • (σ i * σ (Sum.inr 1)).trace) + -(g (Sum.inr 2) • (σ i * σ (Sum.inr 2)).trace)) = 0⊢ g i = 0 g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), pauliSelfAdjoint'._proof_2⟩ + (g (Sum.inr 0) • ⟨-σ (Sum.inr 0), pauliSelfAdjoint'._proof_4⟩ + g (Sum.inr 1) • ⟨-σ (Sum.inr 1), pauliSelfAdjoint'._proof_5⟩ + g (Sum.inr 2) • ⟨-σ (Sum.inr 2), pauliSelfAdjoint'._proof_6⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inl 0)).trace + (-(g (Sum.inr 0) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 0)).trace) + -(g (Sum.inr 1) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 1)).trace) + -(g (Sum.inr 2) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 2)).trace)) = 0⊢ g (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) = 0g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), pauliSelfAdjoint'._proof_2⟩ + (g (Sum.inr 0) • ⟨-σ (Sum.inr 0), pauliSelfAdjoint'._proof_4⟩ + g (Sum.inr 1) • ⟨-σ (Sum.inr 1), pauliSelfAdjoint'._proof_5⟩ + g (Sum.inr 2) • ⟨-σ (Sum.inr 2), pauliSelfAdjoint'._proof_6⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inl 0)).trace + (-(g (Sum.inr 0) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 0)).trace) + -(g (Sum.inr 1) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 1)).trace) + -(g (Sum.inr 2) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 2)).trace)) = 0⊢ g (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) = 0g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), pauliSelfAdjoint'._proof_2⟩ + (g (Sum.inr 0) • ⟨-σ (Sum.inr 0), pauliSelfAdjoint'._proof_4⟩ + g (Sum.inr 1) • ⟨-σ (Sum.inr 1), pauliSelfAdjoint'._proof_5⟩ + g (Sum.inr 2) • ⟨-σ (Sum.inr 2), pauliSelfAdjoint'._proof_6⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inl 0)).trace + (-(g (Sum.inr 0) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inr 0)).trace) + -(g (Sum.inr 1) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inr 1)).trace) + -(g (Sum.inr 2) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inr 2)).trace)) = 0⊢ g (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) = 0g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), pauliSelfAdjoint'._proof_2⟩ + (g (Sum.inr 0) • ⟨-σ (Sum.inr 0), pauliSelfAdjoint'._proof_4⟩ + g (Sum.inr 1) • ⟨-σ (Sum.inr 1), pauliSelfAdjoint'._proof_5⟩ + g (Sum.inr 2) • ⟨-σ (Sum.inr 2), pauliSelfAdjoint'._proof_6⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inl 0)).trace + (-(g (Sum.inr 0) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inr 0)).trace) + -(g (Sum.inr 1) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inr 1)).trace) + -(g (Sum.inr 2) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inr 2)).trace)) = 0⊢ g (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) = 0 g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), pauliSelfAdjoint'._proof_2⟩ + (g (Sum.inr 0) • ⟨-σ (Sum.inr 0), pauliSelfAdjoint'._proof_4⟩ + g (Sum.inr 1) • ⟨-σ (Sum.inr 1), pauliSelfAdjoint'._proof_5⟩ + g (Sum.inr 2) • ⟨-σ (Sum.inr 2), pauliSelfAdjoint'._proof_6⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inl 0)).trace + (-(g (Sum.inr 0) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 0)).trace) + -(g (Sum.inr 1) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 1)).trace) + -(g (Sum.inr 2) • (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 2)).trace)) = 0⊢ g (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) = 0g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), pauliSelfAdjoint'._proof_2⟩ + (g (Sum.inr 0) • ⟨-σ (Sum.inr 0), pauliSelfAdjoint'._proof_4⟩ + g (Sum.inr 1) • ⟨-σ (Sum.inr 1), pauliSelfAdjoint'._proof_5⟩ + g (Sum.inr 2) • ⟨-σ (Sum.inr 2), pauliSelfAdjoint'._proof_6⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inl 0)).trace + (-(g (Sum.inr 0) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 0)).trace) + -(g (Sum.inr 1) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 1)).trace) + -(g (Sum.inr 2) • (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr 2)).trace)) = 0⊢ g (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) = 0g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), pauliSelfAdjoint'._proof_2⟩ + (g (Sum.inr 0) • ⟨-σ (Sum.inr 0), pauliSelfAdjoint'._proof_4⟩ + g (Sum.inr 1) • ⟨-σ (Sum.inr 1), pauliSelfAdjoint'._proof_5⟩ + g (Sum.inr 2) • ⟨-σ (Sum.inr 2), pauliSelfAdjoint'._proof_6⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inl 0)).trace + (-(g (Sum.inr 0) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inr 0)).trace) + -(g (Sum.inr 1) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inr 1)).trace) + -(g (Sum.inr 2) • (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inr 2)).trace)) = 0⊢ g (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) = 0g:Fin 1 ⊕ Fin 3 → ℝhg:g (Sum.inl 0) • ⟨σ (Sum.inl 0), pauliSelfAdjoint'._proof_2⟩ + (g (Sum.inr 0) • ⟨-σ (Sum.inr 0), pauliSelfAdjoint'._proof_4⟩ + g (Sum.inr 1) • ⟨-σ (Sum.inr 1), pauliSelfAdjoint'._proof_5⟩ + g (Sum.inr 2) • ⟨-σ (Sum.inr 2), pauliSelfAdjoint'._proof_6⟩) = 0h1:g (Sum.inl 0) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inl 0)).trace + (-(g (Sum.inr 0) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inr 0)).trace) + -(g (Sum.inr 1) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inr 1)).trace) + -(g (Sum.inr 2) • (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inr 2)).trace)) = 0⊢ g (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) = 0 All goals completed! 🐙

The Pauli matrices where σi are negated span all Self-adjoint matrices.

lemma pauliSelfAdjoint'_span : ⊤ ≤ Submodule.span ℝ (Set.range pauliSelfAdjoint') := ⊢ ⊤ ≤ Submodule.span ℝ (Set.range pauliSelfAdjoint') ⊢ ∀ (x : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))), ∃ c, ∑ i, c i • pauliSelfAdjoint' i = x A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ ∃ c, ∑ i, c i • pauliSelfAdjoint' i = A A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ ∃ c, ∑ i, c i • pauliSelfAdjoint' i = A A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ ∑ i, c i • pauliSelfAdjoint' i = A A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inl 0) + ((-1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 2)) = A A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inl 0) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inl 0) + ((-1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 2)))).trace.re = (σ (Sum.inl 0) * ↑A).trace.reA:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inr 0) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inl 0) + ((-1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 2)))).trace.re = (σ (Sum.inr 0) * ↑A).trace.reA:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inr 1) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inl 0) + ((-1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 2)))).trace.re = (σ (Sum.inr 1) * ↑A).trace.reA:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inr 2) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inl 0) + ((-1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 2)))).trace.re = (σ (Sum.inr 2) * ↑A).trace.re A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inl 0) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inl 0) + ((-1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 2)))).trace.re = (σ (Sum.inl 0) * ↑A).trace.re A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ 2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re * 2 = (σ (Sum.inl 0) * ↑A).trace.re All goals completed! 🐙 A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inr 0) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inl 0) + ((-1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 2)))).trace.re = (σ (Sum.inr 0) * ↑A).trace.re A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ -(-1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re * 2) = (σ (Sum.inr 0) * ↑A).trace.re All goals completed! 🐙 A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inr 1) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inl 0) + ((-1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 2)))).trace.re = (σ (Sum.inr 1) * ↑A).trace.re A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ -(-1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re * 2) = (σ (Sum.inr 1) * ↑A).trace.re All goals completed! 🐙 A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ (σ (Sum.inr 2) * ↑((2⁻¹ * (σ (Sum.inl 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inl 0) + ((-1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re) • pauliSelfAdjoint' (Sum.inr 2)))).trace.re = (σ (Sum.inr 2) * ↑A).trace.re A:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))c:Fin 1 ⊕ Fin 3 → ℝ := fun i => match i with | Sum.inl 0 => 1 / 2 * (σ (Sum.inl 0) * ↑A).trace.re | Sum.inr 0 => -1 / 2 * (σ (Sum.inr 0) * ↑A).trace.re | Sum.inr 1 => -1 / 2 * (σ (Sum.inr 1) * ↑A).trace.re | Sum.inr 2 => -1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re⊢ -(-1 / 2 * (σ (Sum.inr 2) * ↑A).trace.re * 2) = (σ (Sum.inr 2) * ↑A).trace.re All goals completed! 🐙

The basis of selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) formed by Pauli matrices where the 1, 2, 3 pauli matrices are negated. These can be thought of as the covariant Pauli-matrices.

def pauliBasis' : Basis (Fin 1 ⊕ Fin 3) ℝ (selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) := Basis.mk pauliSelfAdjoint'_linearly_independent pauliSelfAdjoint'_span

The decomposition of a self-adjoint matrix into the Pauli matrices (where σi are negated).

lemma pauliBasis'_decomp (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) : M = (1/2 * (Matrix.trace (σ0 * M.1)).re) • pauliBasis' (Sum.inl 0) + (-1/2 * (Matrix.trace (σ1 * M.1)).re) • pauliBasis' (Sum.inr 0) + (-1/2 * (Matrix.trace (σ2 * M.1)).re) • pauliBasis' (Sum.inr 1) + (-1/2 * (Matrix.trace (σ3 * M.1)).re) • pauliBasis' (Sum.inr 2) := M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ M = (1 / 2 * (σ (Sum.inl 0) * ↑M).trace.re) • pauliBasis' (Sum.inl 0) + (-1 / 2 * (σ (Sum.inr 0) * ↑M).trace.re) • pauliBasis' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑M).trace.re) • pauliBasis' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑M).trace.re) • pauliBasis' (Sum.inr 2) M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ (σ (Sum.inl 0) * ↑M).trace.re = (σ (Sum.inl 0) * ↑((1 / 2 * (σ (Sum.inl 0) * ↑M).trace.re) • pauliBasis' (Sum.inl 0) + (-1 / 2 * (σ (Sum.inr 0) * ↑M).trace.re) • pauliBasis' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑M).trace.re) • pauliBasis' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑M).trace.re) • pauliBasis' (Sum.inr 2))).trace.reM:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ (σ (Sum.inr 0) * ↑M).trace.re = (σ (Sum.inr 0) * ↑((1 / 2 * (σ (Sum.inl 0) * ↑M).trace.re) • pauliBasis' (Sum.inl 0) + (-1 / 2 * (σ (Sum.inr 0) * ↑M).trace.re) • pauliBasis' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑M).trace.re) • pauliBasis' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑M).trace.re) • pauliBasis' (Sum.inr 2))).trace.reM:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ (σ (Sum.inr 1) * ↑M).trace.re = (σ (Sum.inr 1) * ↑((1 / 2 * (σ (Sum.inl 0) * ↑M).trace.re) • pauliBasis' (Sum.inl 0) + (-1 / 2 * (σ (Sum.inr 0) * ↑M).trace.re) • pauliBasis' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑M).trace.re) • pauliBasis' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑M).trace.re) • pauliBasis' (Sum.inr 2))).trace.reM:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ (σ (Sum.inr 2) * ↑M).trace.re = (σ (Sum.inr 2) * ↑((1 / 2 * (σ (Sum.inl 0) * ↑M).trace.re) • pauliBasis' (Sum.inl 0) + (-1 / 2 * (σ (Sum.inr 0) * ↑M).trace.re) • pauliBasis' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑M).trace.re) • pauliBasis' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑M).trace.re) • pauliBasis' (Sum.inr 2))).trace.re M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ (σ (Sum.inl 0) * ↑M).trace.re = (σ (Sum.inl 0) * ↑((1 / 2 * (σ (Sum.inl 0) * ↑M).trace.re) • pauliBasis' (Sum.inl 0) + (-1 / 2 * (σ (Sum.inr 0) * ↑M).trace.re) • pauliBasis' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑M).trace.re) • pauliBasis' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑M).trace.re) • pauliBasis' (Sum.inr 2))).trace.re M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ (σ (Sum.inl 0) * ↑M).trace.re = 2⁻¹ * (σ (Sum.inl 0) * ↑M).trace.re * 2 All goals completed! 🐙 M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ (σ (Sum.inr 0) * ↑M).trace.re = (σ (Sum.inr 0) * ↑((1 / 2 * (σ (Sum.inl 0) * ↑M).trace.re) • pauliBasis' (Sum.inl 0) + (-1 / 2 * (σ (Sum.inr 0) * ↑M).trace.re) • pauliBasis' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑M).trace.re) • pauliBasis' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑M).trace.re) • pauliBasis' (Sum.inr 2))).trace.re M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ (σ (Sum.inr 0) * ↑M).trace.re = -(-1 / 2 * (σ (Sum.inr 0) * ↑M).trace.re * 2) All goals completed! 🐙 M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ (σ (Sum.inr 1) * ↑M).trace.re = (σ (Sum.inr 1) * ↑((1 / 2 * (σ (Sum.inl 0) * ↑M).trace.re) • pauliBasis' (Sum.inl 0) + (-1 / 2 * (σ (Sum.inr 0) * ↑M).trace.re) • pauliBasis' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑M).trace.re) • pauliBasis' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑M).trace.re) • pauliBasis' (Sum.inr 2))).trace.re M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ (σ (Sum.inr 1) * ↑M).trace.re = -(-1 / 2 * (σ (Sum.inr 1) * ↑M).trace.re * 2) All goals completed! 🐙 M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ (σ (Sum.inr 2) * ↑M).trace.re = (σ (Sum.inr 2) * ↑((1 / 2 * (σ (Sum.inl 0) * ↑M).trace.re) • pauliBasis' (Sum.inl 0) + (-1 / 2 * (σ (Sum.inr 0) * ↑M).trace.re) • pauliBasis' (Sum.inr 0) + (-1 / 2 * (σ (Sum.inr 1) * ↑M).trace.re) • pauliBasis' (Sum.inr 1) + (-1 / 2 * (σ (Sum.inr 2) * ↑M).trace.re) • pauliBasis' (Sum.inr 2))).trace.re M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ (σ (Sum.inr 2) * ↑M).trace.re = -(-1 / 2 * (σ (Sum.inr 2) * ↑M).trace.re * 2) All goals completed! 🐙

The component of a self-adjoint matrix in the direction σ0 under the basis formed by the covariant Pauli matrices.

@[simp] lemma pauliBasis'_repr_inl_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) : pauliBasis'.repr M (Sum.inl 0) = 1 / 2 * Matrix.trace (σ0 * M.1) := M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ ↑((pauliBasis'.repr M) (Sum.inl 0)) = 1 / 2 * (σ (Sum.inl 0) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = ∑ i, (pauliBasis'.repr M) i • pauliBasis' i⊢ ↑((pauliBasis'.repr M) (Sum.inl 0)) = 1 / 2 * (σ (Sum.inl 0) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))⊢ ↑((pauliBasis'.repr M) (Sum.inl 0)) = 1 / 2 * (σ (Sum.inl 0) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))h0:(σ (Sum.inl 0) * ↑M).trace / 2 = (σ (Sum.inl 0) * ↑((pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2)))).trace / 2⊢ ↑((pauliBasis'.repr M) (Sum.inl 0)) = 1 / 2 * (σ (Sum.inl 0) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))h0:(σ (Sum.inl 0) * ↑M).trace / 2 = ↑((pauliSelfAdjoint'_linearly_independent.repr ⟨M, ⋯⟩) (Sum.inl 0))⊢ ↑((pauliBasis'.repr M) (Sum.inl 0)) = 1 / 2 * (σ (Sum.inl 0) * ↑M).trace linear_combination (norm := M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))h0:(σ (Sum.inl 0) * ↑M).trace / 2 = ↑((pauliSelfAdjoint'_linearly_independent.repr ⟨M, ⋯⟩) (Sum.inl 0))⊢ ↑((pauliBasis'.repr M) (Sum.inl 0)) - ↑((pauliSelfAdjoint'_linearly_independent.repr ⟨M, ⋯⟩) (Sum.inl 0)) = 0) -h0 All goals completed! 🐙

The component of a self-adjoint matrix in the direction -σ1 under the basis formed by the covariant Pauli matrices.

@[simp] lemma pauliBasis'_repr_inr_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) : pauliBasis'.repr M (Sum.inr 0) = - 1 / 2 * Matrix.trace (σ1 * M.1) := M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ ↑((pauliBasis'.repr M) (Sum.inr 0)) = -1 / 2 * (σ (Sum.inr 0) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = ∑ i, (pauliBasis'.repr M) i • pauliBasis' i⊢ ↑((pauliBasis'.repr M) (Sum.inr 0)) = -1 / 2 * (σ (Sum.inr 0) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))⊢ ↑((pauliBasis'.repr M) (Sum.inr 0)) = -1 / 2 * (σ (Sum.inr 0) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))h0:-(σ (Sum.inr 0) * ↑M).trace / 2 = -(σ (Sum.inr 0) * ↑((pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2)))).trace / 2⊢ ↑((pauliBasis'.repr M) (Sum.inr 0)) = -1 / 2 * (σ (Sum.inr 0) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))h0:-(σ (Sum.inr 0) * ↑M).trace / 2 = ↑((pauliSelfAdjoint'_linearly_independent.repr ⟨M, ⋯⟩) (Sum.inr 0))⊢ ↑((pauliBasis'.repr M) (Sum.inr 0)) = -1 / 2 * (σ (Sum.inr 0) * ↑M).trace linear_combination (norm := M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))h0:-(σ (Sum.inr 0) * ↑M).trace / 2 = ↑((pauliSelfAdjoint'_linearly_independent.repr ⟨M, ⋯⟩) (Sum.inr 0))⊢ ↑((pauliBasis'.repr M) (Sum.inr 0)) - ↑((pauliSelfAdjoint'_linearly_independent.repr ⟨M, ⋯⟩) (Sum.inr 0)) = 0) -h0 All goals completed! 🐙

The component of a self-adjoint matrix in the direction -σ2 under the basis formed by the covariant Pauli matrices.

@[simp] lemma pauliBasis'_repr_inr_1 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) : pauliBasis'.repr M (Sum.inr 1) = - 1 / 2 * Matrix.trace (σ2 * M.1) := M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ ↑((pauliBasis'.repr M) (Sum.inr 1)) = -1 / 2 * (σ (Sum.inr 1) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = ∑ i, (pauliBasis'.repr M) i • pauliBasis' i⊢ ↑((pauliBasis'.repr M) (Sum.inr 1)) = -1 / 2 * (σ (Sum.inr 1) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))⊢ ↑((pauliBasis'.repr M) (Sum.inr 1)) = -1 / 2 * (σ (Sum.inr 1) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))h0:-(σ (Sum.inr 1) * ↑M).trace / 2 = -(σ (Sum.inr 1) * ↑((pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2)))).trace / 2⊢ ↑((pauliBasis'.repr M) (Sum.inr 1)) = -1 / 2 * (σ (Sum.inr 1) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))h0:-(σ (Sum.inr 1) * ↑M).trace / 2 = ↑((pauliSelfAdjoint'_linearly_independent.repr ⟨M, ⋯⟩) (Sum.inr 1))⊢ ↑((pauliBasis'.repr M) (Sum.inr 1)) = -1 / 2 * (σ (Sum.inr 1) * ↑M).trace linear_combination (norm := M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))h0:-(σ (Sum.inr 1) * ↑M).trace / 2 = ↑((pauliSelfAdjoint'_linearly_independent.repr ⟨M, ⋯⟩) (Sum.inr 1))⊢ ↑((pauliBasis'.repr M) (Sum.inr 1)) - ↑((pauliSelfAdjoint'_linearly_independent.repr ⟨M, ⋯⟩) (Sum.inr 1)) = 0) -h0 All goals completed! 🐙

The component of a self-adjoint matrix in the direction -σ3 under the basis formed by the covariant Pauli matrices.

@[simp] lemma pauliBasis'_repr_inr_2 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) : pauliBasis'.repr M (Sum.inr 2) = - 1 / 2 * Matrix.trace (σ3 * M.1) := M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))⊢ ↑((pauliBasis'.repr M) (Sum.inr 2)) = -1 / 2 * (σ (Sum.inr 2) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = ∑ i, (pauliBasis'.repr M) i • pauliBasis' i⊢ ↑((pauliBasis'.repr M) (Sum.inr 2)) = -1 / 2 * (σ (Sum.inr 2) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))⊢ ↑((pauliBasis'.repr M) (Sum.inr 2)) = -1 / 2 * (σ (Sum.inr 2) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))h0:-(σ (Sum.inr 2) * ↑M).trace / 2 = -(σ (Sum.inr 2) * ↑((pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2)))).trace / 2⊢ ↑((pauliBasis'.repr M) (Sum.inr 2)) = -1 / 2 * (σ (Sum.inr 2) * ↑M).trace M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))h0:-(σ (Sum.inr 2) * ↑M).trace / 2 = ↑((pauliSelfAdjoint'_linearly_independent.repr ⟨M, ⋯⟩) (Sum.inr 2))⊢ ↑((pauliBasis'.repr M) (Sum.inr 2)) = -1 / 2 * (σ (Sum.inr 2) * ↑M).trace linear_combination (norm := M:↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))hM:M = (pauliBasis'.repr M) (Sum.inl 0) • pauliBasis' (Sum.inl 0) + ((pauliBasis'.repr M) (Sum.inr 0) • pauliBasis' (Sum.inr 0) + (pauliBasis'.repr M) (Sum.inr 1) • pauliBasis' (Sum.inr 1) + (pauliBasis'.repr M) (Sum.inr 2) • pauliBasis' (Sum.inr 2))h0:-(σ (Sum.inr 2) * ↑M).trace / 2 = ↑((pauliSelfAdjoint'_linearly_independent.repr ⟨M, ⋯⟩) (Sum.inr 2))⊢ ↑((pauliBasis'.repr M) (Sum.inr 2)) - ↑((pauliSelfAdjoint'_linearly_independent.repr ⟨M, ⋯⟩) (Sum.inr 2)) = 0) -h0 All goals completed! 🐙

The relationship between the basis pauliBasis of contravariant Pauli-matrices and the basis pauliBasis' of covariant Pauli matrices is by multiplication by the Minkowski matrix.

lemma pauliBasis_minkowskiMetric_pauliBasis' (i : Fin 1 ⊕ Fin 3) : pauliBasis i = minkowskiMatrix i i • pauliBasis' i := i:Fin 1 ⊕ Fin 3⊢ pauliBasis i = minkowskiMatrix i i • pauliBasis' i ⊢ pauliBasis (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) = minkowskiMatrix (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) • pauliBasis' (Sum.inl ((fun i => i) ⟨0, ⋯⟩))⊢ pauliBasis (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) = minkowskiMatrix (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) • pauliBasis' (Sum.inr ((fun i => i) ⟨0, ⋯⟩))⊢ pauliBasis (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) = minkowskiMatrix (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) • pauliBasis' (Sum.inr ((fun i => i) ⟨1, ⋯⟩))⊢ pauliBasis (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) = minkowskiMatrix (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) • pauliBasis' (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ⊢ pauliBasis (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) = minkowskiMatrix (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) • pauliBasis' (Sum.inl ((fun i => i) ⟨0, ⋯⟩))⊢ pauliBasis (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) = minkowskiMatrix (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) • pauliBasis' (Sum.inr ((fun i => i) ⟨0, ⋯⟩))⊢ pauliBasis (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) = minkowskiMatrix (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) • pauliBasis' (Sum.inr ((fun i => i) ⟨1, ⋯⟩))⊢ pauliBasis (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) = minkowskiMatrix (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) • pauliBasis' (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) All goals completed! 🐙