Products

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

Statistics

Metric	Count
Definitions	0
Theorems contrPCoeff_castAdd, contrPCoeff_natAdd, dropPairEmb_apply_lt_lt, dropPairEmb_comm_natAdd, dropPairEmb_natAdd_apply_castAdd, dropPairEmb_natAdd_image_range_castAdd, dropPairEmb_permCond_prod, prodP_contrP_snd, prodP_dropPair, contrT_prodT_snd, prodT_contrT_snd	11
Total	11

TensorSpecies.Tensor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contrT_prodT_snd 📖	mathematical	TensorSpecies.τ	TensorSpecies.Tensor Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F contrT prodT permT PermCond.on_id_symm Pure.dropPairEmb_permCond_prod	—	PermCond.on_id_symm Pure.dropPairEmb_permCond_prod prodT_contrT_snd PermCond.comp permT_permT permT_congr permT_id_self
prodT_contrT_snd 📖	mathematical	TensorSpecies.τ	TensorSpecies.Tensor Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F prodT contrT permT Pure.dropPairEmb_permCond_prod	—	Pure.dropPairEmb_permCond_prod induction_on_pure contrT_pure Pure.prodP_contrP_snd prodT_pure

TensorSpecies.Tensor.Pure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contrPCoeff_castAdd 📖	mathematical	TensorSpecies.τ	contrPCoeff prodP	—	prodP_apply_castAdd TensorSpecies.contr_congr map_map_apply
contrPCoeff_natAdd 📖	mathematical	TensorSpecies.τ	contrPCoeff prodP	—	prodP_apply_natAdd TensorSpecies.contr_congr map_map_apply
dropPairEmb_apply_lt_lt 📖	mathematical	—	dropPairEmb	—	dropPairEmb_succAbove
dropPairEmb_comm_natAdd 📖	mathematical	—	dropPairEmb	—	dropPairEmb_range dropPairEmb_image_compl dropPairEmb_natAdd_image_range_castAdd
dropPairEmb_natAdd_apply_castAdd 📖	mathematical	—	dropPairEmb	—	dropPairEmb_apply_lt_lt
dropPairEmb_natAdd_image_range_castAdd 📖	mathematical	—	dropPairEmb	—	dropPairEmb_natAdd_apply_castAdd
dropPairEmb_permCond_prod 📖	mathematical	TensorSpecies.τ	TensorSpecies.Tensor.PermCond dropPairEmb	—	dropPairEmb_natAdd_apply_castAdd dropPairEmb_comm_natAdd
prodP_contrP_snd 📖	mathematical	TensorSpecies.τ	TensorSpecies.Tensor dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.prodT toTensor contrP TensorSpecies.Tensor.permT dropPairEmb_permCond_prod prodP	—	dropPairEmb_permCond_prod contrPCoeff_natAdd TensorSpecies.Tensor.prodT_pure TensorSpecies.Tensor.permT_pure prodP_dropPair
prodP_dropPair 📖	mathematical	TensorSpecies.τ	prodP dropPairEmb dropPair permP dropPairEmb_permCond_prod	—	dropPairEmb_permCond_prod prodP_apply_finSumFinEquiv dropPairEmb_natAdd_apply_castAdd congr_right prodP_apply_castAdd map_map_apply dropPairEmb_comm_natAdd prodP_apply_natAdd

---

← Back to Index