Documentation Verification Report

Basic

📁 Source: PhysLean/Relativity/Tensors/Contraction/Basic.lean

Statistics

Metric	Count
Definitions `contrT`	1
Theorems `contrT_comm`, `contrT_congr`, `contrT_decide`, `contrT_equivariant`, `contrT_permT`, `contrT_pure`, `contrT_symm`	7
Total	8

TensorSpecies.Tensor

Definitions

Name	Category	Theorems
`contrT` 📖	CompOp	49 math math: `complexLorentzTensor.contrT_ofRat_eq_sum_dropPairSection`, `complexLorentzTensor.contrMetric_contr_coMetric`, `PauliMatrix.pauliCo_contr_pauliContr`, `contrT_fromSingleT_fromPairT`, `TensorSpecies.contrT_unitTensor_dual_single`, `complexLorentzTensor.altLeftMetric_contr_leftMetric`, `contrT_congr`, `realLorentzTensor.contrT_toComplex`, `contrT_comm`, `complexLorentzTensor.leftMetric_contr_altLeftMetric`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor`, `PauliMatrix.pauliCoDown_trace_pauliCo`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv`, `TensorSpecies.contrT_metricTensor_metricTensor`, `fromDualMap_apply`, `complexLorentzTensor.coMetric_contr_contrMetric`, `Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor`, `contrT_permT`, `contrT_equivariant`, `contrT_prodT_snd`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add`, `Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength`, `contrT_basis_repr_apply_eq_sum_fin`, `toDualMap_apply`, `contrT_fromSingleT_fromSingleT`, `complexLorentzTensor.contrT_ofRat`, `TensorSpecies.contrT_single_unitTensor`, `complexLorentzTensor.altRightMetric_contr_rightMetric`, `realLorentzTensor.contrT_basis_repr_apply_eq_dropPairSection`, `contrT_pure`, `Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux`, `Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors`, `fromPairT_contr_fromPairT_eq_fromPairTContr`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv`, `prodT_contrT_snd`, `fromPairT_contr_fromPairT_eq_fromPairTContr_tmul`, `contrT_basis_repr_apply`, `PauliMatrix.auliContrDown_pauliContr_mul_add`, `TensorSpecies.contrT_dual_metricTensor_metricTensor`, `TensorSpecies.contrT_metricTensor_metricTensor_eq_dual_unit`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add`, `contrT_symm`, `PauliMatrix.pauliContr_mul_pauliContrDown_add`, `complexLorentzTensor.rightMetric_contr_altRightMetric`, `complexLorentzTensor.antiSymm_contr_symm`, `realLorentzTensor.contrT_basis_repr_apply_eq_fin`, `PauliMatrix.pauliCo_trace_pauliCoDown`, `fromSingleT_contr_fromPairT_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contrT_comm` 📖	mathematical	`TensorSpecies.τ` `Pure.dropPairEmb`	`TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `contrT` `Pure.dropPairEmbPre` `permT` `Pure.permCond_dropPairEmb_comm` `Pure.dropPairEmb_dropPairEmbPre`	—	`Pure.permCond_dropPairEmb_comm` `Pure.dropPairEmb_dropPairEmbPre` `induction_on_pure` `contrT_pure` `Pure.contrP.eq_1` `permT_pure` `Pure.contrPCoeff_mul_dropPair` `Pure.dropPair_comm`
`contrT_congr` 📖	mathematical	`TensorSpecies.τ`	`TensorSpecies.Tensor` `Pure.dropPairEmb` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `contrT` `permT`	—	`permT_id_self`
`contrT_decide` 📖	—	`TensorSpecies.τ`	—	—	—
`contrT_equivariant` 📖	mathematical	`TensorSpecies.τ`	`TensorSpecies.Tensor` `Pure.dropPairEmb` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `contrT` `actionT`	—	`induction_on_pure` `contrT_pure` `actionT_pure` `Pure.contrPCoeff_invariant` `Pure.dropPair_equivariant` `actionT_smul` `actionT_add`
`contrT_permT` 📖	mathematical	`TensorSpecies.τ` `PermCond`	`TensorSpecies.Tensor` `Pure.dropPairEmb` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `contrT` `permT` `Pure.dropPairOfMap` `Pure.permCond_dropPairOfMap`	—	`Pure.permCond_dropPairOfMap` `induction_on_pure` `contrT_pure` `permT_pure` `Pure.contrPCoeff_permP` `Pure.dropPair_permP`
`contrT_pure` 📖	mathematical	`TensorSpecies.τ`	`TensorSpecies.Tensor` `Pure.dropPairEmb` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `contrT` `Pure.toTensor` `Pure.contrP`	—	—
`contrT_symm` 📖	mathematical	`TensorSpecies.τ`	`TensorSpecies.Tensor` `Pure.dropPairEmb` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `contrT` `permT` `PermCond` `Pure.permCond_dropPairEmb_symm` `TensorSpecies.τ_τ_apply`	—	`Pure.permCond_dropPairEmb_symm` `TensorSpecies.τ_τ_apply` `induction_on_pure` `contrT_pure` `Pure.contrP_symm` `permT_congr`

---

← Back to Index