Product

📁 Source: PhysLean/Relativity/Tensors/Product.lean

Statistics

Metric	Count
Definitions prod, prodEquiv, prodIndexEquiv, prodIndexEquiv, prodP, prodAssocMap, prodAssocMap', prodIndexEquiv, prodLeftMap, prodRightMap, prodSwapMap, prodT, tensorEquivProd	13
Theorems prod_apply_finSumFinEquiv, prodP_apply_castAdd, prodP_apply_finSumFinEquiv, prodP_apply_natAdd, prodP_assoc, prodP_assoc', prodP_basisVector, prodP_component, prodP_equivariant, prodP_permP_left, prodP_permP_right, prodP_swap, prodP_zero_right, prodP_zero_right_permCond, basis_prod_eq, prodAssocMap'_castAdd, prodAssocMap'_natAdd_castAdd, prodAssocMap'_natAdd_natAdd, prodAssocMap'_permCond, prodAssocMap_castAdd_castAdd, prodAssocMap_castAdd_natAdd, prodAssocMap_natAdd, prodAssocMap_permCond, prodIndexEquiv_symm_pure, prodLeftMap_id, prodLeftMap_permCond, prodRightMap_id, prodRightMap_permCond, prodSwapMap_permCond, prodT_assoc, prodT_assoc', prodT_basis, prodT_basis_repr_apply, prodT_default_right, prodT_equivariant, prodT_permT_left, prodT_permT_right, prodT_pure, prodT_swap	39
Total	52

TensorSpecies.Tensor

Definitions

Name	Category	Theorems
prodAssocMap 📖	CompOp	6 math math: Pure.prodP_assoc, prodAssocMap_castAdd_natAdd, prodT_assoc, prodAssocMap_permCond, prodAssocMap_natAdd, prodAssocMap_castAdd_castAdd
prodAssocMap' 📖	CompOp	6 math math: prodT_assoc', prodAssocMap'_permCond, prodAssocMap'_natAdd_natAdd, Pure.prodP_assoc', prodAssocMap'_natAdd_castAdd, prodAssocMap'_castAdd
prodIndexEquiv 📖	CompOp	1 math math: prodIndexEquiv_symm_pure
prodLeftMap 📖	CompOp	4 math math: Pure.prodP_permP_left, prodLeftMap_permCond, prodLeftMap_id, prodT_permT_left
prodRightMap 📖	CompOp	4 math math: prodRightMap_id, Pure.prodP_permP_right, prodT_permT_right, prodRightMap_permCond
prodSwapMap 📖	CompOp	3 math math: Pure.prodP_swap, prodSwapMap_permCond, prodT_swap
prodT 📖	CompOp	46 math math: realLorentzTensor.prodT_toComplex, complexLorentzTensor.contrMetric_contr_coMetric, prodT_basis_repr_apply, PauliMatrix.pauliCo_contr_pauliContr, contrT_fromSingleT_fromPairT, TensorSpecies.contrT_unitTensor_dual_single, complexLorentzTensor.altLeftMetric_contr_leftMetric, complexLorentzTensor.leftMetric_contr_altLeftMetric, PauliMatrix.pauliCoDown_trace_pauliCo, TensorSpecies.contrT_metricTensor_metricTensor, fromDualMap_apply, prodT_assoc', complexLorentzTensor.coMetric_contr_contrMetric, contrT_prodT_snd, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, fromTripleT_tmul, Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength, toDualMap_apply, contrT_fromSingleT_fromSingleT, TensorSpecies.contrT_single_unitTensor, complexLorentzTensor.altRightMetric_contr_rightMetric, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, fromPairT_contr_fromPairT_eq_fromPairTContr, Pure.prodP_contrP_snd, prodT_contrT_snd, fromPairT_contr_fromPairT_eq_fromPairTContr_tmul, PauliMatrix.auliContrDown_pauliContr_mul_add, TensorSpecies.contrT_dual_metricTensor_metricTensor, TensorSpecies.contrT_metricTensor_metricTensor_eq_dual_unit, prodT_swap, Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add, TensorSpecies.Tensorial.toTensor_tprod, prodT_permT_right, prodT_assoc, complexLorentzTensor.prodT_ofRat_ofRat, prodT_pure, PauliMatrix.pauliContr_mul_pauliContrDown_add, prodT_permT_left, complexLorentzTensor.rightMetric_contr_altRightMetric, prodT_equivariant, complexLorentzTensor.antiSymm_contr_symm, prodT_default_right, fromPairT_tmul, prodT_basis, PauliMatrix.pauliCo_trace_pauliCoDown, fromSingleT_contr_fromPairT_tmul
tensorEquivProd 📖	CompOp	1 math math: basis_prod_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_prod_eq 📖	mathematical	—	basis ComponentIdx TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F ComponentIdx.prodEquiv tensorEquivProd	—	prodT_basis basis_apply ComponentIdx.prod_apply_finSumFinEquiv
prodAssocMap'_castAdd 📖	mathematical	—	prodAssocMap'	—	—
prodAssocMap'_natAdd_castAdd 📖	mathematical	—	prodAssocMap'	—	—
prodAssocMap'_natAdd_natAdd 📖	mathematical	—	prodAssocMap'	—	—
prodAssocMap'_permCond 📖	mathematical	—	PermCond prodAssocMap'	—	prodAssocMap'_castAdd prodAssocMap'_natAdd_castAdd prodAssocMap'_natAdd_natAdd
prodAssocMap_castAdd_castAdd 📖	mathematical	—	prodAssocMap	—	—
prodAssocMap_castAdd_natAdd 📖	mathematical	—	prodAssocMap	—	—
prodAssocMap_natAdd 📖	mathematical	—	prodAssocMap	—	—
prodAssocMap_permCond 📖	mathematical	—	PermCond prodAssocMap	—	prodAssocMap_castAdd_castAdd prodAssocMap_castAdd_natAdd prodAssocMap_natAdd
prodIndexEquiv_symm_pure 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F prodIndexEquiv Pure.toTensor TensorSpecies.FD Pure Pure.prodIndexEquiv	—	prodIndexEquiv.eq_1 Pure.toTensor.eq_1 IndexNotation.OverColor.Hom.toEquiv_comp_inv_apply IndexNotation.OverColor.lift.map_tprod
prodLeftMap_id 📖	mathematical	—	prodLeftMap	—	—
prodLeftMap_permCond 📖	mathematical	PermCond	prodLeftMap	—	prodLeftMap.eq_1
prodRightMap_id 📖	mathematical	—	prodRightMap	—	—
prodRightMap_permCond 📖	mathematical	PermCond	prodRightMap	—	prodRightMap.eq_1
prodSwapMap_permCond 📖	mathematical	—	PermCond prodSwapMap	—	—
prodT_assoc 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F prodT permT prodAssocMap prodAssocMap_permCond	—	prodAssocMap_permCond induction_on_pure prodT_pure permT_pure Pure.prodP_assoc permT_congr
prodT_assoc' 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F prodT permT prodAssocMap' prodAssocMap'_permCond	—	prodAssocMap'_permCond induction_on_pure prodT_pure permT_pure Pure.prodP_assoc' permT_congr
prodT_basis 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F prodT ComponentIdx basis Pure.toTensor Pure.basisVector ComponentIdx.prod	—	basis_apply prodT_pure Pure.prodP_basisVector
prodT_basis_repr_apply 📖	mathematical	—	ComponentIdx TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F basis prodT ComponentIdx.prodEquiv	—	induction_on_pure prodT_pure basis_repr_pure Pure.prodP_component
prodT_default_right 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F prodT Pure.toTensor Pure TensorSpecies.FD permT Pure.prodP_zero_right_permCond	—	Pure.prodP_zero_right_permCond induction_on_pure prodT_pure Pure.prodP_zero_right permT_pure
prodT_equivariant 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F prodT actionT	—	induction_on_pure prodT_pure actionT_pure Pure.prodP_equivariant actionT_smul actionT_add
prodT_permT_left 📖	mathematical	PermCond	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F prodT permT prodLeftMap prodLeftMap_permCond	—	prodLeftMap_permCond induction_on_pure prodT_pure permT_pure Pure.prodP_permP_left
prodT_permT_right 📖	mathematical	PermCond	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F prodT permT prodRightMap prodRightMap_permCond	—	prodRightMap_permCond prodSwapMap_permCond prodT_swap PermCond.comp prodLeftMap_permCond permT_congr prodT_permT_left permT_permT
prodT_pure 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F prodT Pure.toTensor Pure.prodP	—	Pure.μ_toTensor_tmul_toTensor prodIndexEquiv_symm_pure
prodT_swap 📖	mathematical	—	TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F prodT permT prodSwapMap prodSwapMap_permCond	—	prodSwapMap_permCond induction_on_pure prodT_pure permT_pure Pure.prodP_swap

TensorSpecies.Tensor.ComponentIdx

Definitions

Name	Category	Theorems
prod 📖	CompOp	3 math math: prod_apply_finSumFinEquiv, TensorSpecies.Tensor.Pure.prodP_basisVector, TensorSpecies.Tensor.prodT_basis
prodEquiv 📖	CompOp	8 math math: TensorSpecies.Tensorial.basis_map_prod, TensorSpecies.Tensor.prodT_basis_repr_apply, SpaceTime.distTensorDeriv_toTensor_basis_repr, SpaceTime.tensorDeriv_toTensor_basis_repr, TensorSpecies.Tensor.Pure.prodP_component, realLorentzTensor.derivative_repr, complexLorentzTensor.prodT_ofRat_ofRat, TensorSpecies.Tensor.basis_prod_eq
prodIndexEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_apply_finSumFinEquiv 📖	mathematical	—	prod TensorSpecies.repDim	—	prod.eq_1 prodIndexEquiv.eq_1

TensorSpecies.Tensor.Pure

Definitions

Name	Category	Theorems
prodIndexEquiv 📖	CompOp	1 math math: TensorSpecies.Tensor.prodIndexEquiv_symm_pure
prodP 📖	CompOp	17 math math: prodP_assoc, prodP_component, prodP_basisVector, prodP_apply_natAdd, prodP_permP_left, prodP_assoc', prodP_zero_right, contrPCoeff_castAdd, prodP_equivariant, prodP_swap, prodP_permP_right, prodP_apply_finSumFinEquiv, prodP_contrP_snd, prodP_apply_castAdd, TensorSpecies.Tensor.prodT_pure, contrPCoeff_natAdd, prodP_dropPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prodP_apply_castAdd 📖	mathematical	—	prodP TensorSpecies.FD	—	prodP_apply_finSumFinEquiv
prodP_apply_finSumFinEquiv 📖	mathematical	—	prodP TensorSpecies.FD	—	prodP.eq_1 prodIndexEquiv.eq_1
prodP_apply_natAdd 📖	mathematical	—	prodP TensorSpecies.FD	—	prodP_apply_finSumFinEquiv
prodP_assoc 📖	mathematical	—	prodP permP TensorSpecies.Tensor.prodAssocMap TensorSpecies.Tensor.prodAssocMap_permCond	—	TensorSpecies.Tensor.prodAssocMap_permCond prodP_apply_castAdd TensorSpecies.Tensor.prodAssocMap_castAdd_castAdd congr_right map_map_apply prodP_apply_natAdd TensorSpecies.Tensor.prodAssocMap_castAdd_natAdd TensorSpecies.Tensor.prodAssocMap_natAdd
prodP_assoc' 📖	mathematical	—	prodP permP TensorSpecies.Tensor.prodAssocMap' TensorSpecies.Tensor.prodAssocMap'_permCond	—	TensorSpecies.Tensor.prodAssocMap'_permCond prodP_apply_castAdd TensorSpecies.Tensor.prodAssocMap'_castAdd congr_right map_map_apply prodP_apply_natAdd TensorSpecies.Tensor.prodAssocMap'_natAdd_castAdd TensorSpecies.Tensor.prodAssocMap'_natAdd_natAdd
prodP_basisVector 📖	mathematical	—	prodP basisVector TensorSpecies.Tensor.ComponentIdx.prod	—	prodP_apply_finSumFinEquiv TensorSpecies.Tensor.ComponentIdx.prod_apply_finSumFinEquiv
prodP_component 📖	mathematical	—	component prodP TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.ComponentIdx.prodEquiv	—	prodP_apply_finSumFinEquiv TensorSpecies.basis_congr_repr
prodP_equivariant 📖	mathematical	—	prodP TensorSpecies.Tensor.Pure instSMul	—	actionP_eq prodP_apply_castAdd prodP_apply_natAdd
prodP_permP_left 📖	mathematical	TensorSpecies.Tensor.PermCond	prodP permP TensorSpecies.Tensor.prodLeftMap TensorSpecies.Tensor.prodLeftMap_permCond	—	TensorSpecies.Tensor.prodLeftMap_permCond congr_right prodP_apply_castAdd map_map_apply prodP_apply_natAdd
prodP_permP_right 📖	mathematical	TensorSpecies.Tensor.PermCond	prodP permP TensorSpecies.Tensor.prodRightMap TensorSpecies.Tensor.prodRightMap_permCond	—	TensorSpecies.Tensor.prodRightMap_permCond TensorSpecies.Tensor.prodSwapMap_permCond prodP_swap TensorSpecies.Tensor.PermCond.comp TensorSpecies.Tensor.prodLeftMap_permCond permP_congr prodP_permP_left permP_permP
prodP_swap 📖	mathematical	—	prodP permP TensorSpecies.Tensor.prodSwapMap TensorSpecies.Tensor.prodSwapMap_permCond	—	TensorSpecies.Tensor.prodSwapMap_permCond prodP_apply_castAdd congr_right prodP_apply_natAdd map_map_apply
prodP_zero_right 📖	mathematical	—	prodP permP prodP_zero_right_permCond	—	prodP_zero_right_permCond prodP_apply_finSumFinEquiv
prodP_zero_right_permCond 📖	mathematical	—	TensorSpecies.Tensor.PermCond	—	—

---

← Back to Index