Documentation Verification Report

RatComplexNum

📁 Source: PhysLean/Mathematics/RatComplexNum.lean

Statistics

Metric	Count
Definitions `RatComplexNum`, `equivToProd`, `fst`, `instAdd`, `instAddCommGroup`, `instDecidableEq`, `instMul`, `instRing`, `snd`, `toComplexNum`	10
Theorems `I_mul_toComplexNum`, `add_fst`, `add_snd`, `ext`, `ext_iff`, `mul_fst`, `mul_snd`, `ofNat_mul_toComplexNum`, `one_fst`, `one_snd`, `toComplexNum_injective`, `zero_fst`, `zero_snd`	13
Total	23

PhysLean

Definitions

Name	Category	Theorems
`RatComplexNum` 📖	CompData	34 math math: `complexLorentzTensor.contrT_ofRat_eq_sum_dropPairSection`, `RatComplexNum.one_fst`, `complexLorentzTensor.altLeftLeftUnit_eq_ofRat`, `PauliMatrix.pauliCoDown_eq_ofRat`, `RatComplexNum.add_fst`, `complexLorentzTensor.altLeftMetric_eq_ofRat`, `complexLorentzTensor.ofRat_basis_repr_apply`, `RatComplexNum.mul_fst`, `complexLorentzTensor.permT_ofRat`, `RatComplexNum.I_mul_toComplexNum`, `complexLorentzTensor.coContrUnit_eq_ofRat`, `RatComplexNum.toComplexNum_injective`, `complexLorentzTensor.altRightMetric_eq_ofRat`, `PauliMatrix.pauliContrDown_ofRat`, `complexLorentzTensor.leftAltLeftUnit_eq_ofRat`, `complexLorentzTensor.altRightRightUnit_eq_ofRat`, `complexLorentzTensor.coMetric_eq_ofRat`, `complexLorentzTensor.basis_eq_ofRat`, `complexLorentzTensor.contrCoUnit_eq_ofRat`, `complexLorentzTensor.rightMetric_eq_ofRat`, `RatComplexNum.ofNat_mul_toComplexNum`, `complexLorentzTensor.rightAltRightUnit_eq_ofRat`, `complexLorentzTensor.contrT_ofRat`, `RatComplexNum.add_snd`, `RatComplexNum.mul_snd`, `complexLorentzTensor.leftMetric_eq_ofRat`, `RatComplexNum.zero_snd`, `complexLorentzTensor.contrMetric_eq_ofRat`, `complexLorentzTensor.prodT_ofRat_ofRat`, `RatComplexNum.zero_fst`, `PauliMatrix.toTensor_eq_ofRat`, `complexLorentzTensor.contr_basis_ratComplexNum`, `PauliMatrix.pauliCo_eq_ofRat`, `RatComplexNum.one_snd`

PhysLean.RatComplexNum

Definitions

Name	Category	Theorems
`equivToProd` 📖	CompOp	—
`fst` 📖	CompOp	6 math math: `one_fst`, `add_fst`, `mul_fst`, `ext_iff`, `mul_snd`, `zero_fst`
`instAdd` 📖	CompOp	2 math math: `add_fst`, `add_snd`
`instAddCommGroup` 📖	CompOp	6 math math: `complexLorentzTensor.altLeftMetric_eq_ofRat`, `complexLorentzTensor.altRightMetric_eq_ofRat`, `complexLorentzTensor.coMetric_eq_ofRat`, `complexLorentzTensor.rightMetric_eq_ofRat`, `complexLorentzTensor.leftMetric_eq_ofRat`, `complexLorentzTensor.contrMetric_eq_ofRat`
`instDecidableEq` 📖	CompOp	—
`instMul` 📖	CompOp	6 math math: `complexLorentzTensor.contrT_ofRat_eq_sum_dropPairSection`, `mul_fst`, `I_mul_toComplexNum`, `ofNat_mul_toComplexNum`, `mul_snd`, `complexLorentzTensor.prodT_ofRat_ofRat`
`instRing` 📖	CompOp	30 math math: `complexLorentzTensor.contrT_ofRat_eq_sum_dropPairSection`, `one_fst`, `complexLorentzTensor.altLeftLeftUnit_eq_ofRat`, `PauliMatrix.pauliCoDown_eq_ofRat`, `complexLorentzTensor.altLeftMetric_eq_ofRat`, `complexLorentzTensor.ofRat_basis_repr_apply`, `complexLorentzTensor.permT_ofRat`, `I_mul_toComplexNum`, `complexLorentzTensor.coContrUnit_eq_ofRat`, `toComplexNum_injective`, `complexLorentzTensor.altRightMetric_eq_ofRat`, `PauliMatrix.pauliContrDown_ofRat`, `complexLorentzTensor.leftAltLeftUnit_eq_ofRat`, `complexLorentzTensor.altRightRightUnit_eq_ofRat`, `complexLorentzTensor.coMetric_eq_ofRat`, `complexLorentzTensor.basis_eq_ofRat`, `complexLorentzTensor.contrCoUnit_eq_ofRat`, `complexLorentzTensor.rightMetric_eq_ofRat`, `ofNat_mul_toComplexNum`, `complexLorentzTensor.rightAltRightUnit_eq_ofRat`, `complexLorentzTensor.contrT_ofRat`, `complexLorentzTensor.leftMetric_eq_ofRat`, `zero_snd`, `complexLorentzTensor.contrMetric_eq_ofRat`, `complexLorentzTensor.prodT_ofRat_ofRat`, `zero_fst`, `PauliMatrix.toTensor_eq_ofRat`, `complexLorentzTensor.contr_basis_ratComplexNum`, `PauliMatrix.pauliCo_eq_ofRat`, `one_snd`
`snd` 📖	CompOp	6 math math: `mul_fst`, `ext_iff`, `add_snd`, `mul_snd`, `zero_snd`, `one_snd`
`toComplexNum` 📖	CompOp	26 math math: `complexLorentzTensor.contrT_ofRat_eq_sum_dropPairSection`, `complexLorentzTensor.altLeftLeftUnit_eq_ofRat`, `PauliMatrix.pauliCoDown_eq_ofRat`, `complexLorentzTensor.altLeftMetric_eq_ofRat`, `complexLorentzTensor.ofRat_basis_repr_apply`, `complexLorentzTensor.permT_ofRat`, `I_mul_toComplexNum`, `complexLorentzTensor.coContrUnit_eq_ofRat`, `toComplexNum_injective`, `complexLorentzTensor.altRightMetric_eq_ofRat`, `PauliMatrix.pauliContrDown_ofRat`, `complexLorentzTensor.leftAltLeftUnit_eq_ofRat`, `complexLorentzTensor.altRightRightUnit_eq_ofRat`, `complexLorentzTensor.coMetric_eq_ofRat`, `complexLorentzTensor.basis_eq_ofRat`, `complexLorentzTensor.contrCoUnit_eq_ofRat`, `complexLorentzTensor.rightMetric_eq_ofRat`, `ofNat_mul_toComplexNum`, `complexLorentzTensor.rightAltRightUnit_eq_ofRat`, `complexLorentzTensor.contrT_ofRat`, `complexLorentzTensor.leftMetric_eq_ofRat`, `complexLorentzTensor.contrMetric_eq_ofRat`, `complexLorentzTensor.prodT_ofRat_ofRat`, `PauliMatrix.toTensor_eq_ofRat`, `complexLorentzTensor.contr_basis_ratComplexNum`, `PauliMatrix.pauliCo_eq_ofRat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`I_mul_toComplexNum` 📖	mathematical	—	`PhysLean.RatComplexNum` `instRing` `toComplexNum` `instMul`	—	—
`add_fst` 📖	mathematical	—	`fst` `PhysLean.RatComplexNum` `instAdd`	—	—
`add_snd` 📖	mathematical	—	`snd` `PhysLean.RatComplexNum` `instAdd`	—	—
`ext` 📖	—	`fst` `snd`	—	—	—
`ext_iff` 📖	mathematical	—	`fst` `snd`	—	`ext`
`mul_fst` 📖	mathematical	—	`fst` `PhysLean.RatComplexNum` `instMul` `snd`	—	—
`mul_snd` 📖	mathematical	—	`snd` `PhysLean.RatComplexNum` `instMul` `fst`	—	—
`ofNat_mul_toComplexNum` 📖	mathematical	—	`PhysLean.RatComplexNum` `instRing` `toComplexNum` `instMul`	—	—
`one_fst` 📖	mathematical	—	`fst` `PhysLean.RatComplexNum` `instRing`	—	—
`one_snd` 📖	mathematical	—	`snd` `PhysLean.RatComplexNum` `instRing`	—	—
`toComplexNum_injective` 📖	mathematical	—	`PhysLean.RatComplexNum` `instRing` `toComplexNum`	—	`ext`
`zero_fst` 📖	mathematical	—	`fst` `PhysLean.RatComplexNum` `instRing`	—	—
`zero_snd` 📖	mathematical	—	`snd` `PhysLean.RatComplexNum` `instRing`	—	—

---

← Back to Index