Basic

📁 Source: PhysLean/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean

Statistics

Metric	Count
Definitions standParam, standParamAsMatrix	2
Theorems VusVubVcdSq_eq, cross_product_t, eq_exp_of_phases, eq_rows, mulExpδ₁₃_eq, standParamAsMatrix_unitary	6
Total	8

(root)

Definitions

Name	Category	Theorems
standParam 📖	CompOp	19 math math: standParam.mulExpδ₁₃_on_param_abs, standParam.on_param_sin_θ₁₂_eq_zero, standParam.mulExpδ₁₃_on_param_neq_zero_arg, standParam.VusVubVcdSq_eq, standParam.exists_for_CKMatrix, standParam.on_param_cos_θ₁₂_eq_zero, standParam.eq_exp_of_phases, standParam.cross_product_t, standParam.on_param_cos_θ₂₃_eq_zero, standParam.mulExpδ₁₃_eq, standParam.on_param_sin_θ₁₃_eq_zero, standParam.mulExpδ₁₃_on_param_eq_zero_iff, standParam.eq_standardParameterization_δ₃, standParam.on_param_cos_θ₁₃_eq_zero, standParam.eq_standParam_of_fstRowThdColRealCond, standParam.eq_standParam_of_ubOnePhaseCond, standParam.exists_δ₁₃, standParam.mulExpδ₁₃_on_param_δ₁₃, standParam.on_param_sin_θ₂₃_eq_zero
standParamAsMatrix 📖	CompOp	1 math math: standParamAsMatrix_unitary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
standParamAsMatrix_unitary 📖	mathematical	—	standParamAsMatrix	—	—

standParam

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
VusVubVcdSq_eq 📖	mathematical	—	Invariant.VusVubVcdSq CKMMatrix CKMMatrixSetoid standParam	—	VAbs'_equiv
cross_product_t 📖	mathematical	—	CKMMatrix.tRow standParam CKMMatrix.uRow CKMMatrix.cRow	—	—
eq_exp_of_phases 📖	mathematical	—	standParam	—	CKMMatrix_ext
eq_rows 📖	—	CKMMatrix.uRow standParam CKMMatrix.cRow CKMMatrix.tRow	—	—	CKMMatrix.ext_Rows cross_product_t
mulExpδ₁₃_eq 📖	mathematical	—	Invariant.mulExpδ₁₃ CKMMatrix CKMMatrixSetoid standParam	—	Invariant.mulExpδ₁₃.eq_1 VusVubVcdSq_eq Invariant.jarlskogℂCKM_equiv

---

← Back to Index