UnitTensor

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

Statistics

Metric	Count
Definitions unitTensor	1
Theorems contrT_single_unitTensor, contrT_unitTensor_dual_single, dual_unitTensor_eq_permT_unitTensor, unitTensor_congr, unitTensor_eq_permT_dual, unitTensor_invariant, unit_app_eq_dual_unit_app, unit_fromSingleTContrFromPairT_eq_fromSingleT	8
Total	9

TensorSpecies

Definitions

Name	Category	Theorems
unitTensor 📖	CompOp	11 math math: dual_unitTensor_eq_permT_unitTensor, contrT_unitTensor_dual_single, unitTensor_invariant, contrT_metricTensor_metricTensor, permT_fromPairTContr_metric_metric, fromPairTContr_metric_metric_eq_permT_unit, unitTensor_congr, unitTensor_eq_permT_dual, contrT_single_unitTensor, contrT_dual_metricTensor_metricTensor, contrT_metricTensor_metricTensor_eq_dual_unit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contrT_single_unitTensor 📖	mathematical	—	Tensor τ Tensor.Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor F Tensor.contrT Tensor.prodT unitTensor Tensor.permT Tensor.PermCond	—	unitTensor.eq_1 Tensor.fromConstPair.eq_1 Tensor.contrT_fromSingleT_fromPairT unit_fromSingleTContrFromPairT_eq_fromSingleT
contrT_unitTensor_dual_single 📖	mathematical	—	Tensor τ Tensor.Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor F Tensor.contrT Tensor.prodT unitTensor Tensor.permT Tensor.PermCond	—	τ_τ_apply unitTensor_eq_permT_dual Tensor.prodLeftMap_permCond Tensor.prodT_permT_left Tensor.Pure.permCond_dropPairOfMap Tensor.contrT_permT Tensor.prodSwapMap_permCond Tensor.prodT_swap Tensor.PermCond.comp Tensor.permT_permT Tensor.Pure.permCond_dropPairEmb_symm Tensor.contrT_symm contrT_single_unitTensor Tensor.permT_congr
dual_unitTensor_eq_permT_unitTensor 📖	mathematical	—	unitTensor τ Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor F Tensor.permT τ_τ_apply	—	τ_τ_apply unitTensor_eq_permT_dual unitTensor_congr Tensor.PermCond.comp Tensor.permT_permT Tensor.permT.congr_simp
unitTensor_congr 📖	mathematical	—	unitTensor Tensor τ IndexNotation.OverColor IndexNotation.instGroupoidOverColor F Tensor.permT Tensor.PermCond	—	Tensor.permT_id_self
unitTensor_eq_permT_dual 📖	mathematical	—	unitTensor Tensor τ IndexNotation.OverColor IndexNotation.instGroupoidOverColor F Tensor.permT τ_τ_apply	—	τ_τ_apply unitTensor.eq_1 unit_app_eq_dual_unit_app Tensor.fromConstPair_whiskerLeft Tensor.fromConstPair_braid Tensor.PermCond.comp Tensor.permT_permT Tensor.permT.congr_simp
unitTensor_invariant 📖	mathematical	—	Tensor τ Tensor.actionT unitTensor	—	unitTensor.eq_1 Tensor.actionT_fromConstPair
unit_app_eq_dual_unit_app 📖	mathematical	—	IndexNotation.OverColor.Discrete.τPair FD τ unit τ_τ_apply	—	τ_τ_apply τ_involution unit_symm
unit_fromSingleTContrFromPairT_eq_fromSingleT 📖	mathematical	—	Tensor.fromSingleTContrFromPairT IndexNotation.OverColor.Discrete.τPair FD τ unit Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor F Tensor.fromSingleT	—	contr_unit

---

← Back to Index