Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `lorentzAlgebra`	1
Theorems `diag_comp`, `mem_iff`, `mem_iff'`, `mem_of_transpose_eta_eq_eta_mul_self`, `space_comps`, `time_comps`, `transpose_eta`	7
Total	8

(root)

Definitions

Name	Category	Theorems
`lorentzAlgebra` 📖	CompOp	16 math math: `lorentzAlgebra.transpose_eq_neg_eta_conj`, `lorentzAlgebra.exp_isOrthochronous`, `lorentzAlgebra.exp_mem_restricted_lorentzGroup`, `lorentzAlgebra.mem_of_transpose_eta_eq_eta_mul_self`, `lorentzAlgebra.mem_iff'`, `lorentzAlgebra.diag_comp`, `lorentzAlgebra.exp_mem_lorentzGroup`, `lorentzAlgebra.exp_isProper`, `lorentzAlgebra.mem_iff`, `lorentzAlgebra.boostGenerator_mem`, `lorentzAlgebra.space_comps`, `lorentzAlgebra.exp_transpose_of_mem_algebra`, `lorentzAlgebra.rotationGenerator_mem`, `lorentzAlgebra.time_comps`, `lorentzAlgebra.transpose_eta`, `lorentzAlgebra.trace_of_mem_is_zero`

lorentzAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diag_comp` 📖	mathematical	—	`lorentzAlgebra`	—	`mem_iff`
`mem_iff` 📖	mathematical	—	`lorentzAlgebra` `minkowskiMatrix`	—	`transpose_eta` `mem_of_transpose_eta_eq_eta_mul_self`
`mem_iff'` 📖	mathematical	—	`lorentzAlgebra` `minkowskiMatrix`	—	`mem_iff` `minkowskiMatrix.sq`
`mem_of_transpose_eta_eq_eta_mul_self` 📖	mathematical	`minkowskiMatrix`	`lorentzAlgebra`	—	—
`space_comps` 📖	mathematical	—	`lorentzAlgebra`	—	`mem_iff`
`time_comps` 📖	mathematical	—	`lorentzAlgebra`	—	`mem_iff`
`transpose_eta` 📖	mathematical	—	`lorentzAlgebra` `minkowskiMatrix`	—	—

---

← Back to Index