Documentation Verification Report

Defs

📁 Source: PhysLean/Mathematics/Geometry/Metric/Riemannian/Defs.lean

Statistics

Metric	Count
Definitions `RiemannianMetric`, `metricInnerProductSpace`, `metricInnerProductSpace'`, `metricNormedAddCommGroup`, `curveLength`, `instCoeSomeENat`, `norm`, `norm'`, `tangentInnerCore`, `toPseudoRiemannianMetric`	10
Theorems `ext`, `ext_iff`, `norm_eq_norm_of_metricNormedAddCommGroup`, `pos_def`, `pos_def'`, `riemannian_metric_negDim_zero`, `toQuadraticForm_posDef`	7
Total	17

PseudoRiemannianMetric

Definitions

Name	Category	Theorems
`RiemannianMetric` 📖	CompData	—

PseudoRiemannianMetric.RiemannianMetric

Definitions

Name	Category	Theorems
`curveLength` 📖	CompOp	—
`instCoeSomeENat` 📖	CompOp	—
`norm` 📖	CompOp	1 math math: `norm_eq_norm_of_metricNormedAddCommGroup`
`norm'` 📖	CompOp	—
`tangentInnerCore` 📖	CompOp	—
`toPseudoRiemannianMetric` 📖	CompOp	5 math math: `riemannian_metric_negDim_zero`, `pos_def'`, `ext_iff`, `pos_def`, `toQuadraticForm_posDef`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`PseudoRiemannianMetric.val` `toPseudoRiemannianMetric`	—	—	—
`ext_iff` 📖	mathematical	—	`PseudoRiemannianMetric.val` `toPseudoRiemannianMetric`	—	`ext`
`norm_eq_norm_of_metricNormedAddCommGroup` 📖	mathematical	—	`norm` `TangentSpace.metricNormedAddCommGroup`	—	—
`pos_def` 📖	mathematical	—	`PseudoRiemannianMetric.val` `toPseudoRiemannianMetric`	—	`pos_def'`
`pos_def'` 📖	mathematical	—	`PseudoRiemannianMetric.val` `toPseudoRiemannianMetric`	—	—
`riemannian_metric_negDim_zero` 📖	mathematical	—	`QuadraticForm.negDim` `PseudoRiemannianMetric.toQuadraticForm` `toPseudoRiemannianMetric`	—	`QuadraticForm.rankNeg_eq_zero` `toQuadraticForm_posDef`
`toQuadraticForm_posDef` 📖	mathematical	—	`PseudoRiemannianMetric.toQuadraticForm` `toPseudoRiemannianMetric`	—	`pos_def`

PseudoRiemannianMetric.RiemannianMetric.TangentSpace

Definitions

Name	Category	Theorems
`metricInnerProductSpace` 📖	CompOp	—
`metricInnerProductSpace'` 📖	CompOp	—
`metricNormedAddCommGroup` 📖	CompOp	1 math math: `PseudoRiemannianMetric.RiemannianMetric.norm_eq_norm_of_metricNormedAddCommGroup`

---

← Back to Index