Relations

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

Statistics

Metric	Count
Definitions	0
Theorems `VAbs_fst_col_eq_one_snd_eq_zero`, `VAbs_fst_col_eq_one_thd_eq_zero`, `VAbs_ge_zero`, `VAbs_leq_one`, `VAbs_sum_sq_col_eq_one`, `VAbs_sum_sq_row_eq_one`, `VAbs_thd_eq_one_fst_eq_zero`, `VAbs_thd_eq_one_snd_eq_zero`, `VAbsub_neq_zero_Vud_Vus_neq_zero`, `VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero`, `Vabs_sq_add_neq_zero`, `VcbAbs_sq_add_VtbAbs_sq`, `Vcd_mul_conj_Vud`, `Vcs_mul_conj_Vus`, `VudAbs_sq_add_VusAbs_sq`, `cb_eq_zero_of_ud_us_zero`, `cb_tb_neq_zero_iff_ub_neq_one`, `cd_of_ud_us_ub_cb_tb`, `conj_Vtb_cross_product`, `conj_Vtb_mul_Vud`, `conj_Vtb_mul_Vus`, `cs_of_ud_us_ub_cb_tb`, `cs_of_ud_us_zero`, `fst_row_normalized_abs`, `fst_row_normalized_normSq`, `fst_row_orthog_snd_row`, `fst_row_orthog_thd_row`, `normSq_Vud_plus_normSq_Vus`, `normSq_Vud_plus_normSq_Vus_neq_zero_ℂ`, `normSq_Vud_plus_normSq_Vus_neq_zero_ℝ`, `snd_row_normalized_abs`, `snd_row_normalized_normSq`, `thd_col_normalized_abs`, `thd_col_normalized_normSq`, `thd_row_normalized_abs`, `thd_row_normalized_normSq`, `ud_us_neq_zero_iff_ub_neq_one`	37
Total	37

CKMMatrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`VAbs_fst_col_eq_one_snd_eq_zero` 📖	—	`VAbs`	—	—	`VAbs_sum_sq_col_eq_one`
`VAbs_fst_col_eq_one_thd_eq_zero` 📖	—	`VAbs`	—	—	`VAbs_sum_sq_col_eq_one`
`VAbs_ge_zero` 📖	mathematical	—	`VAbs`	—	—
`VAbs_leq_one` 📖	mathematical	—	`VAbs`	—	`VAbs_sum_sq_row_eq_one`
`VAbs_sum_sq_col_eq_one` 📖	mathematical	—	`VAbs`	—	—
`VAbs_sum_sq_row_eq_one` 📖	mathematical	—	`VAbs`	—	—
`VAbs_thd_eq_one_fst_eq_zero` 📖	—	`VAbs`	—	—	`VAbs_sum_sq_row_eq_one`
`VAbs_thd_eq_one_snd_eq_zero` 📖	—	`VAbs`	—	—	`VAbs_sum_sq_row_eq_one`
`VAbsub_neq_zero_Vud_Vus_neq_zero` 📖	—	—	—	—	`normSq_Vud_plus_normSq_Vus_neq_zero_ℝ` `ud_us_neq_zero_iff_ub_neq_one`
`VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero` 📖	—	—	—	—	`normSq_Vud_plus_normSq_Vus_neq_zero_ℝ` `ud_us_neq_zero_iff_ub_neq_one`
`Vabs_sq_add_neq_zero` 📖	—	—	—	—	`normSq_Vud_plus_normSq_Vus_neq_zero_ℂ`
`VcbAbs_sq_add_VtbAbs_sq` 📖	mathematical	—	`VcbAbs` `VtbAbs` `VubAbs`	—	`VAbs_sum_sq_col_eq_one`
`Vcd_mul_conj_Vud` 📖	—	—	—	—	`fst_row_orthog_snd_row`
`Vcs_mul_conj_Vus` 📖	—	—	—	—	`fst_row_orthog_snd_row`
`VudAbs_sq_add_VusAbs_sq` 📖	mathematical	—	`VudAbs` `VusAbs` `VubAbs`	—	`VAbs_sum_sq_row_eq_one`
`cb_eq_zero_of_ud_us_zero` 📖	—	—	—	—	`fst_row_normalized_abs` `thd_col_normalized_abs`
`cb_tb_neq_zero_iff_ub_neq_one` 📖	—	—	—	—	`thd_col_normalized_abs`
`cd_of_ud_us_ub_cb_tb` 📖	—	`tRow` `uRow` `cRow`	—	—	`normSq_Vud_plus_normSq_Vus_neq_zero_ℂ` `conj_Vtb_mul_Vus`
`conj_Vtb_cross_product` 📖	—	`tRow` `uRow` `cRow`	—	—	—
`conj_Vtb_mul_Vud` 📖	—	`tRow` `uRow` `cRow`	—	—	`conj_Vtb_cross_product` `Vcd_mul_conj_Vud`
`conj_Vtb_mul_Vus` 📖	—	`tRow` `uRow` `cRow`	—	—	`conj_Vtb_cross_product` `Vcs_mul_conj_Vus`
`cs_of_ud_us_ub_cb_tb` 📖	—	`tRow` `uRow` `cRow`	—	—	`normSq_Vud_plus_normSq_Vus_neq_zero_ℂ` `conj_Vtb_mul_Vud`
`cs_of_ud_us_zero` 📖	mathematical	—	`VcsAbs` `CKMMatrix` `CKMMatrixSetoid` `VcdAbs`	—	`snd_row_normalized_abs` `VAbs_leq_one` `VAbs_ge_zero` `cb_eq_zero_of_ud_us_zero`
`fst_row_normalized_abs` 📖	—	—	—	—	`VAbs_sum_sq_row_eq_one`
`fst_row_normalized_normSq` 📖	—	—	—	—	`fst_row_normalized_abs`
`fst_row_orthog_snd_row` 📖	—	—	—	—	—
`fst_row_orthog_thd_row` 📖	—	—	—	—	—
`normSq_Vud_plus_normSq_Vus` 📖	—	—	—	—	`fst_row_normalized_normSq`
`normSq_Vud_plus_normSq_Vus_neq_zero_ℂ` 📖	—	—	—	—	`normSq_Vud_plus_normSq_Vus_neq_zero_ℝ`
`normSq_Vud_plus_normSq_Vus_neq_zero_ℝ` 📖	—	—	—	—	`normSq_Vud_plus_normSq_Vus` `ud_us_neq_zero_iff_ub_neq_one`
`snd_row_normalized_abs` 📖	—	—	—	—	`VAbs_sum_sq_row_eq_one`
`snd_row_normalized_normSq` 📖	—	—	—	—	`snd_row_normalized_abs`
`thd_col_normalized_abs` 📖	—	—	—	—	`VAbs_sum_sq_col_eq_one`
`thd_col_normalized_normSq` 📖	—	—	—	—	`thd_col_normalized_abs`
`thd_row_normalized_abs` 📖	—	—	—	—	`VAbs_sum_sq_row_eq_one`
`thd_row_normalized_normSq` 📖	—	—	—	—	`thd_row_normalized_abs`
`ud_us_neq_zero_iff_ub_neq_one` 📖	—	—	—	—	`fst_row_normalized_abs`

---

← Back to Index