StandardParameters

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

Statistics

Metric	Count
Definitions `C₁₂`, `C₁₃`, `C₂₃`, `S₁₂`, `S₁₃`, `S₂₃`, `δ₁₃`, `θ₁₂`, `θ₁₃`, `θ₂₃`	10
Theorems `C₁₂_eq_Vud_div_sqrt`, `C₁₂_eq_ℂcos_θ₁₂`, `C₁₂_of_Vub_one`, `C₁₃_eq_add_sq`, `C₁₃_eq_ℂcos_θ₁₃`, `C₁₃_of_Vub_eq_one`, `C₂₃_eq_ℂcos_θ₂₃`, `C₂₃_of_Vub_neq_one`, `S₁₂_eq_sin_θ₁₂`, `S₁₂_eq_ℂsin_θ₁₂`, `S₁₂_leq_one`, `S₁₂_nonneg`, `S₁₂_of_Vub_one`, `S₁₂_sq_add_C₁₂_sq`, `S₁₃_eq_sin_θ₁₃`, `S₁₃_eq_ℂsin_θ₁₃`, `S₁₃_leq_one`, `S₁₃_nonneg`, `S₁₃_of_Vub_one`, `S₁₃_sq_add_C₁₃_sq`, `S₂₃_eq_sin_θ₂₃`, `S₂₃_eq_ℂsin_θ₂₃`, `S₂₃_leq_one`, `S₂₃_nonneg`, `S₂₃_of_Vub_eq_one`, `S₂₃_of_Vub_neq_one`, `S₂₃_sq_add_C₂₃_sq`, `VcbAbs_eq_S₂₃_mul_C₁₃`, `Vs_zero_iff_cos_sin_zero`, `VtbAbs_eq_C₂₃_mul_C₁₃`, `VubAbs_eq_S₁₃`, `VubAbs_of_cos_θ₁₃_zero`, `VudAbs_eq_C₁₂_mul_C₁₃`, `VusAbs_eq_S₁₂_mul_C₁₃`, `complexAbs_cos_θ₁₂`, `complexAbs_cos_θ₁₃`, `complexAbs_cos_θ₂₃`, `complexAbs_sin_θ₁₂`, `complexAbs_sin_θ₁₃`, `complexAbs_sin_θ₂₃`, `eq_standParam_of_fstRowThdColRealCond`, `eq_standParam_of_ubOnePhaseCond`, `eq_standardParameterization_δ₃`, `exists_for_CKMatrix`, `exists_δ₁₃`, `mulExpδ₁₃_on_param_abs`, `mulExpδ₁₃_on_param_eq_zero_iff`, `mulExpδ₁₃_on_param_neq_zero_arg`, `mulExpδ₁₃_on_param_δ₁₃`, `on_param_cos_θ₁₂_eq_zero`, `on_param_cos_θ₁₃_eq_zero`, `on_param_cos_θ₂₃_eq_zero`, `on_param_sin_θ₁₂_eq_zero`, `on_param_sin_θ₁₃_eq_zero`, `on_param_sin_θ₂₃_eq_zero`	55
Total	65

(root)

Definitions

Name	Category	Theorems
`C₁₂` 📖	CompOp	5 math math: `C₁₂_of_Vub_one`, `C₁₂_eq_ℂcos_θ₁₂`, `VudAbs_eq_C₁₂_mul_C₁₃`, `S₁₂_sq_add_C₁₂_sq`, `C₁₂_eq_Vud_div_sqrt`
`C₁₃` 📖	CompOp	8 math math: `C₁₃_eq_add_sq`, `VtbAbs_eq_C₂₃_mul_C₁₃`, `VcbAbs_eq_S₂₃_mul_C₁₃`, `VudAbs_eq_C₁₂_mul_C₁₃`, `C₁₃_eq_ℂcos_θ₁₃`, `S₁₃_sq_add_C₁₃_sq`, `C₁₃_of_Vub_eq_one`, `VusAbs_eq_S₁₂_mul_C₁₃`
`C₂₃` 📖	CompOp	4 math math: `VtbAbs_eq_C₂₃_mul_C₁₃`, `C₂₃_eq_ℂcos_θ₂₃`, `C₂₃_of_Vub_neq_one`, `S₂₃_sq_add_C₂₃_sq`
`S₁₂` 📖	CompOp	7 math math: `S₁₂_eq_sin_θ₁₂`, `S₁₂_of_Vub_one`, `S₁₂_leq_one`, `S₁₂_nonneg`, `S₁₂_sq_add_C₁₂_sq`, `VusAbs_eq_S₁₂_mul_C₁₃`, `S₁₂_eq_ℂsin_θ₁₂`
`S₁₃` 📖	CompOp	7 math math: `S₁₃_nonneg`, `S₁₃_of_Vub_one`, `VubAbs_eq_S₁₃`, `S₁₃_sq_add_C₁₃_sq`, `S₁₃_leq_one`, `S₁₃_eq_ℂsin_θ₁₃`, `S₁₃_eq_sin_θ₁₃`
`S₂₃` 📖	CompOp	8 math math: `S₂₃_eq_ℂsin_θ₂₃`, `S₂₃_nonneg`, `VcbAbs_eq_S₂₃_mul_C₁₃`, `S₂₃_sq_add_C₂₃_sq`, `S₂₃_leq_one`, `S₂₃_eq_sin_θ₂₃`, `S₂₃_of_Vub_eq_one`, `S₂₃_of_Vub_neq_one`
`δ₁₃` 📖	CompOp	1 math math: `standParam.eq_standardParameterization_δ₃`
`θ₁₂` 📖	CompOp	18 math math: `complexAbs_sin_θ₁₂`, `C₁₂_eq_ℂcos_θ₁₂`, `standParam.mulExpδ₁₃_on_param_abs`, `S₁₂_eq_sin_θ₁₂`, `Vs_zero_iff_cos_sin_zero`, `standParam.mulExpδ₁₃_on_param_neq_zero_arg`, `standParam.on_param_cos_θ₂₃_eq_zero`, `standParam.on_param_sin_θ₁₃_eq_zero`, `standParam.mulExpδ₁₃_on_param_eq_zero_iff`, `complexAbs_cos_θ₁₂`, `standParam.eq_standardParameterization_δ₃`, `standParam.on_param_cos_θ₁₃_eq_zero`, `standParam.eq_standParam_of_fstRowThdColRealCond`, `standParam.eq_standParam_of_ubOnePhaseCond`, `S₁₂_eq_ℂsin_θ₁₂`, `standParam.exists_δ₁₃`, `standParam.mulExpδ₁₃_on_param_δ₁₃`, `standParam.on_param_sin_θ₂₃_eq_zero`
`θ₁₃` 📖	CompOp	18 math math: `standParam.mulExpδ₁₃_on_param_abs`, `standParam.on_param_sin_θ₁₂_eq_zero`, `Vs_zero_iff_cos_sin_zero`, `standParam.mulExpδ₁₃_on_param_neq_zero_arg`, `standParam.on_param_cos_θ₁₂_eq_zero`, `standParam.on_param_cos_θ₂₃_eq_zero`, `complexAbs_sin_θ₁₃`, `standParam.mulExpδ₁₃_on_param_eq_zero_iff`, `C₁₃_eq_ℂcos_θ₁₃`, `standParam.eq_standardParameterization_δ₃`, `standParam.eq_standParam_of_fstRowThdColRealCond`, `standParam.eq_standParam_of_ubOnePhaseCond`, `S₁₃_eq_ℂsin_θ₁₃`, `S₁₃_eq_sin_θ₁₃`, `standParam.exists_δ₁₃`, `complexAbs_cos_θ₁₃`, `standParam.mulExpδ₁₃_on_param_δ₁₃`, `standParam.on_param_sin_θ₂₃_eq_zero`
`θ₂₃` 📖	CompOp	18 math math: `standParam.mulExpδ₁₃_on_param_abs`, `standParam.on_param_sin_θ₁₂_eq_zero`, `Vs_zero_iff_cos_sin_zero`, `standParam.mulExpδ₁₃_on_param_neq_zero_arg`, `S₂₃_eq_ℂsin_θ₂₃`, `standParam.on_param_cos_θ₁₂_eq_zero`, `C₂₃_eq_ℂcos_θ₂₃`, `complexAbs_sin_θ₂₃`, `complexAbs_cos_θ₂₃`, `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_δ₁₃`, `S₂₃_eq_sin_θ₂₃`, `standParam.mulExpδ₁₃_on_param_δ₁₃`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C₁₂_eq_Vud_div_sqrt` 📖	mathematical	—	`C₁₂` `VudAbs` `VusAbs`	—	`C₁₂.eq_1` `θ₁₂.eq_1` `S₁₂.eq_1` `CKMMatrix.VAbsub_neq_zero_Vud_Vus_neq_zero` `CKMMatrix.VAbs_ge_zero`
`C₁₂_eq_ℂcos_θ₁₂` 📖	mathematical	—	`θ₁₂` `C₁₂`	—	—
`C₁₂_of_Vub_one` 📖	mathematical	`VubAbs`	`C₁₂`	—	`C₁₂.eq_1` `θ₁₂.eq_1` `S₁₂_of_Vub_one`
`C₁₃_eq_add_sq` 📖	mathematical	—	`C₁₃` `VudAbs` `VusAbs`	—	`C₁₃.eq_1` `θ₁₃.eq_1` `S₁₃.eq_1` `CKMMatrix.VAbs_sum_sq_row_eq_one`
`C₁₃_eq_ℂcos_θ₁₃` 📖	mathematical	—	`θ₁₃` `C₁₃`	—	—
`C₁₃_of_Vub_eq_one` 📖	mathematical	`VubAbs`	`C₁₃`	—	`C₁₃.eq_1` `θ₁₃.eq_1` `S₁₃.eq_1`
`C₂₃_eq_ℂcos_θ₂₃` 📖	mathematical	—	`θ₂₃` `C₂₃`	—	—
`C₂₃_of_Vub_neq_one` 📖	mathematical	—	`C₂₃` `VtbAbs` `VudAbs` `VusAbs`	—	`C₂₃.eq_1` `θ₂₃.eq_1` `S₂₃_of_Vub_neq_one` `CKMMatrix.VudAbs_sq_add_VusAbs_sq` `CKMMatrix.VcbAbs_sq_add_VtbAbs_sq` `CKMMatrix.VAbsub_neq_zero_Vud_Vus_neq_zero` `CKMMatrix.VAbs_ge_zero`
`S₁₂_eq_sin_θ₁₂` 📖	mathematical	—	`θ₁₂` `S₁₂`	—	`S₁₂_nonneg` `S₁₂_leq_one`
`S₁₂_eq_ℂsin_θ₁₂` 📖	mathematical	—	`θ₁₂` `S₁₂`	—	`S₁₂_eq_sin_θ₁₂`
`S₁₂_leq_one` 📖	mathematical	—	`S₁₂`	—	`S₁₂.eq_1` `CKMMatrix.VAbs_ge_zero`
`S₁₂_nonneg` 📖	mathematical	—	`S₁₂`	—	`S₁₂.eq_1` `CKMMatrix.VAbs_ge_zero`
`S₁₂_of_Vub_one` 📖	mathematical	`VubAbs`	`S₁₂`	—	`CKMMatrix.VAbs_sum_sq_row_eq_one`
`S₁₂_sq_add_C₁₂_sq` 📖	mathematical	—	`S₁₂` `C₁₂`	—	`S₁₂_eq_sin_θ₁₂` `C₁₂.eq_1`
`S₁₃_eq_sin_θ₁₃` 📖	mathematical	—	`θ₁₃` `S₁₃`	—	`S₁₃_nonneg` `S₁₃_leq_one`
`S₁₃_eq_ℂsin_θ₁₃` 📖	mathematical	—	`θ₁₃` `S₁₃`	—	`S₁₃_eq_sin_θ₁₃`
`S₁₃_leq_one` 📖	mathematical	—	`S₁₃`	—	`CKMMatrix.VAbs_leq_one`
`S₁₃_nonneg` 📖	mathematical	—	`S₁₃`	—	`CKMMatrix.VAbs_ge_zero`
`S₁₃_of_Vub_one` 📖	mathematical	`VubAbs`	`S₁₃`	—	`S₁₃.eq_1`
`S₁₃_sq_add_C₁₃_sq` 📖	mathematical	—	`S₁₃` `C₁₃`	—	`S₁₃_eq_sin_θ₁₃` `C₁₃.eq_1`
`S₂₃_eq_sin_θ₂₃` 📖	mathematical	—	`θ₂₃` `S₂₃`	—	`S₂₃_nonneg` `S₂₃_leq_one`
`S₂₃_eq_ℂsin_θ₂₃` 📖	mathematical	—	`θ₂₃` `S₂₃`	—	`S₂₃_eq_sin_θ₂₃`
`S₂₃_leq_one` 📖	mathematical	—	`S₂₃`	—	`S₂₃.eq_1` `CKMMatrix.VAbs_leq_one` `CKMMatrix.VAbs_ge_zero` `CKMMatrix.VudAbs_sq_add_VusAbs_sq` `CKMMatrix.VcbAbs_sq_add_VtbAbs_sq`
`S₂₃_nonneg` 📖	mathematical	—	`S₂₃`	—	`S₂₃.eq_1` `CKMMatrix.VAbs_ge_zero`
`S₂₃_of_Vub_eq_one` 📖	mathematical	`VubAbs`	`S₂₃` `VcdAbs`	—	`S₂₃.eq_1`
`S₂₃_of_Vub_neq_one` 📖	mathematical	—	`S₂₃` `VcbAbs` `VudAbs` `VusAbs`	—	`S₂₃.eq_1`
`S₂₃_sq_add_C₂₃_sq` 📖	mathematical	—	`S₂₃` `C₂₃`	—	`S₂₃_eq_sin_θ₂₃` `C₂₃.eq_1`
`VcbAbs_eq_S₂₃_mul_C₁₃` 📖	mathematical	—	`VcbAbs` `S₂₃` `C₁₃`	—	`C₁₃_of_Vub_eq_one` `CKMMatrix.VAbs_fst_col_eq_one_snd_eq_zero` `S₂₃_of_Vub_neq_one` `C₁₃_eq_add_sq` `CKMMatrix.VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero`
`Vs_zero_iff_cos_sin_zero` 📖	mathematical	—	`VudAbs` `CKMMatrix` `CKMMatrixSetoid` `VubAbs` `VusAbs` `VcbAbs` `VtbAbs` `θ₁₂` `θ₁₃` `θ₂₃`	—	`VudAbs_eq_C₁₂_mul_C₁₃` `VubAbs_eq_S₁₃` `VusAbs_eq_S₁₂_mul_C₁₃` `VcbAbs_eq_S₂₃_mul_C₁₃` `VtbAbs_eq_C₂₃_mul_C₁₃` `C₁₂.eq_1` `C₁₃.eq_1` `C₂₃.eq_1` `S₁₂_eq_sin_θ₁₂` `S₂₃_eq_sin_θ₂₃` `S₁₃_eq_sin_θ₁₃`
`VtbAbs_eq_C₂₃_mul_C₁₃` 📖	mathematical	—	`VtbAbs` `C₂₃` `C₁₃`	—	`C₁₃_of_Vub_eq_one` `CKMMatrix.VAbs_fst_col_eq_one_thd_eq_zero` `C₂₃_of_Vub_neq_one` `C₁₃_eq_add_sq` `CKMMatrix.VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero`
`VubAbs_eq_S₁₃` 📖	mathematical	—	`VubAbs` `S₁₃`	—	—
`VubAbs_of_cos_θ₁₃_zero` 📖	mathematical	`θ₁₃`	`VubAbs`	—	`CKMMatrix.VAbs_ge_zero` `CKMMatrix.VAbs_leq_one` `VubAbs_eq_S₁₃` `θ₁₃.eq_1`
`VudAbs_eq_C₁₂_mul_C₁₃` 📖	mathematical	—	`VudAbs` `C₁₂` `C₁₃`	—	`CKMMatrix.VAbs_thd_eq_one_fst_eq_zero` `C₁₃.eq_1` `θ₁₃.eq_1` `S₁₃.eq_1` `C₁₂_eq_Vud_div_sqrt` `CKMMatrix.VAbs_sum_sq_row_eq_one` `CKMMatrix.VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero`
`VusAbs_eq_S₁₂_mul_C₁₃` 📖	mathematical	—	`VusAbs` `S₁₂` `C₁₃`	—	`C₁₃.eq_1` `θ₁₃.eq_1` `S₁₂.eq_1` `S₁₃.eq_1` `CKMMatrix.VAbs_sum_sq_row_eq_one` `CKMMatrix.VAbs_thd_eq_one_snd_eq_zero` `CKMMatrix.VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero`
`complexAbs_cos_θ₁₂` 📖	mathematical	—	`θ₁₂`	—	`C₁₂_eq_ℂcos_θ₁₂`
`complexAbs_cos_θ₁₃` 📖	mathematical	—	`θ₁₃`	—	`C₁₃_eq_ℂcos_θ₁₃`
`complexAbs_cos_θ₂₃` 📖	mathematical	—	`θ₂₃`	—	`C₂₃_eq_ℂcos_θ₂₃`
`complexAbs_sin_θ₁₂` 📖	mathematical	—	`θ₁₂`	—	`S₁₂_eq_ℂsin_θ₁₂` `S₁₂_nonneg`
`complexAbs_sin_θ₁₃` 📖	mathematical	—	`θ₁₃`	—	`S₁₃_eq_ℂsin_θ₁₃` `S₁₃_nonneg`
`complexAbs_sin_θ₂₃` 📖	mathematical	—	`θ₂₃`	—	`S₂₃_eq_ℂsin_θ₂₃` `S₂₃_nonneg`

standParam

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_standParam_of_fstRowThdColRealCond` 📖	mathematical	`CKMMatrix.FstRowThdColRealCond`	`standParam` `θ₁₂` `CKMMatrix` `CKMMatrixSetoid` `θ₁₃` `θ₂₃`	—	`CKMMatrix.ud_us_neq_zero_iff_ub_neq_one` `CKMMatrix.Vabs_sq_add_neq_zero` `eq_rows` `VudAbs_eq_C₁₂_mul_C₁₃` `VusAbs_eq_S₁₂_mul_C₁₃` `S₁₂_eq_sin_θ₁₂` `C₁₃.eq_1` `VubAbs_eq_S₁₃` `S₁₃_eq_sin_θ₁₃` `CKMMatrix.cd_of_fstRowThdColRealCond` `S₁₂_eq_ℂsin_θ₁₂` `S₁₂.eq_1` `C₁₂_eq_ℂcos_θ₁₂` `C₁₂_eq_Vud_div_sqrt` `S₂₃_eq_ℂsin_θ₂₃` `S₂₃_of_Vub_neq_one` `C₂₃_eq_ℂcos_θ₂₃` `C₂₃_of_Vub_neq_one` `S₁₃_eq_ℂsin_θ₁₃` `S₁₃.eq_1` `CKMMatrix.cs_of_fstRowThdColRealCond` `VcbAbs_eq_S₂₃_mul_C₁₃`
`eq_standParam_of_ubOnePhaseCond` 📖	mathematical	`CKMMatrix.ubOnePhaseCond`	`standParam` `θ₁₂` `CKMMatrix` `CKMMatrixSetoid` `θ₁₃` `θ₂₃`	—	`eq_rows` `C₁₃_eq_ℂcos_θ₁₃` `C₁₃_of_Vub_eq_one` `S₁₃_eq_ℂsin_θ₁₃` `S₁₃.eq_1` `S₂₃_eq_ℂsin_θ₂₃` `S₂₃_of_Vub_eq_one` `S₁₂_eq_ℂsin_θ₁₂` `S₁₂_of_Vub_one` `C₁₂_eq_ℂcos_θ₁₂` `C₁₂_of_Vub_one` `S₁₃_of_Vub_one` `θ₂₃.eq_1`
`eq_standardParameterization_δ₃` 📖	mathematical	—	`CKMMatrix` `CKMMatrixSetoid` `standParam` `θ₁₂` `θ₁₃` `θ₂₃` `δ₁₃`	—	`exists_δ₁₃` `eq_exp_of_phases` `mulExpδ₁₃_on_param_neq_zero_arg` `δ₁₃.eq_1` `Invariant.mulExpδ₁₃.eq_1` `phaseShiftRelation_equiv` `Vs_zero_iff_cos_sin_zero` `mulExpδ₁₃_on_param_eq_zero_iff` `on_param_cos_θ₁₂_eq_zero` `on_param_cos_θ₁₃_eq_zero` `on_param_cos_θ₂₃_eq_zero` `on_param_sin_θ₁₂_eq_zero` `on_param_sin_θ₁₃_eq_zero` `on_param_sin_θ₂₃_eq_zero`
`exists_for_CKMatrix` 📖	mathematical	—	`CKMMatrix` `CKMMatrixSetoid` `standParam`	—	`eq_standardParameterization_δ₃`
`exists_δ₁₃` 📖	mathematical	—	`CKMMatrix` `CKMMatrixSetoid` `standParam` `θ₁₂` `θ₁₃` `θ₂₃`	—	`CKMMatrix.fstRowThdColRealCond_holds_up_to_equiv` `phaseShiftRelation_equiv` `eq_standParam_of_fstRowThdColRealCond` `CKMMatrix.ubOnePhaseCond_hold_up_to_equiv_of_ub_one` `eq_standParam_of_ubOnePhaseCond`
`mulExpδ₁₃_on_param_abs` 📖	mathematical	—	`Invariant.mulExpδ₁₃` `CKMMatrix` `CKMMatrixSetoid` `standParam` `θ₁₂` `θ₁₃` `θ₂₃`	—	`mulExpδ₁₃_on_param_δ₁₃` `complexAbs_sin_θ₁₃` `complexAbs_cos_θ₁₃` `complexAbs_sin_θ₁₂` `complexAbs_cos_θ₁₂` `complexAbs_sin_θ₂₃` `complexAbs_cos_θ₂₃`
`mulExpδ₁₃_on_param_eq_zero_iff` 📖	mathematical	—	`Invariant.mulExpδ₁₃` `CKMMatrix` `CKMMatrixSetoid` `standParam` `θ₁₂` `θ₁₃` `θ₂₃` `VudAbs` `VubAbs` `VusAbs` `VcbAbs` `VtbAbs`	—	`VudAbs_eq_C₁₂_mul_C₁₃` `VubAbs_eq_S₁₃` `VusAbs_eq_S₁₂_mul_C₁₃` `VcbAbs_eq_S₂₃_mul_C₁₃` `VtbAbs_eq_C₂₃_mul_C₁₃` `S₁₃_eq_ℂsin_θ₁₃` `S₁₂_eq_ℂsin_θ₁₂` `S₂₃_eq_ℂsin_θ₂₃` `C₁₃_eq_ℂcos_θ₁₃` `C₂₃_eq_ℂcos_θ₂₃` `C₁₂_eq_ℂcos_θ₁₂` `mulExpδ₁₃_on_param_δ₁₃`
`mulExpδ₁₃_on_param_neq_zero_arg` 📖	mathematical	—	`Invariant.mulExpδ₁₃` `CKMMatrix` `CKMMatrixSetoid` `standParam` `θ₁₂` `θ₁₃` `θ₂₃`	—	`mulExpδ₁₃_on_param_δ₁₃` `mulExpδ₁₃_on_param_abs`
`mulExpδ₁₃_on_param_δ₁₃` 📖	mathematical	—	`Invariant.mulExpδ₁₃` `CKMMatrix` `CKMMatrixSetoid` `standParam` `θ₁₂` `θ₁₃` `θ₂₃`	—	`mulExpδ₁₃_eq` `S₁₂_eq_sin_θ₁₂` `S₁₂_nonneg` `S₂₃_eq_sin_θ₂₃` `S₂₃_nonneg`
`on_param_cos_θ₁₂_eq_zero` 📖	mathematical	`θ₁₂` `CKMMatrix` `CKMMatrixSetoid`	`standParam` `θ₁₃` `θ₂₃`	—	—
`on_param_cos_θ₁₃_eq_zero` 📖	mathematical	`θ₁₃` `CKMMatrix` `CKMMatrixSetoid`	`standParam` `θ₁₂` `θ₂₃`	—	`S₁₃_of_Vub_one` `VubAbs_of_cos_θ₁₃_zero` `C₁₂_of_Vub_one` `S₁₂_of_Vub_one`
`on_param_cos_θ₂₃_eq_zero` 📖	mathematical	`θ₂₃` `CKMMatrix` `CKMMatrixSetoid`	`standParam` `θ₁₂` `θ₁₃`	—	—
`on_param_sin_θ₁₂_eq_zero` 📖	mathematical	`θ₁₂` `CKMMatrix` `CKMMatrixSetoid`	`standParam` `θ₁₃` `θ₂₃`	—	—
`on_param_sin_θ₁₃_eq_zero` 📖	mathematical	`θ₁₃` `CKMMatrix` `CKMMatrixSetoid`	`standParam` `θ₁₂` `θ₂₃`	—	—
`on_param_sin_θ₂₃_eq_zero` 📖	mathematical	`θ₂₃` `CKMMatrix` `CKMMatrixSetoid`	`standParam` `θ₁₂` `θ₁₃`	—	—

---

← Back to Index