Documentation Verification Report

SelfAdjoint

📁 Source: PhysLean/Relativity/PauliMatrices/SelfAdjoint.lean

Statistics

Metric	Count
Definitions `pauliBasis`, `pauliBasis'`, `pauliSelfAdjoint`, `pauliSelfAdjoint'`	4
Theorems `pauliBasis'_decomp`, `pauliBasis'_repr_inl_0`, `pauliBasis'_repr_inr_0`, `pauliBasis'_repr_inr_1`, `pauliBasis'_repr_inr_2`, `pauliBasis_minkowskiMetric_pauliBasis'`, `pauliSelfAdjoint'_linearly_independent`, `pauliSelfAdjoint'_span`, `pauliSelfAdjoint_linearly_independent`, `pauliSelfAdjoint_span`, `selfAdjoint_ext`, `selfAdjoint_ext_complex`, `trace_pauliMatrix_mul_selfAdjoint_re`	13
Total	17

PauliMatrix

Definitions

Name	Category	Theorems
`pauliBasis` 📖	CompOp	7 math math: `Lorentz.SL2C.toSelfAdjointMap_pauliBasis`, `leftRightToMatrix_σSA_inl_0_expand`, `leftRightToMatrix_σSA_inr_1_expand`, `asTensor_expand_complexContrBasis`, `pauliBasis_minkowskiMetric_pauliBasis'`, `leftRightToMatrix_σSA_inr_0_expand`, `leftRightToMatrix_σSA_inr_2_expand`
`pauliBasis'` 📖	CompOp	11 math math: `pauliBasis'_repr_inr_1`, `pauliBasis'_decomp`, `pauliBasis'_repr_inr_2`, `Lorentz.ContrMod.toSelfAdjoint_stdBasis`, `pauliBasis'_repr_inl_0`, `Lorentz.SL2C.toLorentzGroup_eq_pauliBasis'`, `pauliBasis'_repr_inr_0`, `pauliBasis_minkowskiMetric_pauliBasis'`, `Lorentz.SL2C.toSelfAdjointMap_basis`, `Lorentz.SL2C.toSelfAdjointMap_apply_pauliBasis'_inl`, `Lorentz.ContrMod.toSelfAdjoint_symm_basis`
`pauliSelfAdjoint` 📖	CompOp	2 math math: `pauliSelfAdjoint_span`, `pauliSelfAdjoint_linearly_independent`
`pauliSelfAdjoint'` 📖	CompOp	2 math math: `pauliSelfAdjoint'_linearly_independent`, `pauliSelfAdjoint'_span`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pauliBasis'_decomp` 📖	mathematical	—	`pauliMatrix` `pauliBasis'`	—	`selfAdjoint_ext` `pauliSelfAdjoint'_linearly_independent` `pauliSelfAdjoint'_span` `σ0_σ0_trace` `σ0_σ1_trace` `σ0_σ2_trace` `σ0_σ3_trace` `σ1_σ0_trace` `σ1_σ1_trace` `σ1_σ2_trace` `σ1_σ3_trace` `σ2_σ0_trace` `σ2_σ1_trace` `σ2_σ2_trace` `σ2_σ3_trace` `σ3_σ0_trace` `σ3_σ1_trace` `σ3_σ2_trace` `σ3_σ3_trace`
`pauliBasis'_repr_inl_0` 📖	mathematical	—	`pauliBasis'` `pauliMatrix`	—	`pauliSelfAdjoint'_linearly_independent` `pauliSelfAdjoint'_span` `σ0_σ0_trace` `σ0_σ1_trace` `σ0_σ2_trace` `σ0_σ3_trace`
`pauliBasis'_repr_inr_0` 📖	mathematical	—	`pauliBasis'` `pauliMatrix`	—	`pauliSelfAdjoint'_linearly_independent` `pauliSelfAdjoint'_span` `σ1_σ0_trace` `σ1_σ1_trace` `σ1_σ2_trace` `σ1_σ3_trace`
`pauliBasis'_repr_inr_1` 📖	mathematical	—	`pauliBasis'` `pauliMatrix`	—	`pauliSelfAdjoint'_linearly_independent` `pauliSelfAdjoint'_span` `σ2_σ0_trace` `σ2_σ1_trace` `σ2_σ2_trace` `σ2_σ3_trace`
`pauliBasis'_repr_inr_2` 📖	mathematical	—	`pauliBasis'` `pauliMatrix`	—	`pauliSelfAdjoint'_linearly_independent` `pauliSelfAdjoint'_span` `σ3_σ0_trace` `σ3_σ1_trace` `σ3_σ2_trace` `σ3_σ3_trace`
`pauliBasis_minkowskiMetric_pauliBasis'` 📖	mathematical	—	`pauliBasis` `minkowskiMatrix` `pauliBasis'`	—	`pauliSelfAdjoint_linearly_independent` `pauliSelfAdjoint_span` `pauliSelfAdjoint'_linearly_independent` `pauliSelfAdjoint'_span` `minkowskiMatrix.inl_0_inl_0` `pauliMatrix_selfAdjoint` `minkowskiMatrix.inr_i_inr_i`
`pauliSelfAdjoint'_linearly_independent` 📖	mathematical	—	`pauliSelfAdjoint'`	—	—
`pauliSelfAdjoint'_span` 📖	mathematical	—	`pauliSelfAdjoint'`	—	`selfAdjoint_ext` `σ0_σ0_trace` `σ0_σ1_trace` `σ0_σ2_trace` `σ0_σ3_trace` `σ1_σ0_trace` `σ1_σ1_trace` `σ1_σ2_trace` `σ1_σ3_trace` `σ2_σ0_trace` `σ2_σ1_trace` `σ2_σ2_trace` `σ2_σ3_trace` `σ3_σ0_trace` `σ3_σ1_trace` `σ3_σ2_trace` `σ3_σ3_trace`
`pauliSelfAdjoint_linearly_independent` 📖	mathematical	—	`pauliSelfAdjoint`	—	`pauliMatrix_selfAdjoint`
`pauliSelfAdjoint_span` 📖	mathematical	—	`pauliSelfAdjoint`	—	`selfAdjoint_ext` `σ0_σ0_trace` `σ0_σ1_trace` `σ0_σ2_trace` `σ0_σ3_trace` `σ1_σ0_trace` `σ1_σ1_trace` `σ1_σ2_trace` `σ1_σ3_trace` `σ2_σ0_trace` `σ2_σ1_trace` `σ2_σ2_trace` `σ2_σ3_trace` `σ3_σ0_trace` `σ3_σ1_trace` `σ3_σ2_trace` `σ3_σ3_trace`
`selfAdjoint_ext` 📖	—	`pauliMatrix`	—	—	`selfAdjoint_ext_complex` `trace_pauliMatrix_mul_selfAdjoint_re`
`selfAdjoint_ext_complex` 📖	—	`pauliMatrix`	—	—	`pauliMatrix_inl_zero_eq_one`
`trace_pauliMatrix_mul_selfAdjoint_re` 📖	mathematical	—	`pauliMatrix`	—	`pauliMatrix_selfAdjoint`

---

← Back to Index