Pure

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

Statistics

Metric	Count
Definitions `Pure`, `contrP`, `contrPCoeff`, `contrPMultilinear`, `dropPair`, `dropPairEmb`, `dropPairEmbPre`, `dropPairOfMap`	8
Theorems `contrPCoeff_dropPair`, `contrPCoeff_invariant`, `contrPCoeff_mul_dropPair`, `contrPCoeff_permP`, `contrPCoeff_symm`, `contrPCoeff_update_dropPairEmb`, `contrPCoeff_update_fst_add`, `contrPCoeff_update_fst_smul`, `contrPCoeff_update_snd_add`, `contrPCoeff_update_snd_smul`, `contrP_equivariant`, `contrP_symm`, `contrP_update_add`, `contrP_update_smul`, `dropPairEmbPre_dropPairEmb`, `dropPairEmbPre_eq_orderIsoOfFin`, `dropPairEmbPre_injective`, `dropPairEmbPre_surjective`, `dropPairEmb_apply_eq_orderIsoOfFin`, `dropPairEmb_comm`, `dropPairEmb_comm_apply`, `dropPairEmb_dropPairEmbPre`, `dropPairEmb_eq_iff_eq`, `dropPairEmb_eq_orderEmbOfFin`, `dropPairEmb_eq_succAbove_succAbove`, `dropPairEmb_image_compl`, `dropPairEmb_injective`, `dropPairEmb_leq_iff_leq`, `dropPairEmb_lt_iff_lt`, `dropPairEmb_monotone`, `dropPairEmb_neq_fst`, `dropPairEmb_neq_snd`, `dropPairEmb_range`, `dropPairEmb_self_apply`, `dropPairEmb_succAbove`, `dropPairEmb_symm`, `dropPairOfMap_bijective`, `dropPairOfMap_id`, `dropPairOfMap_injective`, `dropPairOfMap_surjective`, `dropPair_comm`, `dropPair_equivariant`, `dropPair_permP`, `dropPair_symm`, `dropPair_update_dropPairEmb`, `dropPair_update_fst`, `dropPair_update_snd`, `eq_or_exists_dropPairEmb`, `fst_neq_dropPairEmb_pre`, `permCond_dropPairEmb_comm`, `permCond_dropPairEmb_symm`, `permCond_dropPairOfMap`, `snd_neq_dropPairEmb_pre`	53
Total	61

TensorSpecies.Tensor

Definitions

Name	Category	Theorems
`Pure` 📖	CompOp	12 math math: `Pure.drop_actionP`, `toField_default`, `contrT_fromSingleT_fromSingleT`, `Pure.prodP_equivariant`, `Pure.contrP_equivariant`, `Pure.dropPair_equivariant`, `prodIndexEquiv_symm_pure`, `Pure.actionP_eq`, `actionT_pure`, `Pure.contrPCoeff_invariant`, `fromSingleT_symm_pure`, `prodT_default_right`

TensorSpecies.Tensor.Pure

Definitions

Name	Category	Theorems
`contrP` 📖	CompOp	6 math math: `contrP_symm`, `contrP_update_add`, `TensorSpecies.Tensor.contrT_pure`, `contrP_equivariant`, `prodP_contrP_snd`, `contrP_update_smul`
`contrPCoeff` 📖	CompOp	12 math math: `contrPCoeff_update_fst_smul`, `contrPCoeff_dropPair`, `contrPCoeff_update_dropPairEmb`, `contrPCoeff_update_snd_add`, `contrPCoeff_castAdd`, `contrPCoeff_update_fst_add`, `contrPCoeff_mul_dropPair`, `contrPCoeff_symm`, `contrPCoeff_update_snd_smul`, `contrPCoeff_invariant`, `contrPCoeff_natAdd`, `contrPCoeff_permP`
`contrPMultilinear` 📖	CompOp	—
`dropPair` 📖	CompOp	11 math math: `contrPCoeff_dropPair`, `dropPair_comm`, `dropPair_update_snd`, `dropPair_basisVector`, `contrPCoeff_mul_dropPair`, `dropPair_update_dropPairEmb`, `dropPair_equivariant`, `dropPair_update_fst`, `dropPair_permP`, `dropPair_symm`, `prodP_dropPair`
`dropPairEmb` 📖	CompOp	92 math math: `permCond_dropPairEmb_symm`, `complexLorentzTensor.contrT_ofRat_eq_sum_dropPairSection`, `complexLorentzTensor.contrMetric_contr_coMetric`, `dropPairEmb_apply_lt_lt`, `PauliMatrix.pauliCo_contr_pauliContr`, `eq_or_exists_dropPairEmb`, `TensorSpecies.Tensor.contrT_fromSingleT_fromPairT`, `TensorSpecies.contrT_unitTensor_dual_single`, `complexLorentzTensor.altLeftMetric_contr_leftMetric`, `dropPairEmb_leq_iff_leq`, `dropPairEmb_eq_succAbove_succAbove`, `TensorSpecies.Tensor.contrT_congr`, `dropPairEmb_symm`, `realLorentzTensor.contrT_toComplex`, `dropPairEmb_permCond_prod`, `complexLorentzTensor.leftMetric_contr_altLeftMetric`, `dropPairEmb_comm`, `dropPairEmb_self_apply`, `dropPairEmb_range`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor`, `dropPairEmbPre_dropPairEmb`, `PauliMatrix.pauliCoDown_trace_pauliCo`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv`, `TensorSpecies.contrT_metricTensor_metricTensor`, `TensorSpecies.Tensor.fromDualMap_apply`, `dropPairEmb_image_compl`, `permCond_dropPairOfMap`, `complexLorentzTensor.coMetric_contr_contrMetric`, `Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor`, `TensorSpecies.Tensor.contrT_permT`, `contrP_symm`, `TensorSpecies.Tensor.contrT_equivariant`, `TensorSpecies.Tensor.contrT_prodT_snd`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add`, `dropPairEmb_injective`, `dropPair_comm`, `dropPairEmb_natAdd_image_range_castAdd`, `contrPCoeff_update_dropPairEmb`, `Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength`, `dropPairEmb_eq_orderEmbOfFin`, `TensorSpecies.Tensor.contrT_basis_repr_apply_eq_sum_fin`, `contrP_update_add`, `TensorSpecies.Tensor.toDualMap_apply`, `TensorSpecies.Tensor.contrT_fromSingleT_fromSingleT`, `fst_neq_dropPairEmb_pre`, `complexLorentzTensor.contrT_ofRat`, `dropPairEmb_comm_natAdd`, `TensorSpecies.contrT_single_unitTensor`, `snd_neq_dropPairEmb_pre`, `complexLorentzTensor.altRightMetric_contr_rightMetric`, `realLorentzTensor.contrT_basis_repr_apply_eq_dropPairSection`, `dropPairEmb_comm_apply`, `dropPair_basisVector`, `TensorSpecies.Tensor.contrT_pure`, `Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux`, `Electromagnetism.ElectromagneticPotential.isExtrema_iff_tensors`, `dropPair_update_dropPairEmb`, `TensorSpecies.Tensor.fromPairT_contr_fromPairT_eq_fromPairTContr`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv`, `dropPairEmb_neq_fst`, `contrP_equivariant`, `prodP_contrP_snd`, `dropPair_equivariant`, `dropPairEmb_monotone`, `TensorSpecies.Tensor.prodT_contrT_snd`, `TensorSpecies.Tensor.fromPairT_contr_fromPairT_eq_fromPairTContr_tmul`, `dropPairEmb_dropPairEmbPre`, `TensorSpecies.Tensor.contrT_basis_repr_apply`, `dropPairEmb_apply_eq_orderIsoOfFin`, `PauliMatrix.auliContrDown_pauliContr_mul_add`, `permCond_dropPairEmb_comm`, `dropPairEmb_neq_snd`, `TensorSpecies.contrT_dual_metricTensor_metricTensor`, `dropPairEmb_lt_iff_lt`, `TensorSpecies.contrT_metricTensor_metricTensor_eq_dual_unit`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add`, `dropPairEmb_succAbove`, `TensorSpecies.Tensor.contrT_symm`, `dropPairEmb_eq_iff_eq`, `PauliMatrix.pauliContr_mul_pauliContrDown_add`, `contrP_update_smul`, `dropPairEmb_natAdd_apply_castAdd`, `complexLorentzTensor.rightMetric_contr_altRightMetric`, `complexLorentzTensor.antiSymm_contr_symm`, `dropPair_permP`, `dropPair_symm`, `realLorentzTensor.contrT_basis_repr_apply_eq_fin`, `TensorSpecies.Tensor.ComponentIdx.DropPairSection.mem_iff_apply_dropPairEmb_eq`, `PauliMatrix.pauliCo_trace_pauliCoDown`, `prodP_dropPair`, `TensorSpecies.Tensor.fromSingleT_contr_fromPairT_tmul`
`dropPairEmbPre` 📖	CompOp	11 math math: `dropPairEmbPre_injective`, `TensorSpecies.Tensor.contrT_comm`, `dropPairEmbPre_eq_orderIsoOfFin`, `dropPairEmb_comm`, `dropPairEmbPre_dropPairEmb`, `dropPair_comm`, `dropPairEmb_comm_apply`, `contrPCoeff_mul_dropPair`, `dropPairEmb_dropPairEmbPre`, `permCond_dropPairEmb_comm`, `dropPairEmbPre_surjective`
`dropPairOfMap` 📖	CompOp	7 math math: `permCond_dropPairOfMap`, `TensorSpecies.Tensor.contrT_permT`, `dropPairOfMap_bijective`, `dropPairOfMap_id`, `dropPairOfMap_injective`, `dropPairOfMap_surjective`, `dropPair_permP`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contrPCoeff_dropPair` 📖	mathematical	`TensorSpecies.τ` `dropPairEmb`	`contrPCoeff` `dropPair`	—	—
`contrPCoeff_invariant` 📖	mathematical	`TensorSpecies.τ`	`contrPCoeff` `TensorSpecies.Tensor.Pure` `instSMul`	—	—
`contrPCoeff_mul_dropPair` 📖	mathematical	`TensorSpecies.τ` `dropPairEmb`	`contrPCoeff` `dropPair` `dropPairEmbPre` `dropPairEmb_dropPairEmbPre`	—	`dropPairEmb_dropPairEmbPre` `contrPCoeff_dropPair` `contrPCoeff.congr_simp`
`contrPCoeff_permP` 📖	mathematical	`TensorSpecies.τ` `TensorSpecies.Tensor.PermCond`	`contrPCoeff` `permP`	—	`TensorSpecies.contr_congr`
`contrPCoeff_symm` 📖	mathematical	`TensorSpecies.τ`	`contrPCoeff` `TensorSpecies.τ_τ_apply`	—	`TensorSpecies.τ_τ_apply` `contrPCoeff.eq_1` `TensorSpecies.τ_involution` `TensorSpecies.contr_tmul_symm` `TensorSpecies.contr_congr`
`contrPCoeff_update_dropPairEmb` 📖	mathematical	`TensorSpecies.τ`	`contrPCoeff` `update` `dropPairEmb`	—	—
`contrPCoeff_update_fst_add` 📖	mathematical	`TensorSpecies.τ`	`contrPCoeff` `update` `TensorSpecies.FD`	—	—
`contrPCoeff_update_fst_smul` 📖	mathematical	`TensorSpecies.τ`	`contrPCoeff` `update` `TensorSpecies.FD`	—	—
`contrPCoeff_update_snd_add` 📖	mathematical	`TensorSpecies.τ`	`contrPCoeff` `update` `TensorSpecies.FD`	—	—
`contrPCoeff_update_snd_smul` 📖	mathematical	`TensorSpecies.τ`	`contrPCoeff` `update` `TensorSpecies.FD`	—	—
`contrP_equivariant` 📖	mathematical	`TensorSpecies.τ`	`contrP` `TensorSpecies.Tensor.Pure` `instSMul` `TensorSpecies.Tensor` `dropPairEmb` `TensorSpecies.Tensor.actionT`	—	`contrPCoeff_invariant` `dropPair_equivariant` `TensorSpecies.Tensor.actionT_smul` `TensorSpecies.Tensor.actionT_pure`
`contrP_symm` 📖	mathematical	`TensorSpecies.τ`	`contrP` `TensorSpecies.Tensor` `dropPairEmb` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensor.permT` `TensorSpecies.Tensor.PermCond` `permCond_dropPairEmb_symm` `TensorSpecies.τ_τ_apply`	—	`permCond_dropPairEmb_symm` `TensorSpecies.τ_τ_apply` `contrP.eq_1` `contrPCoeff_symm` `dropPair_symm` `TensorSpecies.Tensor.permT_pure`
`contrP_update_add` 📖	mathematical	`TensorSpecies.τ`	`contrP` `update` `TensorSpecies.FD` `TensorSpecies.Tensor` `dropPairEmb` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F`	—	`eq_or_exists_dropPairEmb` `contrPCoeff_update_fst_add` `dropPair_update_fst` `contrPCoeff_update_snd_add` `dropPair_update_snd` `contrPCoeff_update_dropPairEmb` `dropPair_update_dropPairEmb` `toTensor_update_add`
`contrP_update_smul` 📖	mathematical	`TensorSpecies.τ`	`contrP` `update` `TensorSpecies.FD` `TensorSpecies.Tensor` `dropPairEmb` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F`	—	`eq_or_exists_dropPairEmb` `contrPCoeff_update_fst_smul` `dropPair_update_fst` `contrPCoeff_update_snd_smul` `dropPair_update_snd` `contrPCoeff_update_dropPairEmb` `dropPair_update_dropPairEmb` `toTensor_update_smul`
`dropPairEmbPre_dropPairEmb` 📖	mathematical	—	`dropPairEmbPre` `dropPairEmb`	—	`dropPairEmb_injective` `dropPairEmb_dropPairEmbPre`
`dropPairEmbPre_eq_orderIsoOfFin` 📖	mathematical	—	`dropPairEmbPre`	—	`dropPairEmb_injective` `dropPairEmb_apply_eq_orderIsoOfFin` `dropPairEmb_dropPairEmbPre`
`dropPairEmbPre_injective` 📖	mathematical	—	`dropPairEmbPre`	—	`dropPairEmb_injective` `dropPairEmb_dropPairEmbPre`
`dropPairEmbPre_surjective` 📖	mathematical	—	`dropPairEmbPre`	—	`dropPairEmb_injective` `dropPairEmb_dropPairEmbPre`
`dropPairEmb_apply_eq_orderIsoOfFin` 📖	mathematical	—	`dropPairEmb`	—	`dropPairEmb_eq_orderEmbOfFin`
`dropPairEmb_comm` 📖	mathematical	—	`dropPairEmb` `dropPairEmbPre`	—	`dropPairEmb_injective` `dropPairEmb_range` `dropPairEmb_image_compl` `dropPairEmb_dropPairEmbPre`
`dropPairEmb_comm_apply` 📖	mathematical	—	`dropPairEmb` `dropPairEmbPre`	—	`dropPairEmb_comm`
`dropPairEmb_dropPairEmbPre` 📖	mathematical	—	`dropPairEmb` `dropPairEmbPre`	—	—
`dropPairEmb_eq_iff_eq` 📖	mathematical	—	`dropPairEmb`	—	`dropPairEmb_injective`
`dropPairEmb_eq_orderEmbOfFin` 📖	mathematical	—	`dropPairEmb`	—	`dropPairEmb_eq_succAbove_succAbove`
`dropPairEmb_eq_succAbove_succAbove` 📖	mathematical	—	`dropPairEmb`	—	—
`dropPairEmb_image_compl` 📖	mathematical	—	`dropPairEmb`	—	`dropPairEmb_injective` `dropPairEmb_range`
`dropPairEmb_injective` 📖	mathematical	—	`dropPairEmb`	—	`dropPairEmb_self_apply` `dropPairEmb_eq_succAbove_succAbove`
`dropPairEmb_leq_iff_leq` 📖	mathematical	—	`dropPairEmb`	—	`dropPairEmb_self_apply` `dropPairEmb_eq_succAbove_succAbove`
`dropPairEmb_lt_iff_lt` 📖	mathematical	—	`dropPairEmb`	—	`dropPairEmb_self_apply` `dropPairEmb_eq_succAbove_succAbove`
`dropPairEmb_monotone` 📖	mathematical	—	`dropPairEmb`	—	—
`dropPairEmb_neq_fst` 📖	mathematical	—	`dropPairEmb`	—	—
`dropPairEmb_neq_snd` 📖	mathematical	—	`dropPairEmb`	—	—
`dropPairEmb_range` 📖	mathematical	—	`dropPairEmb`	—	`dropPairEmb_eq_orderEmbOfFin`
`dropPairEmb_self_apply` 📖	mathematical	—	`dropPairEmb`	—	—
`dropPairEmb_succAbove` 📖	mathematical	—	`dropPairEmb`	—	`dropPairEmb_eq_succAbove_succAbove`
`dropPairEmb_symm` 📖	mathematical	—	`dropPairEmb`	—	`dropPairEmb_eq_orderEmbOfFin`
`dropPairOfMap_bijective` 📖	mathematical	—	`dropPairOfMap`	—	`dropPairOfMap_injective` `dropPairOfMap_surjective`
`dropPairOfMap_id` 📖	mathematical	—	`dropPairOfMap`	—	`dropPairEmbPre_dropPairEmb`
`dropPairOfMap_injective` 📖	mathematical	—	`dropPairOfMap`	—	—
`dropPairOfMap_surjective` 📖	mathematical	—	`dropPairOfMap`	—	`dropPairEmbPre_surjective` `eq_or_exists_dropPairEmb`
`dropPair_comm` 📖	mathematical	—	`dropPair` `dropPairEmb` `permP` `dropPairEmbPre` `permCond_dropPairEmb_comm`	—	`permCond_dropPairEmb_comm` `dropPairEmb_comm_apply` `congr_right`
`dropPair_equivariant` 📖	mathematical	—	`dropPair` `TensorSpecies.Tensor.Pure` `instSMul` `dropPairEmb`	—	—
`dropPair_permP` 📖	mathematical	`TensorSpecies.Tensor.PermCond`	`dropPair` `permP` `dropPairEmb` `dropPairOfMap` `permCond_dropPairOfMap`	—	`permCond_dropPairOfMap` `congr_mid` `dropPairEmb_dropPairEmbPre`
`dropPair_symm` 📖	mathematical	—	`dropPair` `permP` `dropPairEmb` `TensorSpecies.Tensor.PermCond` `permCond_dropPairEmb_symm`	—	`permCond_dropPairEmb_symm` `dropPairEmb_symm` `congr_right`
`dropPair_update_dropPairEmb` 📖	mathematical	—	`dropPair` `update` `dropPairEmb`	—	—
`dropPair_update_fst` 📖	mathematical	—	`dropPair` `update`	—	`fst_neq_dropPairEmb_pre`
`dropPair_update_snd` 📖	mathematical	—	`dropPair` `update`	—	`permCond_dropPairEmb_symm` `dropPair_symm` `dropPair_update_fst`
`eq_or_exists_dropPairEmb` 📖	mathematical	—	`dropPairEmb`	—	`permCond_dropPairEmb_symm` `dropPairEmb_eq_orderEmbOfFin`
`fst_neq_dropPairEmb_pre` 📖	mathematical	—	`dropPairEmb`	—	`dropPairEmb_self_apply` `dropPairEmb_eq_orderEmbOfFin`
`permCond_dropPairEmb_comm` 📖	mathematical	—	`dropPairEmb` `dropPairEmbPre`	—	`dropPairEmb_comm_apply`
`permCond_dropPairEmb_symm` 📖	mathematical	—	`dropPairEmb`	—	`dropPairEmb_symm`
`permCond_dropPairOfMap` 📖	mathematical	`TensorSpecies.Tensor.PermCond`	`dropPairEmb` `dropPairOfMap`	—	`dropPairOfMap_bijective` `dropPairEmb_dropPairEmbPre`
`snd_neq_dropPairEmb_pre` 📖	mathematical	—	`dropPairEmb`	—	`dropPairEmb_symm` `fst_neq_dropPairEmb_pre`

---

← Back to Index