Basis

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

Statistics

Metric	Count
Definitions boostGenerator, rotationGenerator	2
Theorems boostGenerator_mem, rotationGenerator_mem	2
Total	4

lorentzAlgebra

Definitions

Name	Category	Theorems
boostGenerator 📖	CompOp	1 math math: boostGenerator_mem
rotationGenerator 📖	CompOp	1 math math: rotationGenerator_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boostGenerator_mem 📖	mathematical	—	lorentzAlgebra boostGenerator	—	mem_iff minkowskiMatrix.as_diagonal
rotationGenerator_mem 📖	mathematical	—	lorentzAlgebra rotationGenerator	—	mem_iff minkowskiMatrix.as_diagonal

---

← Back to Index