Physlib.Particles.FlavorPhysics.CKMMatrix.Basic

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 Mathlib.LinearAlgebra.UnitaryGroup
public import Mathlib.Analysis.Complex.Trigonometric

The CKM Matrix

The definition of the type of CKM matrices as unitary $3×3$-matrices.

An equivalence relation on CKM matrices is defined, where two matrices are equivalent if they are related by phase shifts.

The notation [V]ud etc can be used for the elements of a CKM matrix, and [V]ud|us etc for the ratios of elements.

@[expose] public section

Given three real numbers a b c the complex matrix with exp (I * a) etc on the leading diagonal.

@[simp]
def phaseShiftMatrix (a b c : ℝ) : Matrix (Fin 3) (Fin 3) ℂ :=
  ![![cexp (I * a), 0, 0], ![0, cexp (I * b), 0], ![0, 0, cexp (I * c)]]

The phase shift matrix for zero-phases is the identity.

lemma phaseShiftMatrix_one : phaseShiftMatrix 0 0 0 = 1 := by⊢ phaseShiftMatrix 0 0 0 = 1
  ext i ji:Fin 3j:Fin 3⊢ phaseShiftMatrix 0 0 0 i j = 1 i j
  fin_cases i«0»j:Fin 3⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨0, ⋯⟩) j = 1 ((fun i => i) ⟨0, ⋯⟩) j«1»j:Fin 3⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨1, ⋯⟩) j = 1 ((fun i => i) ⟨1, ⋯⟩) j«2»j:Fin 3⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨2, ⋯⟩) j = 1 ((fun i => i) ⟨2, ⋯⟩) j <;>«0»j:Fin 3⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨0, ⋯⟩) j = 1 ((fun i => i) ⟨0, ⋯⟩) j«1»j:Fin 3⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨1, ⋯⟩) j = 1 ((fun i => i) ⟨1, ⋯⟩) j«2»j:Fin 3⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨2, ⋯⟩) j = 1 ((fun i => i) ⟨2, ⋯⟩) j fin_cases j«2».«0»⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = 1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«2».«1»⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = 1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«2».«2»⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = 1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) <;>«0».«0»⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = 1 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«0».«1»⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = 1 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«0».«2»⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = 1 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)«1».«0»⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = 1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«1».«1»⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = 1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«1».«2»⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = 1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)«2».«0»⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = 1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«2».«1»⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = 1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«2».«2»⊢ phaseShiftMatrix 0 0 0 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = 1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) simp [phaseShiftMatrix, one_apply]All goals completed! 🐙

The conjugate transpose of the phase shift matrix is the phase-shift matrix with negated phases.

lemma phaseShiftMatrix_star (a b c : ℝ) :
    (phaseShiftMatrix a b c)ᴴ = phaseShiftMatrix (- a) (- b) (- c) := bya:ℝb:ℝc:ℝ⊢ (phaseShiftMatrix a b c)ᴴ = phaseShiftMatrix (-a) (-b) (-c)
  funext i ja:ℝb:ℝc:ℝi:Fin 3j:Fin 3⊢ (phaseShiftMatrix a b c)ᴴ i j = phaseShiftMatrix (-a) (-b) (-c) i j
  fin_cases i«0»a:ℝb:ℝc:ℝj:Fin 3⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨0, ⋯⟩) j = phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨0, ⋯⟩) j«1»a:ℝb:ℝc:ℝj:Fin 3⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨1, ⋯⟩) j = phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨1, ⋯⟩) j«2»a:ℝb:ℝc:ℝj:Fin 3⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨2, ⋯⟩) j = phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨2, ⋯⟩) j <;>«0»a:ℝb:ℝc:ℝj:Fin 3⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨0, ⋯⟩) j = phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨0, ⋯⟩) j«1»a:ℝb:ℝc:ℝj:Fin 3⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨1, ⋯⟩) j = phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨1, ⋯⟩) j«2»a:ℝb:ℝc:ℝj:Fin 3⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨2, ⋯⟩) j = phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨2, ⋯⟩) j fin_cases j«2».«0»a:ℝb:ℝc:ℝ⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«2».«1»a:ℝb:ℝc:ℝ⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«2».«2»a:ℝb:ℝc:ℝ⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) <;>«0».«0»a:ℝb:ℝc:ℝ⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«0».«1»a:ℝb:ℝc:ℝ⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«0».«2»a:ℝb:ℝc:ℝ⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)«1».«0»a:ℝb:ℝc:ℝ⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«1».«1»a:ℝb:ℝc:ℝ⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«1».«2»a:ℝb:ℝc:ℝ⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)«2».«0»a:ℝb:ℝc:ℝ⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«2».«1»a:ℝb:ℝc:ℝ⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«2».«2»a:ℝb:ℝc:ℝ⊢ (phaseShiftMatrix a b c)ᴴ ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  phaseShiftMatrix (-a) (-b) (-c) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)
    simp [phaseShiftMatrix, conjTranspose_apply, ← exp_conj, conj_I, conj_ofReal]All goals completed! 🐙

The multiple of two phase shift matrices is equal to the phase shift matrix with added phases.

lemma phaseShiftMatrix_mul (a b c d e f : ℝ) :
    phaseShiftMatrix a b c * phaseShiftMatrix d e f = phaseShiftMatrix (a + d) (b + e) (c + f) := bya:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ phaseShiftMatrix a b c * phaseShiftMatrix d e f = phaseShiftMatrix (a + d) (b + e) (c + f)
  ext i ja:ℝb:ℝc:ℝd:ℝe:ℝf:ℝi:Fin 3j:Fin 3⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) i j = phaseShiftMatrix (a + d) (b + e) (c + f) i j
  fin_cases i«0»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝj:Fin 3⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨0, ⋯⟩) j =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨0, ⋯⟩) j«1»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝj:Fin 3⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨1, ⋯⟩) j =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨1, ⋯⟩) j«2»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝj:Fin 3⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨2, ⋯⟩) j =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨2, ⋯⟩) j <;>«0»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝj:Fin 3⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨0, ⋯⟩) j =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨0, ⋯⟩) j«1»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝj:Fin 3⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨1, ⋯⟩) j =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨1, ⋯⟩) j«2»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝj:Fin 3⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨2, ⋯⟩) j =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨2, ⋯⟩) j fin_cases j«2».«0»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«2».«1»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«2».«2»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) <;>«0».«0»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«0».«1»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«0».«2»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)«1».«0»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«1».«1»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«1».«2»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)«2».«0»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«2».«1»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«2».«2»a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ (phaseShiftMatrix a b c * phaseShiftMatrix d e f) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  phaseShiftMatrix (a + d) (b + e) (c + f) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)
    simp [phaseShiftMatrix, mul_apply, Fin.sum_univ_three, ← exp_add, mul_add]All goals completed! 🐙

Given three real numbers a b c the unitary matrix with exp (I * a) etc on the leading diagonal.


@[simps!]
def phaseShift (a b c : ℝ) : unitaryGroup (Fin 3) ℂ :=
  ⟨phaseShiftMatrix a b c,
  bya:ℝb:ℝc:ℝ⊢ phaseShiftMatrix a b c ∈ unitaryGroup (Fin 3) ℂ
    rw [mem_unitaryGroup_iffa:ℝb:ℝc:ℝ⊢ phaseShiftMatrix a b c * star (phaseShiftMatrix a b c) = 1a:ℝb:ℝc:ℝ⊢ phaseShiftMatrix a b c * star (phaseShiftMatrix a b c) = 1]a:ℝb:ℝc:ℝ⊢ phaseShiftMatrix a b c * star (phaseShiftMatrix a b c) = 1
    change _ * (phaseShiftMatrix a b c)ᴴ = 1a:ℝb:ℝc:ℝ⊢ phaseShiftMatrix a b c * (phaseShiftMatrix a b c)ᴴ = 1
    rw [phaseShiftMatrix_star,a:ℝb:ℝc:ℝ⊢ phaseShiftMatrix a b c * phaseShiftMatrix (-a) (-b) (-c) = 1a:ℝb:ℝc:ℝ⊢ phaseShiftMatrix (a + -a) (b + -b) (c + -c) = phaseShiftMatrix 0 0 0 phaseShiftMatrix_mul,a:ℝb:ℝc:ℝ⊢ phaseShiftMatrix (a + -a) (b + -b) (c + -c) = 1a:ℝb:ℝc:ℝ⊢ phaseShiftMatrix (a + -a) (b + -b) (c + -c) = phaseShiftMatrix 0 0 0 ← phaseShiftMatrix_onea:ℝb:ℝc:ℝ⊢ phaseShiftMatrix (a + -a) (b + -b) (c + -c) = phaseShiftMatrix 0 0 0a:ℝb:ℝc:ℝ⊢ phaseShiftMatrix (a + -a) (b + -b) (c + -c) = phaseShiftMatrix 0 0 0]a:ℝb:ℝc:ℝ⊢ phaseShiftMatrix (a + -a) (b + -b) (c + -c) = phaseShiftMatrix 0 0 0
    simp only [phaseShiftMatrix, add_neg_cancel, ofReal_zero, mul_zero, exp_zero]All goals completed! 🐙⟩

The underlying matrix of the phase-shift element of the unitary group is the phase-shift matrix.

lemma phaseShift_coe_matrix (a b c : ℝ) : ↑(phaseShift a b c) = phaseShiftMatrix a b c := rfl

The relation on unitary matrices (CKM matrices) satisfied if two unitary matrices are related by phase shifts of quarks.

def PhaseShiftRelation (U V : unitaryGroup (Fin 3) ℂ) : Prop :=
  ∃ a b c e f g, U = phaseShift a b c * V * phaseShift e f g

The relation PhaseShiftRelation is reflective.

lemma phaseShiftRelation_refl (U : unitaryGroup (Fin 3) ℂ) : PhaseShiftRelation U U := byU:↥(unitaryGroup (Fin 3) ℂ)⊢ PhaseShiftRelation U U
  refine ⟨0, 0, 0, 0, 0, 0, ?_⟩U:↥(unitaryGroup (Fin 3) ℂ)⊢ U = phaseShift 0 0 0 * U * phaseShift 0 0 0
  simp only [Subtype.ext_iff, Submonoid.coe_mul, phaseShift_coe_matrix, phaseShiftMatrix_one,
    one_mul, mul_one]All goals completed! 🐙

The relation PhaseShiftRelation is symmetric.

lemma phaseShiftRelation_symm {U V : unitaryGroup (Fin 3) ℂ} :
    PhaseShiftRelation U V → PhaseShiftRelation V U := byU:↥(unitaryGroup (Fin 3) ℂ)V:↥(unitaryGroup (Fin 3) ℂ)⊢ PhaseShiftRelation U V → PhaseShiftRelation V U
  rintro ⟨a, b, c, e, f, g, rfl⟩V:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ PhaseShiftRelation V (phaseShift a b c * V * phaseShift e f g)
  refine ⟨-a, -b, -c, -e, -f, -g, ?_⟩V:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ V = phaseShift (-a) (-b) (-c) * (phaseShift a b c * V * phaseShift e f g) * phaseShift (-e) (-f) (-g)
  simp only [Subtype.ext_iff, Submonoid.coe_mul, phaseShift_coe_matrix, mul_assoc,
    phaseShiftMatrix_mul, add_neg_cancel, phaseShiftMatrix_one, mul_one]V:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ↑V = phaseShiftMatrix (-a) (-b) (-c) * (phaseShiftMatrix a b c * ↑V)
  simp only [← mul_assoc, phaseShiftMatrix_mul, neg_add_cancel, phaseShiftMatrix_one, one_mul]All goals completed! 🐙

The relation PhaseShiftRelation is transitive.


lemma phaseShiftRelation_trans {U V W : unitaryGroup (Fin 3) ℂ} :
    PhaseShiftRelation U V → PhaseShiftRelation V W → PhaseShiftRelation U W := byU:↥(unitaryGroup (Fin 3) ℂ)V:↥(unitaryGroup (Fin 3) ℂ)W:↥(unitaryGroup (Fin 3) ℂ)⊢ PhaseShiftRelation U V → PhaseShiftRelation V W → PhaseShiftRelation U W
  rintro ⟨a, b, c, e, f, g, rfl⟩ ⟨d, i, j, k, l, m, rfl⟩W:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝd:ℝi:ℝj:ℝk:ℝl:ℝm:ℝ⊢ PhaseShiftRelation (phaseShift a b c * (phaseShift d i j * W * phaseShift k l m) * phaseShift e f g) W
  refine ⟨a + d, b + i, c + j, e + k, f + l, g + m, ?_⟩W:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝd:ℝi:ℝj:ℝk:ℝl:ℝm:ℝ⊢ phaseShift a b c * (phaseShift d i j * W * phaseShift k l m) * phaseShift e f g =
  phaseShift (a + d) (b + i) (c + j) * W * phaseShift (e + k) (f + l) (g + m)
  simp only [Subtype.ext_iff, Submonoid.coe_mul, phaseShift_coe_matrix]W:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝd:ℝi:ℝj:ℝk:ℝl:ℝm:ℝ⊢ phaseShiftMatrix a b c * (phaseShiftMatrix d i j * ↑W * phaseShiftMatrix k l m) * phaseShiftMatrix e f g =
  phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (e + k) (f + l) (g + m)
  rw [mul_assoc,W:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝd:ℝi:ℝj:ℝk:ℝl:ℝm:ℝ⊢ phaseShiftMatrix a b c * (phaseShiftMatrix d i j * ↑W * phaseShiftMatrix k l m * phaseShiftMatrix e f g) =
  phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (e + k) (f + l) (g + m)All goals completed! 🐙 mul_assoc,W:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝd:ℝi:ℝj:ℝk:ℝl:ℝm:ℝ⊢ phaseShiftMatrix a b c * (phaseShiftMatrix d i j * ↑W * (phaseShiftMatrix k l m * phaseShiftMatrix e f g)) =
  phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (e + k) (f + l) (g + m)All goals completed! 🐙 phaseShiftMatrix_mul,W:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝd:ℝi:ℝj:ℝk:ℝl:ℝm:ℝ⊢ phaseShiftMatrix a b c * (phaseShiftMatrix d i j * ↑W * phaseShiftMatrix (k + e) (l + f) (m + g)) =
  phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (e + k) (f + l) (g + m)All goals completed! 🐙 ← mul_assoc,W:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝd:ℝi:ℝj:ℝk:ℝl:ℝm:ℝ⊢ phaseShiftMatrix a b c * (phaseShiftMatrix d i j * ↑W) * phaseShiftMatrix (k + e) (l + f) (m + g) =
  phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (e + k) (f + l) (g + m)All goals completed! 🐙 ← mul_assoc,W:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝd:ℝi:ℝj:ℝk:ℝl:ℝm:ℝ⊢ phaseShiftMatrix a b c * phaseShiftMatrix d i j * ↑W * phaseShiftMatrix (k + e) (l + f) (m + g) =
  phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (e + k) (f + l) (g + m)All goals completed! 🐙 phaseShiftMatrix_mul,W:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝd:ℝi:ℝj:ℝk:ℝl:ℝm:ℝ⊢ phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (k + e) (l + f) (m + g) =
  phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (e + k) (f + l) (g + m)All goals completed! 🐙
    add_comm k e,W:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝd:ℝi:ℝj:ℝk:ℝl:ℝm:ℝ⊢ phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (e + k) (l + f) (m + g) =
  phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (e + k) (f + l) (g + m)All goals completed! 🐙 add_comm l f,W:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝd:ℝi:ℝj:ℝk:ℝl:ℝm:ℝ⊢ phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (e + k) (f + l) (m + g) =
  phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (e + k) (f + l) (g + m)All goals completed! 🐙 add_comm m gW:↥(unitaryGroup (Fin 3) ℂ)a:ℝb:ℝc:ℝe:ℝf:ℝg:ℝd:ℝi:ℝj:ℝk:ℝl:ℝm:ℝ⊢ phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (e + k) (f + l) (g + m) =
  phaseShiftMatrix (a + d) (b + i) (c + j) * ↑W * phaseShiftMatrix (e + k) (f + l) (g + m)All goals completed! 🐙]All goals completed! 🐙

The relation PhaseShiftRelation is an equivalence relation.

lemma phaseShiftRelation_equiv : Equivalence PhaseShiftRelation where
  refl := phaseShiftRelation_refl
  symm := phaseShiftRelation_symm
  trans := phaseShiftRelation_trans

The type of CKM matrices.

def CKMMatrix : Type := unitaryGroup (Fin 3) ℂ

Two CKM matrices are equal if their underlying unitary matrices are equal.

lemma CKMMatrix_ext {U V : CKMMatrix} (h : U.val = V.val) : U = V := Subtype.ext h

The udth element of the CKM matrix.

scoped[CKMMatrix] notation (name := ud_element) "[" V "]ud" => V.1 0 0

The usth element of the CKM matrix.

scoped[CKMMatrix] notation (name := us_element) "[" V "]us" => V.1 0 1

The ubth element of the CKM matrix.

scoped[CKMMatrix] notation (name := ub_element) "[" V "]ub" => V.1 0 2

The cdth element of the CKM matrix.

scoped[CKMMatrix] notation (name := cd_element) "[" V "]cd" => V.1 1 0

The csth element of the CKM matrix.

scoped[CKMMatrix] notation (name := cs_element) "[" V "]cs" => V.1 1 1

The cbth element of the CKM matrix.

scoped[CKMMatrix] notation (name := cb_element) "[" V "]cb" => V.1 1 2

The tdth element of the CKM matrix.

scoped[CKMMatrix] notation (name := td_element) "[" V "]td" => V.1 2 0

The tsth element of the CKM matrix.

scoped[CKMMatrix] notation (name := ts_element) "[" V "]ts" => V.1 2 1

The tbth element of the CKM matrix.

scoped[CKMMatrix] notation (name := tb_element) "[" V "]tb" => V.1 2 2

The setoid of CKM matrices defined by phase shifts of fermions.

instance CKMMatrixSetoid : Setoid CKMMatrix := ⟨PhaseShiftRelation, phaseShiftRelation_equiv⟩

The matrix obtained from V by shifting the phases of the fermions.

@[simps!]
def phaseShiftApply (V : CKMMatrix) (a b c d e f : ℝ) : CKMMatrix :=
    phaseShift a b c * ↑V * phaseShift d e f

A CKM matrix is equivalent to a phase-shift of itself.

lemma equiv (V : CKMMatrix) (a b c d e f : ℝ) :
    V ≈ phaseShiftApply V a b c d e f := byV:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ V ≈ phaseShiftApply V a b c d e f
  symmV:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ phaseShiftApply V a b c d e f ≈ V
  exact ⟨a, b, c, d, e, f, rfl⟩All goals completed! 🐙

The ud component of the CKM matrix obtained after applying a phase shift.

lemma ud (V : CKMMatrix) (a b c d e f : ℝ) :
    (phaseShiftApply V a b c d e f).1 0 0 = cexp (a * I + d * I) * V.1 0 0 := byV:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ ↑(phaseShiftApply V a b c d e f) 0 0 = cexp (↑a * I + ↑d * I) * ↑V 0 0
  simp only [Fin.isValue, phaseShiftApply_coe, mul_apply, cons_val', cons_val_fin_one,
    cons_val_zero, Fin.sum_univ_three, cons_val_one, zero_mul, add_zero, cons_val, mul_zero,
    exp_add]V:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ cexp (I * ↑a) * ↑V 0 0 * cexp (I * ↑d) = cexp (↑a * I) * cexp (↑d * I) * ↑V 0 0
  ring_nfAll goals completed! 🐙

The us component of the CKM matrix obtained after applying a phase shift.

lemma us (V : CKMMatrix) (a b c d e f : ℝ) :
    (phaseShiftApply V a b c d e f).1 0 1 = cexp (a * I + e * I) * V.1 0 1 := byV:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ ↑(phaseShiftApply V a b c d e f) 0 1 = cexp (↑a * I + ↑e * I) * ↑V 0 1
  simp only [Fin.isValue, phaseShiftApply_coe, mul_apply, cons_val', cons_val_fin_one,
    cons_val_zero, Fin.sum_univ_three, cons_val_one, zero_mul, add_zero, cons_val, mul_zero,
    zero_add, exp_add]V:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ cexp (I * ↑a) * ↑V 0 1 * cexp (I * ↑e) = cexp (↑a * I) * cexp (↑e * I) * ↑V 0 1
  ring_nfAll goals completed! 🐙

The ub component of the CKM matrix obtained after applying a phase shift.

lemma ub (V : CKMMatrix) (a b c d e f : ℝ) :
    (phaseShiftApply V a b c d e f).1 0 2 = cexp (a * I + f * I) * V.1 0 2 := byV:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ ↑(phaseShiftApply V a b c d e f) 0 2 = cexp (↑a * I + ↑f * I) * ↑V 0 2
  simp only [Fin.isValue, phaseShiftApply_coe, mul_apply, cons_val', cons_val_fin_one,
    cons_val_zero, Fin.sum_univ_three, cons_val_one, zero_mul, add_zero, cons_val, mul_zero,
    zero_add, exp_add]V:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ cexp (I * ↑a) * ↑V 0 2 * cexp (I * ↑f) = cexp (↑a * I) * cexp (↑f * I) * ↑V 0 2
  ring_nfAll goals completed! 🐙

The cd component of the CKM matrix obtained after applying a phase shift.

lemma cd (V : CKMMatrix) (a b c d e f : ℝ) :
    (phaseShiftApply V a b c d e f).1 1 0= cexp (b * I + d * I) * V.1 1 0 := byV:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ ↑(phaseShiftApply V a b c d e f) 1 0 = cexp (↑b * I + ↑d * I) * ↑V 1 0
  simp only [Fin.isValue, phaseShiftApply_coe, mul_apply, cons_val', cons_val_fin_one, cons_val_one,
    cons_val_zero, Fin.sum_univ_three, zero_mul, zero_add, cons_val, add_zero, mul_zero, exp_add]V:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ cexp (I * ↑b) * ↑V 1 0 * cexp (I * ↑d) = cexp (↑b * I) * cexp (↑d * I) * ↑V 1 0
  ring_nfAll goals completed! 🐙

The cs component of the CKM matrix obtained after applying a phase shift.

lemma cs (V : CKMMatrix) (a b c d e f : ℝ) :
    (phaseShiftApply V a b c d e f).1 1 1 = cexp (b * I + e * I) * V.1 1 1 := byV:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ ↑(phaseShiftApply V a b c d e f) 1 1 = cexp (↑b * I + ↑e * I) * ↑V 1 1
  simp only [Fin.isValue, phaseShiftApply_coe, mul_apply, cons_val', cons_val_fin_one, cons_val_one,
    cons_val_zero, Fin.sum_univ_three, zero_mul, zero_add, cons_val, add_zero, mul_zero, exp_add]V:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ cexp (I * ↑b) * ↑V 1 1 * cexp (I * ↑e) = cexp (↑b * I) * cexp (↑e * I) * ↑V 1 1
  ring_nfAll goals completed! 🐙

The cb component of the CKM matrix obtained after applying a phase shift.

lemma cb (V : CKMMatrix) (a b c d e f : ℝ) :
    (phaseShiftApply V a b c d e f).1 1 2 = cexp (b * I + f * I) * V.1 1 2 := byV:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ ↑(phaseShiftApply V a b c d e f) 1 2 = cexp (↑b * I + ↑f * I) * ↑V 1 2
  simp only [Fin.isValue, phaseShiftApply_coe, mul_apply, cons_val', cons_val_fin_one, cons_val_one,
    cons_val_zero, Fin.sum_univ_three, zero_mul, zero_add, cons_val, add_zero, mul_zero, exp_add]V:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ cexp (I * ↑b) * ↑V 1 2 * cexp (I * ↑f) = cexp (↑b * I) * cexp (↑f * I) * ↑V 1 2
  ring_nfAll goals completed! 🐙

The td component of the CKM matrix obtained after applying a phase shift.

lemma td (V : CKMMatrix) (a b c d e f : ℝ) :
    (phaseShiftApply V a b c d e f).1 2 0= cexp (c * I + d * I) * V.1 2 0 := byV:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ ↑(phaseShiftApply V a b c d e f) 2 0 = cexp (↑c * I + ↑d * I) * ↑V 2 0
  simp only [Fin.isValue, phaseShiftApply_coe, mul_apply, cons_val', cons_val_fin_one, cons_val,
    cons_val_one, Fin.sum_univ_three, cons_val_zero, zero_mul, add_zero, zero_add, mul_zero,
    exp_add]V:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ cexp (I * ↑c) * ↑V 2 0 * cexp (I * ↑d) = cexp (↑c * I) * cexp (↑d * I) * ↑V 2 0
  ring_nfAll goals completed! 🐙

The ts component of the CKM matrix obtained after applying a phase shift.

lemma ts (V : CKMMatrix) (a b c d e f : ℝ) :
    (phaseShiftApply V a b c d e f).1 2 1 = cexp (c * I + e * I) * V.1 2 1 := byV:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ ↑(phaseShiftApply V a b c d e f) 2 1 = cexp (↑c * I + ↑e * I) * ↑V 2 1
  simp only [Fin.isValue, phaseShiftApply_coe, mul_apply, cons_val', cons_val_fin_one, cons_val,
    cons_val_one, Fin.sum_univ_three, cons_val_zero, zero_mul, add_zero, zero_add, mul_zero,
    exp_add]V:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ cexp (I * ↑c) * ↑V 2 1 * cexp (I * ↑e) = cexp (↑c * I) * cexp (↑e * I) * ↑V 2 1
  ring_nfAll goals completed! 🐙

The tb component of the CKM matrix obtained after applying a phase shift.

lemma tb (V : CKMMatrix) (a b c d e f : ℝ) :
    (phaseShiftApply V a b c d e f).1 2 2 = cexp (c * I + f * I) * V.1 2 2 := byV:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ ↑(phaseShiftApply V a b c d e f) 2 2 = cexp (↑c * I + ↑f * I) * ↑V 2 2
  simp only [Fin.isValue, phaseShiftApply_coe, mul_apply, cons_val', cons_val_fin_one, cons_val,
    cons_val_one, Fin.sum_univ_three, cons_val_zero, zero_mul, add_zero, zero_add, mul_zero,
    exp_add]V:CKMMatrixa:ℝb:ℝc:ℝd:ℝe:ℝf:ℝ⊢ cexp (I * ↑c) * ↑V 2 2 * cexp (I * ↑f) = cexp (↑c * I) * cexp (↑f * I) * ↑V 2 2
  ring_nfAll goals completed! 🐙

The absolute value of the (i,j)th element of V.

@[simp]
def VAbs' (V : unitaryGroup (Fin 3) ℂ) (i j : Fin 3) : ℝ := norm (V i j)

If two CKM matrices are equivalent (under phase shifts), then their absolute values are the same.

lemma VAbs'_equiv (i j : Fin 3) (V U : CKMMatrix) (h : V ≈ U) :
    VAbs' V i j = VAbs' U i j := byi:Fin 3j:Fin 3V:CKMMatrixU:CKMMatrixh:V ≈ U⊢ VAbs' V i j = VAbs' U i j
  obtain ⟨a, b, c, e, f, g, rfl⟩ := hi:Fin 3j:Fin 3U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ VAbs' (phaseShift a b c * U * phaseShift e f g) i j = VAbs' U i j
  simp only [VAbs', Submonoid.coe_mul, phaseShift_coe_matrix, phaseShiftMatrix, mul_apply,
    Fin.sum_univ_three]i:Fin 3j:Fin 3U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] i 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] i 1 * ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] i 2 * ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 j +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] i 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] i 1 * ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] i 2 * ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 j +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] i 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] i 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] i 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 j‖ =
  ‖↑U i j‖
  fin_cases i«0»j:Fin 3U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 j +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 j +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 j‖ =
  ‖↑U ((fun i => i) ⟨0, ⋯⟩) j‖«1»j:Fin 3U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 j +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 j +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 j‖ =
  ‖↑U ((fun i => i) ⟨1, ⋯⟩) j‖«2»j:Fin 3U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 j +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 j +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 j‖ =
  ‖↑U ((fun i => i) ⟨2, ⋯⟩) j‖ <;>«0»j:Fin 3U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 j +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 j +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 j‖ =
  ‖↑U ((fun i => i) ⟨0, ⋯⟩) j‖«1»j:Fin 3U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 j +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 j +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 j‖ =
  ‖↑U ((fun i => i) ⟨1, ⋯⟩) j‖«2»j:Fin 3U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 j +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 j +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 j‖ =
  ‖↑U ((fun i => i) ⟨2, ⋯⟩) j‖ fin_cases j«2».«0»U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 ((fun i => i) ⟨0, ⋯⟩) +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 ((fun i => i) ⟨0, ⋯⟩) +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 ((fun i => i) ⟨0, ⋯⟩)‖ =
  ‖↑U ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)‖«2».«1»U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 ((fun i => i) ⟨1, ⋯⟩) +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 ((fun i => i) ⟨1, ⋯⟩) +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 ((fun i => i) ⟨1, ⋯⟩)‖ =
  ‖↑U ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)‖«2».«2»U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 ((fun i => i) ⟨2, ⋯⟩) +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 ((fun i => i) ⟨2, ⋯⟩) +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 ((fun i => i) ⟨2, ⋯⟩)‖ =
  ‖↑U ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)‖ <;>«0».«0»U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 ((fun i => i) ⟨0, ⋯⟩) +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 ((fun i => i) ⟨0, ⋯⟩) +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 ((fun i => i) ⟨0, ⋯⟩)‖ =
  ‖↑U ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)‖«0».«1»U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 ((fun i => i) ⟨1, ⋯⟩) +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 ((fun i => i) ⟨1, ⋯⟩) +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 ((fun i => i) ⟨1, ⋯⟩)‖ =
  ‖↑U ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)‖«0».«2»U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 ((fun i => i) ⟨2, ⋯⟩) +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 ((fun i => i) ⟨2, ⋯⟩) +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨0, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 ((fun i => i) ⟨2, ⋯⟩)‖ =
  ‖↑U ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)‖«1».«0»U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 ((fun i => i) ⟨0, ⋯⟩) +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 ((fun i => i) ⟨0, ⋯⟩) +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 ((fun i => i) ⟨0, ⋯⟩)‖ =
  ‖↑U ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)‖«1».«1»U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 ((fun i => i) ⟨1, ⋯⟩) +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 ((fun i => i) ⟨1, ⋯⟩) +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 ((fun i => i) ⟨1, ⋯⟩)‖ =
  ‖↑U ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)‖«1».«2»U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 ((fun i => i) ⟨2, ⋯⟩) +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 ((fun i => i) ⟨2, ⋯⟩) +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨1, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 ((fun i => i) ⟨2, ⋯⟩)‖ =
  ‖↑U ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)‖«2».«0»U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 ((fun i => i) ⟨0, ⋯⟩) +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 ((fun i => i) ⟨0, ⋯⟩) +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 ((fun i => i) ⟨0, ⋯⟩)‖ =
  ‖↑U ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)‖«2».«1»U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 ((fun i => i) ⟨1, ⋯⟩) +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 ((fun i => i) ⟨1, ⋯⟩) +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 ((fun i => i) ⟨1, ⋯⟩)‖ =
  ‖↑U ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)‖«2».«2»U:CKMMatrixa:ℝb:ℝc:ℝe:ℝf:ℝg:ℝ⊢ ‖(![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 0 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 0 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 0) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 0 ((fun i => i) ⟨2, ⋯⟩) +
        (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 1 +
              ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 *
                ↑U 1 1 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 *
              ↑U 2 1) *
          ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 1 ((fun i => i) ⟨2, ⋯⟩) +
      (![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 0 * ↑U 0 2 +
            ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 1 * ↑U 1 2 +
          ![![cexp (I * ↑a), 0, 0], ![0, cexp (I * ↑b), 0], ![0, 0, cexp (I * ↑c)]] ((fun i => i) ⟨2, ⋯⟩) 2 * ↑U 2 2) *
        ![![cexp (I * ↑e), 0, 0], ![0, cexp (I * ↑f), 0], ![0, 0, cexp (I * ↑g)]] 2 ((fun i => i) ⟨2, ⋯⟩)‖ =
  ‖↑U ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)‖
    simp [Complex.norm_exp, mul_comm]All goals completed! 🐙

The absolute value of the (i,j)th any representative of ⟦V⟧.

def VAbs (i j : Fin 3) : Quotient CKMMatrixSetoid → ℝ :=
  Quotient.lift (fun V => VAbs' V i j) (VAbs'_equiv i j)

The absolute value of the udth element of a representative of an equivalence class of CKM matrices.

@[simp]
abbrev VudAbs := VAbs 0 0

The absolute value of the usth element of a representative of an equivalence class of CKM matrices.

@[simp]
abbrev VusAbs := VAbs 0 1

The absolute value of the ubth element of a representative of an equivalence class of CKM matrices.

@[simp]
abbrev VubAbs := VAbs 0 2

The absolute value of the cdth element of a representative of an equivalence class of CKM matrices.

@[simp]
abbrev VcdAbs := VAbs 1 0

The absolute value of the csth element of a representative of an equivalence class of CKM matrices.

@[simp]
abbrev VcsAbs := VAbs 1 1

The absolute value of the cbth element of a representative of an equivalence class of CKM matrices.

@[simp]
abbrev VcbAbs := VAbs 1 2

The absolute value of the tdth element of a representative of an equivalence class of CKM matrices.

@[simp]
abbrev VtdAbs := VAbs 2 0

The absolute value of the tsth element of a representative of an equivalence class of CKM matrices.

@[simp]
abbrev VtsAbs := VAbs 2 1

The absolute value of the tbth element of a representative of an equivalence class of CKM matrices.

@[simp]
abbrev VtbAbs := VAbs 2 2

The ratio of the ub and ud elements of a CKM matrix.

def Rubud (V : CKMMatrix) : ℂ := [V]ub / [V]ud

The ratio of the ub and ud elements of a CKM matrix.

scoped[CKMMatrix] notation (name := ub_ud_ratio) "[" V "]ub|ud" => Rubud V

The ratio of the us and ud elements of a CKM matrix.

def Rusud (V : CKMMatrix) : ℂ := [V]us / [V]ud

The ratio of the us and ud elements of a CKM matrix.

scoped[CKMMatrix] notation (name := us_ud_ratio) "[" V "]us|ud" => Rusud V

The ratio of the ud and us elements of a CKM matrix.

def Rudus (V : CKMMatrix) : ℂ := [V]ud / [V]us

The ratio of the ud and us elements of a CKM matrix.

scoped[CKMMatrix] notation (name := ud_us_ratio) "[" V "]ud|us" => Rudus V

The ratio of the ub and us elements of a CKM matrix.

def Rubus (V : CKMMatrix) : ℂ := [V]ub / [V]us

The ratio of the ub and us elements of a CKM matrix.

scoped[CKMMatrix] notation (name := ub_us_ratio) "[" V "]ub|us" => Rubus V

The ratio of the cd and cb elements of a CKM matrix.

def Rcdcb (V : CKMMatrix) : ℂ := [V]cd / [V]cb

The ratio of the cd and cb elements of a CKM matrix.

scoped[CKMMatrix] notation (name := cd_cb_ratio) "[" V "]cd|cb" => Rcdcb V

lemma Rcdcb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0) : [V]cd = Rcdcb V * [V]cb :=
  (div_mul_cancel₀ (V.1 1 0) h).symm

The ratio of the cs and cb elements of a CKM matrix.

def Rcscb (V : CKMMatrix) : ℂ := [V]cs / [V]cb

The ratio of the cs and cb elements of a CKM matrix.

scoped[CKMMatrix] notation (name := cs_cb_ratio) "[" V "]cs|cb" => Rcscb V

Multiplying the ratio of the cs by cb element of a CKM matrix by the cb element returns the cs element, as long as the cb element is non-zero.

lemma Rcscb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0) : [V]cs = Rcscb V * [V]cb :=
  (div_mul_cancel₀ [V]cs h).symm