Documentation Verification Report

ExponentialMap

📁 Source: PhysLean/Relativity/LorentzAlgebra/ExponentialMap.lean

Statistics

Metric	Count
Definitions `instUniformSpaceMatrix`	1
Theorems `exp_reindex`, `trace_reindex`, `exp_isOrthochronous`, `exp_isProper`, `exp_mem_lorentzGroup`, `exp_mem_restricted_lorentzGroup`, `exp_transpose_of_mem_algebra`, `trace_eq_sum_diagonal`, `trace_of_mem_is_zero`, `transpose_eq_neg_eta_conj`	10
Total	11

lorentzAlgebra

Definitions

Name	Category	Theorems
`instUniformSpaceMatrix` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exp_isOrthochronous` 📖	mathematical	—	`LorentzGroup.IsOrthochronous` `LorentzGroup` `lorentzAlgebra` `exp_mem_lorentzGroup`	—	`exp_mem_lorentzGroup` `LorentzGroup.isOrthochronous_on_connected_component` `LorentzGroup.id_isOrthochronous`
`exp_isProper` 📖	mathematical	—	`LorentzGroup.IsProper` `LorentzGroup` `lorentzAlgebra` `exp_mem_lorentzGroup`	—	`exp_mem_lorentzGroup` `Matrix.exp_reindex` `Matrix.trace_reindex` `trace_of_mem_is_zero` `Matrix.det_exp_real`
`exp_mem_lorentzGroup` 📖	mathematical	—	`LorentzGroup` `lorentzAlgebra`	—	`LorentzGroup.mem_iff_transpose_mul_minkowskiMatrix_mul_self` `exp_transpose_of_mem_algebra` `minkowskiMatrix.sq`
`exp_mem_restricted_lorentzGroup` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.restricted` `lorentzAlgebra` `exp_mem_lorentzGroup`	—	`exp_mem_lorentzGroup` `exp_isProper` `exp_isOrthochronous`
`exp_transpose_of_mem_algebra` 📖	mathematical	—	`lorentzAlgebra` `minkowskiMatrix`	—	`transpose_eq_neg_eta_conj` `minkowskiMatrix.sq`
`trace_eq_sum_diagonal` 📖	—	—	—	—	—
`trace_of_mem_is_zero` 📖	mathematical	—	`lorentzAlgebra`	—	`trace_eq_sum_diagonal` `diag_comp`
`transpose_eq_neg_eta_conj` 📖	mathematical	—	`lorentzAlgebra` `minkowskiMatrix`	—	`transpose_eta` `minkowskiMatrix.sq`

lorentzAlgebra.Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exp_reindex` 📖	—	—	—	—	—
`trace_reindex` 📖	—	—	—	—	—

---

← Back to Index