Dual

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

Statistics

Metric	Count
Definitions fromDualMap, toDual, toDualMap	3
Theorems fromDualMap_apply, fromDualMap_eq_permT_toDualMap, fromDualMap_toDualMap, toDualMap_apply, toDualMap_eq_permT_fromDualMap, toDualMap_fromDualMap, toDual_equivariant, repDim_τ	8
Total	11

TensorSpecies

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
repDim_τ 📖	mathematical	—	repDim τ	—	Tensor.finrank_tensor_eq

TensorSpecies.Tensor

Definitions

Name	Category	Theorems
fromDualMap 📖	CompOp	5 math math: fromDualMap_apply, toDualMap_eq_permT_fromDualMap, fromDualMap_eq_permT_toDualMap, toDualMap_fromDualMap, fromDualMap_toDualMap
toDual 📖	CompOp	1 math math: toDual_equivariant
toDualMap 📖	CompOp	5 math math: toDualMap_eq_permT_fromDualMap, fromDualMap_eq_permT_toDualMap, toDualMap_apply, toDualMap_fromDualMap, fromDualMap_toDualMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromDualMap_apply 📖	mathematical	—	TensorSpecies.Tensor TensorSpecies.τ IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromDualMap Pure.dropPairEmb permT PermCond contrT prodT TensorSpecies.metricTensor	—	—
fromDualMap_eq_permT_toDualMap 📖	mathematical	—	TensorSpecies.Tensor TensorSpecies.τ IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromDualMap permT PermCond TensorSpecies.τ_τ_apply toDualMap	—	TensorSpecies.τ_τ_apply fromDualMap_apply toDualMap_apply PermCond.comp permT_permT permT.congr_simp TensorSpecies.metricTensor_congr prodLeftMap_permCond prodT_permT_left Pure.permCond_dropPairOfMap contrT_permT permT_congr
fromDualMap_toDualMap 📖	mathematical	—	TensorSpecies.Tensor TensorSpecies.τ IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F fromDualMap toDualMap	—	TensorSpecies.τ_τ_apply fromDualMap_eq_permT_toDualMap toDualMap_eq_permT_fromDualMap PermCond.comp permT_congr toDualMap_fromDualMap permT_permT permT_id_self
toDualMap_apply 📖	mathematical	—	TensorSpecies.Tensor TensorSpecies.τ IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toDualMap Pure.dropPairEmb permT PermCond contrT TensorSpecies.τ_τ_apply prodT TensorSpecies.metricTensor	—	—
toDualMap_eq_permT_fromDualMap 📖	mathematical	—	TensorSpecies.Tensor TensorSpecies.τ IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toDualMap fromDualMap permT PermCond TensorSpecies.τ_τ_apply	—	TensorSpecies.τ_τ_apply fromDualMap_eq_permT_toDualMap toDualMap_apply prodRightMap_permCond Pure.permCond_dropPairOfMap prodLeftMap_permCond prodT_permT_right TensorSpecies.metricTensor_congr prodT_permT_left contrT_permT PermCond.comp permT_congr permT_permT permT.congr_simp
toDualMap_fromDualMap 📖	mathematical	—	TensorSpecies.Tensor TensorSpecies.τ IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toDualMap fromDualMap	—	TensorSpecies.τ_τ_apply toDualMap_apply fromDualMap_apply prodRightMap_permCond prodT_permT_right Pure.dropPairEmb_permCond_prod prodT_contrT_snd Pure.permCond_dropPairOfMap contrT_permT Pure.permCond_dropPairEmb_comm Pure.dropPairEmb_dropPairEmbPre contrT_comm PermCond.comp permT_permT prodAssocMap'_permCond prodSwapMap_permCond prodT_assoc' prodT_swap prodRightMap_id PermCond.on_id_symm contrT_congr contrT_prodT_snd TensorSpecies.contrT_dual_metricTensor_metricTensor permT.congr_simp TensorSpecies.contrT_unitTensor_dual_single permT_congr_eq_id Pure.dropPairOfMap_id Pure.dropPairOfMap.congr_simp
toDual_equivariant 📖	mathematical	—	TensorSpecies.Tensor TensorSpecies.τ IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toDual actionT	—	TensorSpecies.metricTensor_invariant prodT_equivariant contrT_equivariant permT_equivariant

---

← Back to Index