Documentation Verification Report

Basic

📁 Source: PhysLean/Relativity/Tensors/RealTensor/Metrics/Basic.lean

Statistics

Metric	Count
Definitions `coMetric`, `contrMetric`, `termη`, `termη'`	4
Theorems `actionT_coMetric`, `actionT_contrMetric`, `coMetric_eq_fromConstPair`, `coMetric_eq_fromPairT`, `coMetric_repr_apply_eq_minkowskiMatrix`, `contrMetric_eq_fromConstPair`, `contrMetric_eq_fromPairT`, `contrMetric_repr_apply_eq_minkowskiMatrix`	8
Total	12

realLorentzTensor

Definitions

Name	Category	Theorems
`coMetric` 📖	CompOp	4 math math: `coMetric_eq_fromConstPair`, `actionT_coMetric`, `coMetric_repr_apply_eq_minkowskiMatrix`, `coMetric_eq_fromPairT`
`contrMetric` 📖	CompOp	8 math math: `contrMetric_repr_apply_eq_minkowskiMatrix`, `contrMetric_eq_fromPairT`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add`, `actionT_contrMetric`, `Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength`, `Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux`, `contrMetric_eq_fromConstPair`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add`
`termη` 📖	CompOp	—
`termη'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`actionT_coMetric` 📖	mathematical	—	`LorentzGroup` `TensorSpecies.Tensor` `Color` `lorentzGroupIsGroup` `realLorentzTensor` `Color.down` `TensorSpecies.Tensor.actionT` `coMetric`	—	`TensorSpecies.metricTensor_invariant`
`actionT_contrMetric` 📖	mathematical	—	`LorentzGroup` `TensorSpecies.Tensor` `Color` `lorentzGroupIsGroup` `realLorentzTensor` `Color.up` `TensorSpecies.Tensor.actionT` `contrMetric`	—	`TensorSpecies.metricTensor_invariant`
`coMetric_eq_fromConstPair` 📖	mathematical	—	`coMetric` `TensorSpecies.Tensor.fromConstPair` `Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `Color.down` `Lorentz.preCoMetric`	—	`coMetric.eq_1` `TensorSpecies.metricTensor.eq_1`
`coMetric_eq_fromPairT` 📖	mathematical	—	`coMetric` `LorentzGroup` `lorentzGroupIsGroup` `Color` `TensorSpecies.FD` `realLorentzTensor` `Color.down` `TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensor.fromPairT` `Lorentz.preCoMetricVal`	—	`coMetric_eq_fromConstPair` `TensorSpecies.Tensor.fromConstPair.eq_1` `Lorentz.preCoMetric_apply_one`
`coMetric_repr_apply_eq_minkowskiMatrix` 📖	mathematical	—	`TensorSpecies.Tensor.ComponentIdx` `Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `Color.down` `TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensor.basis` `coMetric` `minkowskiMatrix`	—	`coMetric_eq_fromPairT` `Lorentz.coCoToMatrixRe_symm_expand_tmul` `TensorSpecies.Tensor.fromPairT_basis_repr`
`contrMetric_eq_fromConstPair` 📖	mathematical	—	`contrMetric` `TensorSpecies.Tensor.fromConstPair` `Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `Color.up` `Lorentz.preContrMetric`	—	`contrMetric.eq_1` `TensorSpecies.metricTensor.eq_1`
`contrMetric_eq_fromPairT` 📖	mathematical	—	`contrMetric` `LorentzGroup` `lorentzGroupIsGroup` `Color` `TensorSpecies.FD` `realLorentzTensor` `Color.up` `TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensor.fromPairT` `Lorentz.preContrMetricVal`	—	`contrMetric_eq_fromConstPair` `TensorSpecies.Tensor.fromConstPair.eq_1` `Lorentz.preContrMetric_apply_one`
`contrMetric_repr_apply_eq_minkowskiMatrix` 📖	mathematical	—	`TensorSpecies.Tensor.ComponentIdx` `Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `Color.up` `TensorSpecies.Tensor` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `TensorSpecies.Tensor.basis` `contrMetric` `minkowskiMatrix`	—	`contrMetric_eq_fromPairT` `Lorentz.contrContrToMatrixRe_symm_expand_tmul` `TensorSpecies.Tensor.fromPairT_basis_repr`

---

← Back to Index