Basic

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

Statistics

Metric	Count
Definitions `pauliMatrix`, `pauliMatrixInvertiable`, `termσ`, `termσ0`, `termσ1`, `termσ2`, `termσ3`	7
Theorems `pauliMatrix_inl_zero_eq_one`, `pauliMatrix_inv`, `pauliMatrix_mul_self`, `pauliMatrix_selfAdjoint`, `trace_σ1`, `trace_σ2`, `trace_σ3`, `σ0_σ0_trace`, `σ0_σ1_trace`, `σ0_σ2_trace`, `σ0_σ3_trace`, `σ1_σ0_trace`, `σ1_σ1_trace`, `σ1_σ2_commutator`, `σ1_σ2_trace`, `σ1_σ3_commutator`, `σ1_σ3_trace`, `σ2_mul_σ1`, `σ2_σ0_trace`, `σ2_σ1_commutator`, `σ2_σ1_trace`, `σ2_σ2_trace`, `σ2_σ3_commutator`, `σ2_σ3_trace`, `σ3_mul_σ1`, `σ3_mul_σ2`, `σ3_σ0_trace`, `σ3_σ1_commutator`, `σ3_σ1_trace`, `σ3_σ2_commutator`, `σ3_σ2_trace`, `σ3_σ3_trace`	32
Total	39

PauliMatrix

Definitions

Name	Category	Theorems
`pauliMatrix` 📖	CompOp	50 math math: `Lorentz.ContrMod.toSelfAdjoint_apply_coe`, `pauliCo_contr_pauliContr`, `σ2_σ3_trace`, `σ3_σ2_commutator`, `σ2_σ1_commutator`, `trace_σ2`, `pauliBasis'_repr_inr_1`, `σ1_σ0_trace`, `pauliMatrix_inl_zero_eq_one`, `σ2_σ1_trace`, `TwoHiggsDoublet.gramMatrix_eq_gramVector_sum_pauliMatrix`, `σ2_σ3_commutator`, `σ0_σ1_trace`, `toTensor_smul_eq_self`, `σ1_σ3_trace`, `trace_pauliMatrix_mul_selfAdjoint_re`, `pauliBasis'_decomp`, `pauliBasis'_repr_inr_2`, `trace_σ1`, `pauliBasis'_repr_inl_0`, `σ2_mul_σ1`, `Lorentz.ContrMod.toSelfAdjoint_apply`, `σ0_σ0_trace`, `σ1_σ1_trace`, `σ3_mul_σ2`, `ofCliffordAlgebra_ι_single`, `pauliMatrix_inv`, `pauliMatrix_mul_self`, `trace_σ3`, `smul_eq_self`, `toTensor_basis_expand`, `σ3_σ0_trace`, `σ1_σ2_trace`, `pauliMatrix_selfAdjoint`, `σ3_σ1_commutator`, `pauliBasis'_repr_inr_0`, `σ0_σ2_trace`, `auliContrDown_pauliContr_mul_add`, `σ2_σ0_trace`, `σ0_σ3_trace`, `σ3_σ1_trace`, `toTensor_eq_asConsTensor`, `toTensor_eq_ofRat`, `σ1_σ2_commutator`, `σ1_σ3_commutator`, `pauliContr_mul_pauliContrDown_add`, `σ3_σ2_trace`, `σ2_σ2_trace`, `σ3_mul_σ1`, `σ3_σ3_trace`
`pauliMatrixInvertiable` 📖	CompOp	1 math math: `pauliMatrix_inv`
`termσ` 📖	CompOp	—
`termσ0` 📖	CompOp	—
`termσ1` 📖	CompOp	—
`termσ2` 📖	CompOp	—
`termσ3` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pauliMatrix_inl_zero_eq_one` 📖	mathematical	—	`pauliMatrix`	—	—
`pauliMatrix_inv` 📖	mathematical	—	`pauliMatrix` `pauliMatrixInvertiable`	—	—
`pauliMatrix_mul_self` 📖	mathematical	—	`pauliMatrix`	—	—
`pauliMatrix_selfAdjoint` 📖	mathematical	—	`pauliMatrix`	—	—
`trace_σ1` 📖	mathematical	—	`pauliMatrix`	—	—
`trace_σ2` 📖	mathematical	—	`pauliMatrix`	—	—
`trace_σ3` 📖	mathematical	—	`pauliMatrix`	—	—
`σ0_σ0_trace` 📖	mathematical	—	`pauliMatrix`	—	`pauliMatrix_mul_self`
`σ0_σ1_trace` 📖	mathematical	—	`pauliMatrix`	—	—
`σ0_σ2_trace` 📖	mathematical	—	`pauliMatrix`	—	—
`σ0_σ3_trace` 📖	mathematical	—	`pauliMatrix`	—	—
`σ1_σ0_trace` 📖	mathematical	—	`pauliMatrix`	—	—
`σ1_σ1_trace` 📖	mathematical	—	`pauliMatrix`	—	`pauliMatrix_mul_self`
`σ1_σ2_commutator` 📖	mathematical	—	`pauliMatrix`	—	—
`σ1_σ2_trace` 📖	mathematical	—	`pauliMatrix`	—	—
`σ1_σ3_commutator` 📖	mathematical	—	`pauliMatrix`	—	—
`σ1_σ3_trace` 📖	mathematical	—	`pauliMatrix`	—	—
`σ2_mul_σ1` 📖	mathematical	—	`pauliMatrix`	—	—
`σ2_σ0_trace` 📖	mathematical	—	`pauliMatrix`	—	—
`σ2_σ1_commutator` 📖	mathematical	—	`pauliMatrix`	—	—
`σ2_σ1_trace` 📖	mathematical	—	`pauliMatrix`	—	—
`σ2_σ2_trace` 📖	mathematical	—	`pauliMatrix`	—	`pauliMatrix_mul_self`
`σ2_σ3_commutator` 📖	mathematical	—	`pauliMatrix`	—	—
`σ2_σ3_trace` 📖	mathematical	—	`pauliMatrix`	—	—
`σ3_mul_σ1` 📖	mathematical	—	`pauliMatrix`	—	—
`σ3_mul_σ2` 📖	mathematical	—	`pauliMatrix`	—	—
`σ3_σ0_trace` 📖	mathematical	—	`pauliMatrix`	—	—
`σ3_σ1_commutator` 📖	mathematical	—	`pauliMatrix`	—	—
`σ3_σ1_trace` 📖	mathematical	—	`pauliMatrix`	—	`σ3_mul_σ1` `σ1_σ3_trace`
`σ3_σ2_commutator` 📖	mathematical	—	`pauliMatrix`	—	—
`σ3_σ2_trace` 📖	mathematical	—	`pauliMatrix`	—	`σ3_mul_σ2` `σ2_σ3_trace`
`σ3_σ3_trace` 📖	mathematical	—	`pauliMatrix`	—	`pauliMatrix_mul_self`

---

← Back to Index