Documentation Verification Report

Rows

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

Statistics

Metric	Count
Definitions `cRow`, `c_row`, `rowBasis`, `rows`, `tRow`, `t_row`, `uRow`, `u_row`, `ucCross`	9
Theorems `cRow_cross_tRow_conj`, `cRow_cross_tRow_eq_uRow`, `cRow_cross_tRow_normalized`, `cRow_normalized`, `cRow_tRow_orthog`, `cRow_uRow_orthog`, `ext_Rows`, `rowBasis_repr_apply`, `rowBasis_repr_symm_apply`, `rows_linearly_independent`, `tRow_cRow_orthog`, `tRow_normalized`, `tRow_uRow_orthog`, `uRow_cRow_orthog`, `uRow_cross_cRow_conj`, `uRow_cross_cRow_eq_tRow`, `uRow_cross_cRow_normalized`, `uRow_normalized`, `uRow_tRow_orthog`, `cRow_mul`, `tRow_mul`, `uRow_mul`, `ucCross_fst`, `ucCross_snd`, `ucCross_thd`	25
Total	34

CKMMatrix

Definitions

Name	Category	Theorems
`cRow` 📖	CompOp	16 math math: `cRow_cross_tRow_eq_uRow`, `phaseShiftApply.cRow_mul`, `standParam.cross_product_t`, `cRow_normalized`, `uRow_cross_cRow_normalized`, `cRow_tRow_orthog`, `cRow_cross_tRow_normalized`, `cRow_uRow_orthog`, `phaseShiftApply.ucCross_thd`, `cRow_cross_tRow_conj`, `tRow_cRow_orthog`, `uRow_cRow_orthog`, `uRow_cross_cRow_conj`, `phaseShiftApply.ucCross_snd`, `phaseShiftApply.ucCross_fst`, `uRow_cross_cRow_eq_tRow`
`c_row` 📖	CompOp	—
`rowBasis` 📖	CompOp	2 math math: `rowBasis_repr_symm_apply`, `rowBasis_repr_apply`
`rows` 📖	CompOp	3 math math: `rowBasis_repr_symm_apply`, `rowBasis_repr_apply`, `rows_linearly_independent`
`tRow` 📖	CompOp	11 math math: `cRow_cross_tRow_eq_uRow`, `tRow_uRow_orthog`, `standParam.cross_product_t`, `cRow_tRow_orthog`, `tRow_normalized`, `cRow_cross_tRow_normalized`, `cRow_cross_tRow_conj`, `phaseShiftApply.tRow_mul`, `tRow_cRow_orthog`, `uRow_tRow_orthog`, `uRow_cross_cRow_eq_tRow`
`t_row` 📖	CompOp	—
`uRow` 📖	CompOp	14 math math: `phaseShiftApply.uRow_mul`, `uRow_normalized`, `cRow_cross_tRow_eq_uRow`, `tRow_uRow_orthog`, `standParam.cross_product_t`, `uRow_cross_cRow_normalized`, `cRow_uRow_orthog`, `phaseShiftApply.ucCross_thd`, `uRow_cRow_orthog`, `uRow_cross_cRow_conj`, `phaseShiftApply.ucCross_snd`, `uRow_tRow_orthog`, `phaseShiftApply.ucCross_fst`, `uRow_cross_cRow_eq_tRow`
`u_row` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cRow_cross_tRow_conj` 📖	mathematical	—	`cRow` `tRow`	—	—
`cRow_cross_tRow_eq_uRow` 📖	mathematical	—	`uRow` `cRow` `tRow`	—	`rows_linearly_independent` `cRow_tRow_orthog` `cRow_uRow_orthog` `cRow_normalized` `tRow_cRow_orthog` `tRow_uRow_orthog` `tRow_normalized` `uRow_normalized` `cRow_cross_tRow_normalized`
`cRow_cross_tRow_normalized` 📖	mathematical	—	`cRow` `tRow`	—	`cRow_cross_tRow_conj` `cRow_normalized` `tRow_normalized` `tRow_cRow_orthog` `cRow_tRow_orthog`
`cRow_normalized` 📖	mathematical	—	`cRow`	—	—
`cRow_tRow_orthog` 📖	mathematical	—	`cRow` `tRow`	—	—
`cRow_uRow_orthog` 📖	mathematical	—	`cRow` `uRow`	—	—
`ext_Rows` 📖	—	`uRow` `cRow` `tRow`	—	—	`CKMMatrix_ext`
`rowBasis_repr_apply` 📖	mathematical	—	`rowBasis` `rows` `rows_linearly_independent`	—	—
`rowBasis_repr_symm_apply` 📖	mathematical	—	`rowBasis` `rows`	—	—
`rows_linearly_independent` 📖	mathematical	—	`rows`	—	`uRow_tRow_orthog` `uRow_cRow_orthog` `uRow_normalized` `cRow_tRow_orthog` `cRow_uRow_orthog` `cRow_normalized` `tRow_cRow_orthog` `tRow_uRow_orthog` `tRow_normalized`
`tRow_cRow_orthog` 📖	mathematical	—	`tRow` `cRow`	—	—
`tRow_normalized` 📖	mathematical	—	`tRow`	—	—
`tRow_uRow_orthog` 📖	mathematical	—	`tRow` `uRow`	—	—
`uRow_cRow_orthog` 📖	mathematical	—	`uRow` `cRow`	—	—
`uRow_cross_cRow_conj` 📖	mathematical	—	`uRow` `cRow`	—	—
`uRow_cross_cRow_eq_tRow` 📖	mathematical	—	`tRow` `uRow` `cRow`	—	`rows_linearly_independent` `rowBasis.eq_1` `uRow_tRow_orthog` `uRow_cRow_orthog` `uRow_normalized` `cRow_tRow_orthog` `cRow_uRow_orthog` `cRow_normalized` `tRow_normalized` `uRow_cross_cRow_normalized`
`uRow_cross_cRow_normalized` 📖	mathematical	—	`uRow` `cRow`	—	`uRow_cross_cRow_conj` `uRow_normalized` `cRow_normalized` `cRow_uRow_orthog` `uRow_cRow_orthog`
`uRow_normalized` 📖	mathematical	—	`uRow`	—	—
`uRow_tRow_orthog` 📖	mathematical	—	`uRow` `tRow`	—	—

phaseShiftApply

Definitions

Name	Category	Theorems
`ucCross` 📖	CompOp	3 math math: `ucCross_thd`, `ucCross_snd`, `ucCross_fst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cRow_mul` 📖	mathematical	—	`CKMMatrix.cRow` `phaseShiftApply`	—	`cd` `cs` `cb`
`tRow_mul` 📖	mathematical	—	`CKMMatrix.tRow` `phaseShiftApply`	—	`td` `ts` `tb`
`uRow_mul` 📖	mathematical	—	`CKMMatrix.uRow` `phaseShiftApply`	—	`ud` `us` `ub`
`ucCross_fst` 📖	mathematical	—	`ucCross` `CKMMatrix.uRow` `CKMMatrix.cRow`	—	`us` `ub` `cs` `cb`
`ucCross_snd` 📖	mathematical	—	`ucCross` `CKMMatrix.uRow` `CKMMatrix.cRow`	—	`ud` `us` `ub` `cd` `cs` `cb`
`ucCross_thd` 📖	mathematical	—	`ucCross` `CKMMatrix.uRow` `CKMMatrix.cRow`	—	`ud` `us` `ub` `cd` `cs` `cb`

---

← Back to Index