Physlib.Relativity.LorentzAlgebra.Basis

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.LorentzAlgebra.Basic

Generators of the Lorentz Algebra

This file defines the 6 standard generators of the Lorentz algebra so(1,3) :

Boost generators K₀, K₁, K₂: Generate Lorentz transformations (velocity changes)

Rotation generators J₀, J₁, J₂: Generate spatial rotations

These generators form a basis for the 6-dimensional Lie algebra so(1,3), though the full basis structure (linear independence and spanning) is not yet proven here.

Physical Interpretation

boostGenerator i: Infinitesimal boost in the i-th spatial direction. Exponentiating this generator produces finite Lorentz boosts.

rotationGenerator i: Infinitesimal rotation about the i-th axis following the right-hand rule. Exponentiating this generator produces spatial rotations.

Mathematical Structure

Each generator satisfies the Lorentz algebra condition: Aᵀ η = -η A, where η is the Minkowski metric with signature (+,-,-,-).

The boost generators are symmetric matrices with non-zero entries only in the time-space block, while rotation generators are antisymmetric matrices acting only on spatial indices.

References

Weinberg, The Quantum Theory of Fields, Vol 1, Section 2.7

Peskin & Schroeder, An Introduction to QFT, Appendix A

Future Work

TODO can be completed by proving linear independence and spanning of these 6 generators, then constructing a formal Basis (Fin 2 × Fin 3) ℝ lorentzAlgebra.

@[expose] public section

The boost generator K_i in the Lorentz algebra so(1,3).

This matrix generates infinitesimal Lorentz boosts in the i-th spatial direction. The matrix has non-zero entries only at positions (0, i+1) and (i+1, 0) with value 1, where we use the index convention 0 = time, 1,2,3 = space.

Properties

Symmetric: K_iᵀ = K_i

Traceless: tr(K_i) = 0

Satisfies Lorentz algebra condition: K_iᵀ η = -η K_i

Physical Meaning

Exponentiating β·K_i produces a finite Lorentz boost with rapidity β in direction i.

def boostGenerator (i : Fin 3) : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ :=
  fun μ ν =>
    if (μ = Sum.inl 0 ∧ ν = Sum.inr i) ∨ (μ = Sum.inr i ∧ ν = Sum.inl 0) then 1
    else 0

The rotation generator J_i in the Lorentz algebra so(1,3).

This matrix generates infinitesimal rotations about the i-th axis following the right-hand rule. The matrix acts only on spatial indices in the antisymmetric pattern characteristic of angular momentum generators.

Properties

Antisymmetric: J_iᵀ = -J_i

Traceless: tr(J_i) = 0

Satisfies Lorentz algebra condition: J_iᵀ η = -η J_i

Structure

J_0 (rotation about x-axis) : Acts on (y,z) components

J_1 (rotation about y-axis) : Acts on (z,x) components

J_2 (rotation about z-axis) : Acts on (x,y) components

Physical Meaning

Exponentiating θ·J_i produces a finite rotation by angle θ about axis i.

def rotationGenerator (i : Fin 3) : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ :=
  fun μ ν =>
    match i with
    | 0 => if μ = Sum.inr 1 ∧ ν = Sum.inr 2 then -1
            else if μ = Sum.inr 2 ∧ ν = Sum.inr 1 then 1
            else 0
      | 1 => if μ = Sum.inr 0 ∧ ν = Sum.inr 2 then 1
            else if μ = Sum.inr 2 ∧ ν = Sum.inr 0 then -1
            else 0
      | 2 => if μ = Sum.inr 0 ∧ ν = Sum.inr 1 then -1
            else if μ = Sum.inr 1 ∧ ν = Sum.inr 0 then 1
            else 0

The boost generator K_i is in the Lorentz algebra.


lemma boostGenerator_mem (i : Fin 3) : boostGenerator i ∈ lorentzAlgebra := byi:Fin 3⊢ boostGenerator i ∈ lorentzAlgebra
  rw [lorentzAlgebra.mem_iffi:Fin 3⊢ (boostGenerator i)ᵀ * minkowskiMatrix = -minkowskiMatrix * boostGenerator ii:Fin 3⊢ (boostGenerator i)ᵀ * minkowskiMatrix = -minkowskiMatrix * boostGenerator i]i:Fin 3⊢ (boostGenerator i)ᵀ * minkowskiMatrix = -minkowskiMatrix * boostGenerator i
  ext μ νi:Fin 3μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) μ ν = (-minkowskiMatrix * boostGenerator i) μ ν
  fin_cases μ«0»i:Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-minkowskiMatrix * boostGenerator i) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν«1»i:Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν«2»i:Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν«3»i:Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν <;>«0»i:Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-minkowskiMatrix * boostGenerator i) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν«1»i:Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν«2»i:Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν«3»i:Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν fin_cases ν«3».«0»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«3».«1»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«3».«2»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«3».«3»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) <;>«0».«0»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«0».«1»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«0».«2»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«0».«3»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«1».«0»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«1».«1»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«1».«2»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«1».«3»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«2».«0»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«2».«1»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«2».«2»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«2».«3»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«3».«0»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«3».«1»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«3».«2»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«3».«3»i:Fin 3⊢ ((boostGenerator i)ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * boostGenerator i) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    simp [boostGenerator, minkowskiMatrix.as_diagonal, mul_diagonal, diagonal_mul, neg_ite]All goals completed! 🐙

The rotation generator J_i is in the Lorentz algebra.


lemma rotationGenerator_mem (i : Fin 3) : rotationGenerator i ∈ lorentzAlgebra := byi:Fin 3⊢ rotationGenerator i ∈ lorentzAlgebra
  rw [lorentzAlgebra.mem_iffi:Fin 3⊢ (rotationGenerator i)ᵀ * minkowskiMatrix = -minkowskiMatrix * rotationGenerator ii:Fin 3⊢ (rotationGenerator i)ᵀ * minkowskiMatrix = -minkowskiMatrix * rotationGenerator i]i:Fin 3⊢ (rotationGenerator i)ᵀ * minkowskiMatrix = -minkowskiMatrix * rotationGenerator i
  ext μ νi:Fin 3μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator i)ᵀ * minkowskiMatrix) μ ν = (-minkowskiMatrix * rotationGenerator i) μ ν
  fin_cases i«0»μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) μ ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) μ ν«1»μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) μ ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) μ ν«2»μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) μ ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) μ ν <;>«0»μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) μ ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) μ ν«1»μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) μ ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) μ ν«2»μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) μ ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) μ ν fin_cases μ«2».«0»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν«2».«1»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν«2».«2»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν«2».«3»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν <;>«0».«0»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν«0».«1»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν«0».«2»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν«0».«3»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν«1».«0»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν«1».«1»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν«1».«2»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν«1».«3»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν«2».«0»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν«2».«1»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν«2».«2»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν«2».«3»ν:Fin 1 ⊕ Fin 3⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν fin_cases ν«2».«3».«0»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«2».«3».«1»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«2».«3».«2»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«2».«3».«3»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) <;>«0».«0».«0»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«0».«0».«1»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«0».«0».«2»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«0».«0».«3»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«0».«1».«0»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«0».«1».«1»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«0».«1».«2»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«0».«1».«3»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«0».«2».«0»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«0».«2».«1»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«0».«2».«2»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«0».«2».«3»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«0».«3».«0»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«0».«3».«1»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«0».«3».«2»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«0».«3».«3»⊢ ((rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«1».«0».«0»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«1».«0».«1»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«1».«0».«2»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«1».«0».«3»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«1».«1».«0»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«1».«1».«1»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«1».«1».«2»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«1».«1».«3»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«1».«2».«0»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«1».«2».«1»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«1».«2».«2»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«1».«2».«3»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«1».«3».«0»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«1».«3».«1»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«1».«3».«2»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«1».«3».«3»⊢ ((rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«2».«0».«0»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«2».«0».«1»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«2».«0».«2»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«2».«0».«3»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«2».«1».«0»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«2».«1».«1»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«2».«1».«2»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«2».«1».«3»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«2».«2».«0»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«2».«2».«1»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«2».«2».«2»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«2».«2».«3»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«2».«3».«0»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«2».«3».«1»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«2».«3».«2»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«2».«3».«3»⊢ ((rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ * minkowskiMatrix) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-minkowskiMatrix * rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
    simp [rotationGenerator, minkowskiMatrix.as_diagonal, mul_diagonal, diagonal_mul]All goals completed! 🐙

The boost generators are symmetric.

@[simp]
lemma boostGenerator_transpose (i : Fin 3) :
    (boostGenerator i)ᵀ = boostGenerator i := byi:Fin 3⊢ (boostGenerator i)ᵀ = boostGenerator i
  ext μ νi:Fin 3μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ (boostGenerator i)ᵀ μ ν = boostGenerator i μ ν
  simp only [transpose_apply, boostGenerator, and_comm, or_comm]All goals completed! 🐙

The boost generators are traceless.

@[simp]
lemma boostGenerator_trace (i : Fin 3) :
    Matrix.trace (boostGenerator i) = 0 := byi:Fin 3⊢ (boostGenerator i).trace = 0
  simp [Matrix.trace, Matrix.diag, boostGenerator]All goals completed! 🐙

The rotation generators are antisymmetric.

@[simp]
lemma rotationGenerator_transpose (i : Fin 3) :
    (rotationGenerator i)ᵀ = -rotationGenerator i := byi:Fin 3⊢ (rotationGenerator i)ᵀ = -rotationGenerator i
  ext μ νi:Fin 3μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator i)ᵀ μ ν = (-rotationGenerator i) μ ν
  fin_cases i«0»μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ μ ν = (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) μ ν«1»μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ μ ν = (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) μ ν«2»μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ μ ν = (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) μ ν <;>«0»μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ μ ν = (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) μ ν«1»μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ μ ν = (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) μ ν«2»μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ μ ν = (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) μ ν fin_cases μ«2».«0»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν«2».«1»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν«2».«2»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν«2».«3»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν <;>«0».«0»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν«0».«1»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν«0».«2»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν«0».«3»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν«1».«0»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν«1».«1»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν«1».«2»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν«1».«3»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν«2».«0»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) ν«2».«1»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) ν«2».«2»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) ν«2».«3»ν:Fin 1 ⊕ Fin 3⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) ν fin_cases ν«2».«3».«0»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«2».«3».«1»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«2».«3».«2»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«2».«3».«3»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) <;>«0».«0».«0»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«0».«0».«1»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«0».«0».«2»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«0».«0».«3»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«0».«1».«0»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«0».«1».«1»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«0».«1».«2»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«0».«1».«3»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«0».«2».«0»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«0».«2».«1»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«0».«2».«2»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«0».«2».«3»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«0».«3».«0»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«0».«3».«1»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«0».«3».«2»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«0».«3».«3»⊢ (rotationGenerator ((fun i => i) ⟨0, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«1».«0».«0»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«1».«0».«1»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«1».«0».«2»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«1».«0».«3»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«1».«1».«0»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«1».«1».«1»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«1».«1».«2»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«1».«1».«3»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«1».«2».«0»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«1».«2».«1»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«1».«2».«2»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«1».«2».«3»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«1».«3».«0»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«1».«3».«1»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«1».«3».«2»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«1».«3».«3»⊢ (rotationGenerator ((fun i => i) ⟨1, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«2».«0».«0»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«2».«0».«1»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«2».«0».«2»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«2».«0».«3»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«2».«1».«0»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«2».«1».«1»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«2».«1».«2»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«2».«1».«3»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«2».«2».«0»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«2».«2».«1»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«2».«2».«2»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«2».«2».«3»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩))«2».«3».«0»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«2».«3».«1»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«2».«3».«2»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«2».«3».«3»⊢ (rotationGenerator ((fun i => i) ⟨2, ⋯⟩))ᵀ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) =
  (-rotationGenerator ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) simp [rotationGenerator]All goals completed! 🐙

The rotation generators are traceless.


@[simp]
lemma rotationGenerator_trace (i : Fin 3) :
    Matrix.trace (rotationGenerator i) = 0 := byi:Fin 3⊢ (rotationGenerator i).trace = 0
  have h := Matrix.trace_transpose (rotationGenerator i)i:Fin 3h:(rotationGenerator i)ᵀ.trace = (rotationGenerator i).trace⊢ (rotationGenerator i).trace = 0
  rw [rotationGenerator_transpose,i:Fin 3h:(-rotationGenerator i).trace = (rotationGenerator i).trace⊢ (rotationGenerator i).trace = 0i:Fin 3h:-(rotationGenerator i).trace = (rotationGenerator i).trace⊢ (rotationGenerator i).trace = 0 Matrix.trace_negi:Fin 3h:-(rotationGenerator i).trace = (rotationGenerator i).trace⊢ (rotationGenerator i).trace = 0i:Fin 3h:-(rotationGenerator i).trace = (rotationGenerator i).trace⊢ (rotationGenerator i).trace = 0] at hi:Fin 3h:-(rotationGenerator i).trace = (rotationGenerator i).trace⊢ (rotationGenerator i).trace = 0
  exact eq_zero_of_neg_eq hAll goals completed! 🐙