1. Physlib
  2. Particles
  3. FlavorPhysics
  4. CKMMatrix
  5. Rows
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.Particles.FlavorPhysics.CKMMatrix.Basic public import Mathlib.Analysis.SpecialFunctions.Complex.Arg public import Mathlib.LinearAlgebra.CrossProduct public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas public import Mathlib.Tactic.Cases

Rows for the CKM Matrix

This file contains the definition extracting the rows of the CKM matrix and proves some properties between them.

The first row can be extracted as [V]u for a CKM matrix V.

@[expose] public section

The uth row of the CKM matrix.

def uRow (V : CKMMatrix) : Fin 3 → ℂ := ![[V]ud, [V]us, [V]ub]

The uth row of the CKM matrix.

scoped[CKMMatrix] notation (name := u_row) "[" V "]u" => uRow V

The cth row of the CKM matrix.

def cRow (V : CKMMatrix) : Fin 3 → ℂ := ![[V]cd, [V]cs, [V]cb]

The cth row of the CKM matrix.

scoped[CKMMatrix] notation (name := c_row) "[" V "]c" => cRow V

The tth row of the CKM matrix.

def tRow (V : CKMMatrix) : Fin 3 → ℂ := ![[V]td, [V]ts, [V]tb]

The tth row of the CKM matrix.

scoped[CKMMatrix] notation (name := t_row) "[" V "]t" => tRow V

The up-quark row of the CKM matrix is normalized to 1.

V:CKMMatrixht:↑V 0 0 * (starRingEnd ℂ) (↑V 0 0) + ↑V 0 1 * (starRingEnd ℂ) (↑V 0 1) + ↑V 0 2 * (starRingEnd ℂ) (↑V 0 2) = 1⊢ (starRingEnd ℂ) (↑V 0 0) * ↑V 0 0 + (starRingEnd ℂ) (↑V 0 1) * ↑V 0 1 + (starRingEnd ℂ) (↑V 0 2) * ↑V 0 2 = 1 All goals completed! 🐙

The charm-quark row of the CKM matrix is normalized to 1.

V:CKMMatrixht:↑V 1 0 * (starRingEnd ℂ) (↑V 1 0) + ↑V 1 1 * (starRingEnd ℂ) (↑V 1 1) + ↑V 1 2 * (starRingEnd ℂ) (↑V 1 2) = 1⊢ (starRingEnd ℂ) (↑V 1 0) * ↑V 1 0 + (starRingEnd ℂ) (↑V 1 1) * ↑V 1 1 + (starRingEnd ℂ) (↑V 1 2) * ↑V 1 2 = 1 All goals completed! 🐙

The top-quark row of the CKM matrix is normalized to 1.

V:CKMMatrixht:↑V 2 0 * (starRingEnd ℂ) (↑V 2 0) + ↑V 2 1 * (starRingEnd ℂ) (↑V 2 1) + ↑V 2 2 * (starRingEnd ℂ) (↑V 2 2) = 1⊢ (starRingEnd ℂ) (↑V 2 0) * ↑V 2 0 + (starRingEnd ℂ) (↑V 2 1) * ↑V 2 1 + (starRingEnd ℂ) (↑V 2 2) * ↑V 2 2 = 1 All goals completed! 🐙

The up-quark row of the CKM matrix is orthogonal to the charm-quark row.

V:CKMMatrixht:↑V 1 0 * (starRingEnd ℂ) (↑V 0 0) + ↑V 1 1 * (starRingEnd ℂ) (↑V 0 1) + ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) = 0⊢ (starRingEnd ℂ) (↑V 0 0) * ↑V 1 0 + (starRingEnd ℂ) (↑V 0 1) * ↑V 1 1 + (starRingEnd ℂ) (↑V 0 2) * ↑V 1 2 = 0 All goals completed! 🐙

The up-quark row of the CKM matrix is orthogonal to the top-quark row.

V:CKMMatrixht:↑V 2 0 * (starRingEnd ℂ) (↑V 0 0) + ↑V 2 1 * (starRingEnd ℂ) (↑V 0 1) + ↑V 2 2 * (starRingEnd ℂ) (↑V 0 2) = 0⊢ (starRingEnd ℂ) (↑V 0 0) * ↑V 2 0 + (starRingEnd ℂ) (↑V 0 1) * ↑V 2 1 + (starRingEnd ℂ) (↑V 0 2) * ↑V 2 2 = 0 All goals completed! 🐙

The charm-quark row of the CKM matrix is orthogonal to the up-quark row.

V:CKMMatrixht:↑V 0 0 * (starRingEnd ℂ) (↑V 1 0) + ↑V 0 1 * (starRingEnd ℂ) (↑V 1 1) + ↑V 0 2 * (starRingEnd ℂ) (↑V 1 2) = 0⊢ (starRingEnd ℂ) (↑V 1 0) * ↑V 0 0 + (starRingEnd ℂ) (↑V 1 1) * ↑V 0 1 + (starRingEnd ℂ) (↑V 1 2) * ↑V 0 2 = 0 All goals completed! 🐙

The charm-quark row of the CKM matrix is orthogonal to the top-quark row.

V:CKMMatrixht:↑V 2 0 * (starRingEnd ℂ) (↑V 1 0) + ↑V 2 1 * (starRingEnd ℂ) (↑V 1 1) + ↑V 2 2 * (starRingEnd ℂ) (↑V 1 2) = 0⊢ (starRingEnd ℂ) (↑V 1 0) * ↑V 2 0 + (starRingEnd ℂ) (↑V 1 1) * ↑V 2 1 + (starRingEnd ℂ) (↑V 1 2) * ↑V 2 2 = 0 All goals completed! 🐙

The top-quark row of the CKM matrix is orthogonal to the up-quark row.

V:CKMMatrixht:↑V 0 0 * (starRingEnd ℂ) (↑V 2 0) + ↑V 0 1 * (starRingEnd ℂ) (↑V 2 1) + ↑V 0 2 * (starRingEnd ℂ) (↑V 2 2) = 0⊢ (starRingEnd ℂ) (↑V 2 0) * ↑V 0 0 + (starRingEnd ℂ) (↑V 2 1) * ↑V 0 1 + (starRingEnd ℂ) (↑V 2 2) * ↑V 0 2 = 0 All goals completed! 🐙

The top-quark row of the CKM matrix is orthogonal to the charm-quark row.

V:CKMMatrixht:↑V 1 0 * (starRingEnd ℂ) (↑V 2 0) + ↑V 1 1 * (starRingEnd ℂ) (↑V 2 1) + ↑V 1 2 * (starRingEnd ℂ) (↑V 2 2) = 0⊢ (starRingEnd ℂ) (↑V 2 0) * ↑V 1 0 + (starRingEnd ℂ) (↑V 2 1) * ↑V 1 1 + (starRingEnd ℂ) (↑V 2 2) * ↑V 1 2 = 0 All goals completed! 🐙
lemma uRow_cross_cRow_conj (V : CKMMatrix) : conj (conj [V]u ⨯₃ conj [V]c) = [V]u ⨯₃ [V]c := V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ((crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)) = (crossProduct [V]u) [V]c V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 2) - (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 1), (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 0) - (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 2), (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 1) - (starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 0)] = ![[V]u 1 * [V]c 2 - [V]u 2 * [V]c 1, [V]u 2 * [V]c 0 - [V]u 0 * [V]c 2, [V]u 0 * [V]c 1 - [V]u 1 * [V]c 0] V:CKMMatrixi:Fin 3⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 2) - (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 1), (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 0) - (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 2), (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 1) - (starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 0)] i = ![[V]u 1 * [V]c 2 - [V]u 2 * [V]c 1, [V]u 2 * [V]c 0 - [V]u 0 * [V]c 2, [V]u 0 * [V]c 1 - [V]u 1 * [V]c 0] i V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 2) - (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 1), (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 0) - (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 2), (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 1) - (starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 0)] ((fun i => i) ⟨0, ⋯⟩) = ![[V]u 1 * [V]c 2 - [V]u 2 * [V]c 1, [V]u 2 * [V]c 0 - [V]u 0 * [V]c 2, [V]u 0 * [V]c 1 - [V]u 1 * [V]c 0] ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 2) - (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 1), (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 0) - (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 2), (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 1) - (starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 0)] ((fun i => i) ⟨1, ⋯⟩) = ![[V]u 1 * [V]c 2 - [V]u 2 * [V]c 1, [V]u 2 * [V]c 0 - [V]u 0 * [V]c 2, [V]u 0 * [V]c 1 - [V]u 1 * [V]c 0] ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 2) - (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 1), (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 0) - (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 2), (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 1) - (starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 0)] ((fun i => i) ⟨2, ⋯⟩) = ![[V]u 1 * [V]c 2 - [V]u 2 * [V]c 1, [V]u 2 * [V]c 0 - [V]u 0 * [V]c 2, [V]u 0 * [V]c 1 - [V]u 1 * [V]c 0] ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 2) - (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 1), (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 0) - (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 2), (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 1) - (starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 0)] ((fun i => i) ⟨0, ⋯⟩) = ![[V]u 1 * [V]c 2 - [V]u 2 * [V]c 1, [V]u 2 * [V]c 0 - [V]u 0 * [V]c 2, [V]u 0 * [V]c 1 - [V]u 1 * [V]c 0] ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 2) - (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 1), (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 0) - (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 2), (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 1) - (starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 0)] ((fun i => i) ⟨1, ⋯⟩) = ![[V]u 1 * [V]c 2 - [V]u 2 * [V]c 1, [V]u 2 * [V]c 0 - [V]u 0 * [V]c 2, [V]u 0 * [V]c 1 - [V]u 1 * [V]c 0] ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 2) - (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 1), (starRingEnd ℂ) ([V]u 2) * (starRingEnd ℂ) ([V]c 0) - (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 2), (starRingEnd ℂ) ([V]u 0) * (starRingEnd ℂ) ([V]c 1) - (starRingEnd ℂ) ([V]u 1) * (starRingEnd ℂ) ([V]c 0)] ((fun i => i) ⟨2, ⋯⟩) = ![[V]u 1 * [V]c 2 - [V]u 2 * [V]c 1, [V]u 2 * [V]c 0 - [V]u 0 * [V]c 2, [V]u 0 * [V]c 1 - [V]u 1 * [V]c 0] ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙lemma cRow_cross_tRow_conj (V : CKMMatrix) : conj (conj [V]c ⨯₃ conj [V]t) = [V]c ⨯₃ [V]t := V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ((crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]c)) ((starRingEnd (Fin 3 → ℂ)) [V]t)) = (crossProduct [V]c) [V]t V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 2) - (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 1), (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 0) - (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 2), (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 1) - (starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 0)] = ![[V]c 1 * [V]t 2 - [V]c 2 * [V]t 1, [V]c 2 * [V]t 0 - [V]c 0 * [V]t 2, [V]c 0 * [V]t 1 - [V]c 1 * [V]t 0] V:CKMMatrixi:Fin 3⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 2) - (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 1), (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 0) - (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 2), (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 1) - (starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 0)] i = ![[V]c 1 * [V]t 2 - [V]c 2 * [V]t 1, [V]c 2 * [V]t 0 - [V]c 0 * [V]t 2, [V]c 0 * [V]t 1 - [V]c 1 * [V]t 0] i V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 2) - (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 1), (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 0) - (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 2), (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 1) - (starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 0)] ((fun i => i) ⟨0, ⋯⟩) = ![[V]c 1 * [V]t 2 - [V]c 2 * [V]t 1, [V]c 2 * [V]t 0 - [V]c 0 * [V]t 2, [V]c 0 * [V]t 1 - [V]c 1 * [V]t 0] ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 2) - (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 1), (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 0) - (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 2), (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 1) - (starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 0)] ((fun i => i) ⟨1, ⋯⟩) = ![[V]c 1 * [V]t 2 - [V]c 2 * [V]t 1, [V]c 2 * [V]t 0 - [V]c 0 * [V]t 2, [V]c 0 * [V]t 1 - [V]c 1 * [V]t 0] ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 2) - (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 1), (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 0) - (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 2), (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 1) - (starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 0)] ((fun i => i) ⟨2, ⋯⟩) = ![[V]c 1 * [V]t 2 - [V]c 2 * [V]t 1, [V]c 2 * [V]t 0 - [V]c 0 * [V]t 2, [V]c 0 * [V]t 1 - [V]c 1 * [V]t 0] ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 2) - (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 1), (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 0) - (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 2), (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 1) - (starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 0)] ((fun i => i) ⟨0, ⋯⟩) = ![[V]c 1 * [V]t 2 - [V]c 2 * [V]t 1, [V]c 2 * [V]t 0 - [V]c 0 * [V]t 2, [V]c 0 * [V]t 1 - [V]c 1 * [V]t 0] ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 2) - (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 1), (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 0) - (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 2), (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 1) - (starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 0)] ((fun i => i) ⟨1, ⋯⟩) = ![[V]c 1 * [V]t 2 - [V]c 2 * [V]t 1, [V]c 2 * [V]t 0 - [V]c 0 * [V]t 2, [V]c 0 * [V]t 1 - [V]c 1 * [V]t 0] ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrix⊢ (starRingEnd (Fin 3 → ℂ)) ![(starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 2) - (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 1), (starRingEnd ℂ) ([V]c 2) * (starRingEnd ℂ) ([V]t 0) - (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 2), (starRingEnd ℂ) ([V]c 0) * (starRingEnd ℂ) ([V]t 1) - (starRingEnd ℂ) ([V]c 1) * (starRingEnd ℂ) ([V]t 0)] ((fun i => i) ⟨2, ⋯⟩) = ![[V]c 1 * [V]t 2 - [V]c 2 * [V]t 1, [V]c 2 * [V]t 0 - [V]c 0 * [V]t 2, [V]c 0 * [V]t 1 - [V]c 1 * [V]t 0] ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙V:CKMMatrix⊢ 1 * 1 - 0 * 0 = 1 All goals completed! 🐙V:CKMMatrix⊢ 1 * 1 - 0 * 0 = 1 All goals completed! 🐙

A map from Fin 3 to each row of a CKM matrix.

@[simp] def rows (V : CKMMatrix) : Fin 3 → Fin 3 → ℂ := fun i => match i with | 0 => uRow V | 1 => cRow V | 2 => tRow V

The rows of a CKM matrix are linearly independent.

V:CKMMatrixg:Fin 3 → ℂhg:g 0 • [V]u + g 1 • [V]c + g 2 • [V]t = 0h0:g 0 * 1 + g 1 * 0 + g 2 * 0 = 0h1:g 0 * 0 + g 1 * 1 + g 2 * 0 = 0h2:g 0 * 0 + g 1 * 0 + g 2 * 1 = 0⊢ ∀ (i : Fin 3), g i = 0 V:CKMMatrixg:Fin 3 → ℂhg:g 0 • [V]u + g 1 • [V]c + g 2 • [V]t = 0h0:g 0 = 0h1:g 1 = 0h2:g 2 = 0⊢ ∀ (i : Fin 3), g i = 0 V:CKMMatrixg:Fin 3 → ℂhg:g 0 • [V]u + g 1 • [V]c + g 2 • [V]t = 0h0:g 0 = 0h1:g 1 = 0h2:g 2 = 0i:Fin 3⊢ g i = 0 V:CKMMatrixg:Fin 3 → ℂhg:g 0 • [V]u + g 1 • [V]c + g 2 • [V]t = 0h0:g 0 = 0h1:g 1 = 0h2:g 2 = 0⊢ g ((fun i => i) ⟨0, ⋯⟩) = 0V:CKMMatrixg:Fin 3 → ℂhg:g 0 • [V]u + g 1 • [V]c + g 2 • [V]t = 0h0:g 0 = 0h1:g 1 = 0h2:g 2 = 0⊢ g ((fun i => i) ⟨1, ⋯⟩) = 0V:CKMMatrixg:Fin 3 → ℂhg:g 0 • [V]u + g 1 • [V]c + g 2 • [V]t = 0h0:g 0 = 0h1:g 1 = 0h2:g 2 = 0⊢ g ((fun i => i) ⟨2, ⋯⟩) = 0 V:CKMMatrixg:Fin 3 → ℂhg:g 0 • [V]u + g 1 • [V]c + g 2 • [V]t = 0h0:g 0 = 0h1:g 1 = 0h2:g 2 = 0⊢ g ((fun i => i) ⟨0, ⋯⟩) = 0V:CKMMatrixg:Fin 3 → ℂhg:g 0 • [V]u + g 1 • [V]c + g 2 • [V]t = 0h0:g 0 = 0h1:g 1 = 0h2:g 2 = 0⊢ g ((fun i => i) ⟨1, ⋯⟩) = 0V:CKMMatrixg:Fin 3 → ℂhg:g 0 • [V]u + g 1 • [V]c + g 2 • [V]t = 0h0:g 0 = 0h1:g 1 = 0h2:g 2 = 0⊢ g ((fun i => i) ⟨2, ⋯⟩) = 0 All goals completed! 🐙

The rows of a CKM matrix as a basis of ℂ³.

@[simps!] noncomputable def rowBasis (V : CKMMatrix) : Basis (Fin 3) ℂ (Fin 3 → ℂ) := basisOfLinearIndependentOfCardEqFinrank (rows_linearly_independent V) (Module.finrank_fin_fun ℂ).symm
V:CKMMatrixg:Fin 3 → ℂh0:g 1 = 0h1:g 2 = 0hg:g 0 • [V]u = (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]c)) ((starRingEnd (Fin 3 → ℂ)) [V]t)h3✝:(starRingEnd (Fin 3 → ℂ)) ((crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]c)) ((starRingEnd (Fin 3 → ℂ)) [V]t)) = (starRingEnd ℂ) (g 0) • (starRingEnd (Fin 3 → ℂ)) [V]uhx:‖g 0‖ = -1h3:1 ≤ 0h4:0 < 1⊢ ∃ κ, [V]u = cexp (↑κ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]c)) ((starRingEnd (Fin 3 → ℂ)) [V]t) All goals completed! 🐙All goals completed! 🐙lemma ext_Rows {U V : CKMMatrix} (hu : [U]u = [V]u) (hc : [U]c = [V]c) (ht : [U]t = [V]t) : U = V := U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]t⊢ U = V U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]t⊢ ↑U = ↑V U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]ti:Fin 3j:Fin 3⊢ ↑U i j = ↑V i j U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]tj:Fin 3⊢ ↑U ((fun i => i) ⟨0, ⋯⟩) j = ↑V ((fun i => i) ⟨0, ⋯⟩) jU:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]tj:Fin 3⊢ ↑U ((fun i => i) ⟨1, ⋯⟩) j = ↑V ((fun i => i) ⟨1, ⋯⟩) jU:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]tj:Fin 3⊢ ↑U ((fun i => i) ⟨2, ⋯⟩) j = ↑V ((fun i => i) ⟨2, ⋯⟩) j U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]tj:Fin 3⊢ ↑U ((fun i => i) ⟨0, ⋯⟩) j = ↑V ((fun i => i) ⟨0, ⋯⟩) j U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]tj:Fin 3h1:[U]u j = [V]u j⊢ ↑U ((fun i => i) ⟨0, ⋯⟩) j = ↑V ((fun i => i) ⟨0, ⋯⟩) j U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]u ((fun i => i) ⟨0, ⋯⟩) = [V]u ((fun i => i) ⟨0, ⋯⟩)⊢ ↑U ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑V ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]u ((fun i => i) ⟨1, ⋯⟩) = [V]u ((fun i => i) ⟨1, ⋯⟩)⊢ ↑U ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑V ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]u ((fun i => i) ⟨2, ⋯⟩) = [V]u ((fun i => i) ⟨2, ⋯⟩)⊢ ↑U ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑V ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]u ((fun i => i) ⟨0, ⋯⟩) = [V]u ((fun i => i) ⟨0, ⋯⟩)⊢ ↑U ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑V ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]u ((fun i => i) ⟨1, ⋯⟩) = [V]u ((fun i => i) ⟨1, ⋯⟩)⊢ ↑U ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑V ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]u ((fun i => i) ⟨2, ⋯⟩) = [V]u ((fun i => i) ⟨2, ⋯⟩)⊢ ↑U ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑V ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙 U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]tj:Fin 3⊢ ↑U ((fun i => i) ⟨1, ⋯⟩) j = ↑V ((fun i => i) ⟨1, ⋯⟩) j U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]tj:Fin 3h1:[U]c j = [V]c j⊢ ↑U ((fun i => i) ⟨1, ⋯⟩) j = ↑V ((fun i => i) ⟨1, ⋯⟩) j U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]c ((fun i => i) ⟨0, ⋯⟩) = [V]c ((fun i => i) ⟨0, ⋯⟩)⊢ ↑U ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑V ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]c ((fun i => i) ⟨1, ⋯⟩) = [V]c ((fun i => i) ⟨1, ⋯⟩)⊢ ↑U ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑V ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]c ((fun i => i) ⟨2, ⋯⟩) = [V]c ((fun i => i) ⟨2, ⋯⟩)⊢ ↑U ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑V ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]c ((fun i => i) ⟨0, ⋯⟩) = [V]c ((fun i => i) ⟨0, ⋯⟩)⊢ ↑U ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑V ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]c ((fun i => i) ⟨1, ⋯⟩) = [V]c ((fun i => i) ⟨1, ⋯⟩)⊢ ↑U ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑V ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]c ((fun i => i) ⟨2, ⋯⟩) = [V]c ((fun i => i) ⟨2, ⋯⟩)⊢ ↑U ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑V ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙 U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]tj:Fin 3⊢ ↑U ((fun i => i) ⟨2, ⋯⟩) j = ↑V ((fun i => i) ⟨2, ⋯⟩) j U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]tj:Fin 3h1:[U]t j = [V]t j⊢ ↑U ((fun i => i) ⟨2, ⋯⟩) j = ↑V ((fun i => i) ⟨2, ⋯⟩) j U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]t ((fun i => i) ⟨0, ⋯⟩) = [V]t ((fun i => i) ⟨0, ⋯⟩)⊢ ↑U ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑V ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]t ((fun i => i) ⟨1, ⋯⟩) = [V]t ((fun i => i) ⟨1, ⋯⟩)⊢ ↑U ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑V ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]t ((fun i => i) ⟨2, ⋯⟩) = [V]t ((fun i => i) ⟨2, ⋯⟩)⊢ ↑U ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑V ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]t ((fun i => i) ⟨0, ⋯⟩) = [V]t ((fun i => i) ⟨0, ⋯⟩)⊢ ↑U ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑V ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]t ((fun i => i) ⟨1, ⋯⟩) = [V]t ((fun i => i) ⟨1, ⋯⟩)⊢ ↑U ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑V ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)U:CKMMatrixV:CKMMatrixhu:[U]u = [V]uhc:[U]c = [V]cht:[U]t = [V]th1:[U]t ((fun i => i) ⟨2, ⋯⟩) = [V]t ((fun i => i) ⟨2, ⋯⟩)⊢ ↑U ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑V ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙

The cross product of the conjugate of the u and c rows of a CKM matrix.

def ucCross : Fin 3 → ℂ := conj [phaseShiftApply V a b c d e f]u ⨯₃ conj [phaseShiftApply V a b c d e f]c
lemma ucCross_fst (V : CKMMatrix) : (ucCross V a b c d e f) 0 = cexp ((- a * I) + (- b * I) + (- e * I) + (- f * I)) * (conj [V]u ⨯₃ conj [V]c) 0 := a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝV:CKMMatrix⊢ ucCross V a b c d e f 0 = cexp (-↑a * I + -↑b * I + -↑e * I + -↑f * I) * (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c) 0 a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝV:CKMMatrix⊢ cexp (-(↑a * I)) * cexp (-(↑e * I)) * (starRingEnd ℂ) (↑V 0 1) * (cexp (-(↑b * I)) * cexp (-(↑f * I)) * (starRingEnd ℂ) (↑V 1 2)) - cexp (-(↑a * I)) * cexp (-(↑f * I)) * (starRingEnd ℂ) (↑V 0 2) * (cexp (-(↑b * I)) * cexp (-(↑e * I)) * (starRingEnd ℂ) (↑V 1 1)) = cexp (-(↑a * I)) * cexp (-(↑b * I)) * cexp (-(↑e * I)) * cexp (-(↑f * I)) * ((starRingEnd ℂ) (↑V 0 1) * (starRingEnd ℂ) (↑V 1 2) - (starRingEnd ℂ) (↑V 0 2) * (starRingEnd ℂ) (↑V 1 1)) All goals completed! 🐙lemma ucCross_snd (V : CKMMatrix) : (ucCross V a b c d e f) 1 = cexp ((- a * I) + (- b * I) + (- d * I) + (- f * I)) * (conj [V]u ⨯₃ conj [V]c) 1 := a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝV:CKMMatrix⊢ ucCross V a b c d e f 1 = cexp (-↑a * I + -↑b * I + -↑d * I + -↑f * I) * (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c) 1 a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝV:CKMMatrix⊢ cexp (-(↑a * I)) * cexp (-(↑f * I)) * (starRingEnd ℂ) (↑V 0 2) * (cexp (-(↑b * I)) * cexp (-(↑d * I)) * (starRingEnd ℂ) (↑V 1 0)) - cexp (-(↑a * I)) * cexp (-(↑d * I)) * (starRingEnd ℂ) (↑V 0 0) * (cexp (-(↑b * I)) * cexp (-(↑f * I)) * (starRingEnd ℂ) (↑V 1 2)) = cexp (-(↑a * I)) * cexp (-(↑b * I)) * cexp (-(↑d * I)) * cexp (-(↑f * I)) * ((starRingEnd ℂ) (↑V 0 2) * (starRingEnd ℂ) (↑V 1 0) - (starRingEnd ℂ) (↑V 0 0) * (starRingEnd ℂ) (↑V 1 2)) All goals completed! 🐙lemma ucCross_thd (V : CKMMatrix) : (ucCross V a b c d e f) 2 = cexp ((- a * I) + (- b * I) + (- d * I) + (- e * I)) * (conj [V]u ⨯₃ conj [V]c) 2 := a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝV:CKMMatrix⊢ ucCross V a b c d e f 2 = cexp (-↑a * I + -↑b * I + -↑d * I + -↑e * I) * (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c) 2 a:ℝb:ℝc:ℝd:ℝe:ℝf:ℝV:CKMMatrix⊢ cexp (-(↑a * I)) * cexp (-(↑d * I)) * (starRingEnd ℂ) (↑V 0 0) * (cexp (-(↑b * I)) * cexp (-(↑e * I)) * (starRingEnd ℂ) (↑V 1 1)) - cexp (-(↑a * I)) * cexp (-(↑e * I)) * (starRingEnd ℂ) (↑V 0 1) * (cexp (-(↑b * I)) * cexp (-(↑d * I)) * (starRingEnd ℂ) (↑V 1 0)) = cexp (-(↑a * I)) * cexp (-(↑b * I)) * cexp (-(↑d * I)) * cexp (-(↑e * I)) * ((starRingEnd ℂ) (↑V 0 0) * (starRingEnd ℂ) (↑V 1 1) - (starRingEnd ℂ) (↑V 0 1) * (starRingEnd ℂ) (↑V 1 0)) All goals completed! 🐙lemma uRow_mul (V : CKMMatrix) (a b c : ℝ) : [phaseShiftApply V a b c 0 0 0]u = cexp (a * I) • [V]u := V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]u = cexp (↑a * I) • [V]u V:CKMMatrixa:ℝb:ℝc:ℝi:Fin 3⊢ [phaseShiftApply V a b c 0 0 0]u i = (cexp (↑a * I) • [V]u) i V:CKMMatrixa:ℝb:ℝc:ℝi:Fin 3⊢ [phaseShiftApply V a b c 0 0 0]u i = cexp (↑a * I) * [V]u i V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]u ((fun i => i) ⟨0, ⋯⟩) = cexp (↑a * I) * [V]u ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]u ((fun i => i) ⟨1, ⋯⟩) = cexp (↑a * I) * [V]u ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]u ((fun i => i) ⟨2, ⋯⟩) = cexp (↑a * I) * [V]u ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]u ((fun i => i) ⟨0, ⋯⟩) = cexp (↑a * I) * [V]u ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]u ((fun i => i) ⟨1, ⋯⟩) = cexp (↑a * I) * [V]u ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]u ((fun i => i) ⟨2, ⋯⟩) = cexp (↑a * I) * [V]u ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixa:ℝb:ℝc:ℝ⊢ ↑(phaseShiftApply V a b c 0 0 0) 0 2 = cexp (↑a * I) * [V]u ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixa:ℝb:ℝc:ℝ⊢ ↑(phaseShiftApply V a b c 0 0 0) 0 0 = cexp (↑a * I) * [V]u ((fun i => i) ⟨0, ⋯⟩) All goals completed! 🐙 V:CKMMatrixa:ℝb:ℝc:ℝ⊢ ↑(phaseShiftApply V a b c 0 0 0) 0 1 = cexp (↑a * I) * [V]u ((fun i => i) ⟨1, ⋯⟩) All goals completed! 🐙 V:CKMMatrixa:ℝb:ℝc:ℝ⊢ ↑(phaseShiftApply V a b c 0 0 0) 0 2 = cexp (↑a * I) * [V]u ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙lemma cRow_mul (V : CKMMatrix) (a b c : ℝ) : [phaseShiftApply V a b c 0 0 0]c = cexp (b * I) • [V]c := V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]c = cexp (↑b * I) • [V]c V:CKMMatrixa:ℝb:ℝc:ℝi:Fin 3⊢ [phaseShiftApply V a b c 0 0 0]c i = (cexp (↑b * I) • [V]c) i V:CKMMatrixa:ℝb:ℝc:ℝi:Fin 3⊢ [phaseShiftApply V a b c 0 0 0]c i = cexp (↑b * I) * [V]c i V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]c ((fun i => i) ⟨0, ⋯⟩) = cexp (↑b * I) * [V]c ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]c ((fun i => i) ⟨1, ⋯⟩) = cexp (↑b * I) * [V]c ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]c ((fun i => i) ⟨2, ⋯⟩) = cexp (↑b * I) * [V]c ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]c ((fun i => i) ⟨0, ⋯⟩) = cexp (↑b * I) * [V]c ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]c ((fun i => i) ⟨1, ⋯⟩) = cexp (↑b * I) * [V]c ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]c ((fun i => i) ⟨2, ⋯⟩) = cexp (↑b * I) * [V]c ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixa:ℝb:ℝc:ℝ⊢ ↑(phaseShiftApply V a b c 0 0 0) 1 2 = cexp (↑b * I) * [V]c ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixa:ℝb:ℝc:ℝ⊢ ↑(phaseShiftApply V a b c 0 0 0) 1 0 = cexp (↑b * I) * [V]c ((fun i => i) ⟨0, ⋯⟩) All goals completed! 🐙 V:CKMMatrixa:ℝb:ℝc:ℝ⊢ ↑(phaseShiftApply V a b c 0 0 0) 1 1 = cexp (↑b * I) * [V]c ((fun i => i) ⟨1, ⋯⟩) All goals completed! 🐙 V:CKMMatrixa:ℝb:ℝc:ℝ⊢ ↑(phaseShiftApply V a b c 0 0 0) 1 2 = cexp (↑b * I) * [V]c ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙lemma tRow_mul (V : CKMMatrix) (a b c : ℝ) : [phaseShiftApply V a b c 0 0 0]t = cexp (c * I) • [V]t := V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]t = cexp (↑c * I) • [V]t V:CKMMatrixa:ℝb:ℝc:ℝi:Fin 3⊢ [phaseShiftApply V a b c 0 0 0]t i = (cexp (↑c * I) • [V]t) i V:CKMMatrixa:ℝb:ℝc:ℝi:Fin 3⊢ [phaseShiftApply V a b c 0 0 0]t i = cexp (↑c * I) * [V]t i V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]t ((fun i => i) ⟨0, ⋯⟩) = cexp (↑c * I) * [V]t ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]t ((fun i => i) ⟨1, ⋯⟩) = cexp (↑c * I) * [V]t ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]t ((fun i => i) ⟨2, ⋯⟩) = cexp (↑c * I) * [V]t ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]t ((fun i => i) ⟨0, ⋯⟩) = cexp (↑c * I) * [V]t ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]t ((fun i => i) ⟨1, ⋯⟩) = cexp (↑c * I) * [V]t ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixa:ℝb:ℝc:ℝ⊢ [phaseShiftApply V a b c 0 0 0]t ((fun i => i) ⟨2, ⋯⟩) = cexp (↑c * I) * [V]t ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixa:ℝb:ℝc:ℝ⊢ ↑(phaseShiftApply V a b c 0 0 0) 2 2 = cexp (↑c * I) * [V]t ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixa:ℝb:ℝc:ℝ⊢ ↑(phaseShiftApply V a b c 0 0 0) 2 0 = cexp (↑c * I) * [V]t ((fun i => i) ⟨0, ⋯⟩) All goals completed! 🐙 V:CKMMatrixa:ℝb:ℝc:ℝ⊢ ↑(phaseShiftApply V a b c 0 0 0) 2 1 = cexp (↑c * I) * [V]t ((fun i => i) ⟨1, ⋯⟩) All goals completed! 🐙 V:CKMMatrixa:ℝb:ℝc:ℝ⊢ ↑(phaseShiftApply V a b c 0 0 0) 2 2 = cexp (↑c * I) * [V]t ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙