MetricTensor

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

Statistics

Metric	Count
Definitions metricTensor	1
Theorems contrT_dual_metricTensor_metricTensor, contrT_metricTensor_metricTensor, contrT_metricTensor_metricTensor_eq_dual_unit, fromPairTContr_metric_metric_eq_permT_unit, metricTensor_congr, metricTensor_invariant, permT_fromPairTContr_metric_metric	7
Total	8

TensorSpecies

Definitions

Name	Category	Theorems
metricTensor 📖	CompOp	7 math math: metricTensor_congr, contrT_metricTensor_metricTensor, Tensor.fromDualMap_apply, metricTensor_invariant, Tensor.toDualMap_apply, contrT_dual_metricTensor_metricTensor, contrT_metricTensor_metricTensor_eq_dual_unit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contrT_dual_metricTensor_metricTensor 📖	mathematical	—	Tensor τ Tensor.Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor F Tensor.contrT τ_τ_apply Tensor.prodT metricTensor Tensor.permT Tensor.PermCond unitTensor	—	τ_τ_apply metricTensor_congr Tensor.prodRightMap_permCond Tensor.prodT_permT_right Tensor.Pure.permCond_dropPairOfMap Tensor.contrT_permT contrT_metricTensor_metricTensor unitTensor_eq_permT_dual Tensor.PermCond.comp Tensor.permT_permT Tensor.permT.congr_simp Tensor.permT_congr
contrT_metricTensor_metricTensor 📖	mathematical	—	Tensor τ Tensor.Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor F Tensor.contrT Tensor.prodT metricTensor Tensor.permT unitTensor	—	metricTensor.eq_1 Tensor.fromConstPair.eq_1 Tensor.fromPairT_contr_fromPairT_eq_fromPairTContr fromPairTContr_metric_metric_eq_permT_unit Tensor.PermCond.comp Tensor.permT_permT
contrT_metricTensor_metricTensor_eq_dual_unit 📖	mathematical	—	Tensor τ Tensor.Pure.dropPairEmb IndexNotation.OverColor IndexNotation.instGroupoidOverColor F Tensor.contrT Tensor.prodT metricTensor Tensor.permT τ_τ_apply unitTensor	—	τ_τ_apply contrT_metricTensor_metricTensor unitTensor_eq_permT_dual Tensor.PermCond.comp Tensor.permT_permT Tensor.permT_congr
fromPairTContr_metric_metric_eq_permT_unit 📖	mathematical	—	Tensor.fromPairTContr τ IndexNotation.OverColor.Discrete.pair FD metric Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor F Tensor.permT unitTensor	—	permT_fromPairTContr_metric_metric Tensor.PermCond.comp Tensor.permT_permT Tensor.permT_congr_eq_id
metricTensor_congr 📖	mathematical	—	metricTensor Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor F Tensor.permT Tensor.PermCond	—	Tensor.permT_id_self
metricTensor_invariant 📖	mathematical	—	Tensor Tensor.actionT metricTensor	—	metricTensor.eq_1 Tensor.actionT_fromConstPair
permT_fromPairTContr_metric_metric 📖	mathematical	—	Tensor τ IndexNotation.OverColor IndexNotation.instGroupoidOverColor F Tensor.permT Tensor.fromPairTContr IndexNotation.OverColor.Discrete.pair FD metric unitTensor	—	Tensor.fromPairTContr.eq_1 Tensor.fromPairT_comm contr_metric

---

← Back to Index