FromBoostRotation

📁 Source: PhysLean/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean

Statistics

Metric	Count
Definitions toBoostRotation, toRotation, toVelocity	3
Theorems toRotation_continuous, toVelocity_continuous	2
Total	5

LorentzGroup

Definitions

Name	Category	Theorems
toBoostRotation 📖	CompOp	—
toRotation 📖	CompOp	1 math math: toRotation_continuous
toVelocity 📖	CompOp	1 math math: toVelocity_continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toRotation_continuous 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup restricted Rotations instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup toRotation	—	instIsTopologicalGroupElemMatrixSumFinOfNatNatReal generalizedBoost_continuous_snd toVelocity_continuous
toVelocity_continuous 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup restricted Lorentz.Vector Lorentz.Velocity instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup Lorentz.Velocity.instTopologicalSpaceElemVector toVelocity	—	toVector_continuous

---

← Back to Index