Documentation Verification Report

UnitTensor

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

Statistics

MetricCount
DefinitionsunitTensor
1
TheoremscontrT_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
Total9

TensorSpecies

Definitions

NameCategoryTheorems
unitTensor 📖CompOp
11 mathmath: 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

NameKindAssumesProvesValidatesDepends On
contrT_single_unitTensor 📖mathematicalTensor
τ
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 📖mathematicalTensor
τ
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 📖mathematicalunitTensor
τ
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 📖mathematicalunitTensor
Tensor
τ
IndexNotation.OverColor
IndexNotation.instGroupoidOverColor
F
Tensor.permT
Tensor.PermCond
Tensor.permT_id_self
unitTensor_eq_permT_dual 📖mathematicalunitTensor
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 📖mathematicalTensor
τ
Tensor.actionT
unitTensor
unitTensor.eq_1
Tensor.actionT_fromConstPair
unit_app_eq_dual_unit_app 📖mathematicalIndexNotation.OverColor.Discrete.τPair
FD
τ
unit
τ_τ_apply
τ_τ_apply
τ_involution
unit_symm
unit_fromSingleTContrFromPairT_eq_fromSingleT 📖mathematicalTensor.fromSingleTContrFromPairT
IndexNotation.OverColor.Discrete.τPair
FD
τ
unit
Tensor
IndexNotation.OverColor
IndexNotation.instGroupoidOverColor
F
Tensor.fromSingleT
contr_unit

---

← Back to Index