Documentation Verification Report

PhaseFreedom

📁 Source: PhysLean/Particles/FlavorPhysics/CKMMatrix/PhaseFreedom.lean

Statistics

MetricCount
DefinitionsFstRowThdColRealCond, ubOnePhaseCond
2
Theoremscd_of_fstRowThdColRealCond, cs_of_fstRowThdColRealCond, fstRowThdColRealCond_holds_up_to_equiv, fstRowThdColRealCond_shift_solution, shift_cb_phase_zero, shift_cd_phase_pi, shift_cross_product_phase_zero, shift_cs_phase_zero, shift_tb_phase_zero, shift_ub_phase_zero, shift_ud_phase_zero, shift_us_phase_zero, ubOnePhaseCond_hold_up_to_equiv_of_ub_one, ubOnePhaseCond_shift_solution
14
Total16

CKMMatrix

Definitions

NameCategoryTheorems
FstRowThdColRealCond 📖MathDef
1 mathmath: fstRowThdColRealCond_holds_up_to_equiv
ubOnePhaseCond 📖MathDef
1 mathmath: ubOnePhaseCond_hold_up_to_equiv_of_ub_one

Theorems

NameKindAssumesProvesValidatesDepends On
cd_of_fstRowThdColRealCond 📖mathematicalFstRowThdColRealCondVtbAbs
CKMMatrix
CKMMatrixSetoid
VusAbs
VudAbs
VubAbs
VcbAbs
cd_of_ud_us_ub_cb_tb
Vabs_sq_add_neq_zero
cs_of_fstRowThdColRealCond 📖mathematicalFstRowThdColRealCondVtbAbs
CKMMatrix
CKMMatrixSetoid
VudAbs
VusAbs
VubAbs
VcbAbs
cs_of_ud_us_ub_cb_tb
Vabs_sq_add_neq_zero
fstRowThdColRealCond_holds_up_to_equiv 📖mathematicalCKMMatrix
CKMMatrixSetoid
FstRowThdColRealCond
uRow_cross_cRow_eq_tRow
phaseShiftApply.equiv
shift_ud_phase_zero
shift_us_phase_zero
shift_cb_phase_zero
shift_tb_phase_zero
shift_cross_product_phase_zero
fstRowThdColRealCond_shift_solution 📖
shift_cb_phase_zero 📖mathematicalphaseShiftApply
VcbAbs
CKMMatrix
CKMMatrixSetoid
phaseShiftApply.cb
shift_cd_phase_pi 📖mathematicalphaseShiftApply
VcdAbs
CKMMatrix
CKMMatrixSetoid
phaseShiftApply.cd
shift_cross_product_phase_zero 📖mathematicaluRow
cRow
tRow
phaseShiftApplyphaseShiftApply.ucCross_fst
phaseShiftApply.td
phaseShiftApply.ucCross_snd
phaseShiftApply.ts
phaseShiftApply.ucCross_thd
phaseShiftApply.tb
shift_cs_phase_zero 📖mathematicalphaseShiftApply
VcsAbs
CKMMatrix
CKMMatrixSetoid
phaseShiftApply.cs
shift_tb_phase_zero 📖mathematicalphaseShiftApply
VtbAbs
CKMMatrix
CKMMatrixSetoid
phaseShiftApply.tb
shift_ub_phase_zero 📖mathematicalphaseShiftApply
VubAbs
CKMMatrix
CKMMatrixSetoid
phaseShiftApply.ub
shift_ud_phase_zero 📖mathematicalphaseShiftApply
VudAbs
CKMMatrix
CKMMatrixSetoid
phaseShiftApply.ud
shift_us_phase_zero 📖mathematicalphaseShiftApply
VusAbs
CKMMatrix
CKMMatrixSetoid
phaseShiftApply.us
ubOnePhaseCond_hold_up_to_equiv_of_ub_one 📖mathematicalFstRowThdColRealCondCKMMatrix
CKMMatrixSetoid
ubOnePhaseCond
phaseShiftApply.equiv
cb_eq_zero_of_ud_us_zero
shift_ub_phase_zero
ud_us_neq_zero_iff_ub_neq_one
shift_cross_product_phase_zero
shift_cd_phase_pi
shift_cs_phase_zero
cs_of_ud_us_zero
ubOnePhaseCond_shift_solution 📖

---

← Back to Index