Basic

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

Statistics

Metric	Count
Definitions restricted	1
Theorems isOrthochronous_of_restricted, restricted_eq_identity_component_of_isConnected, restricted_normal_subgroup	3
Total	4

LorentzGroup

Definitions

Name	Category	Theorems
restricted 📖	CompOp	8 math math: lorentzAlgebra.exp_mem_restricted_lorentzGroup, restricted_normal_subgroup, isOrthochronous_of_restricted, toVelocity_continuous, toRotation_continuous, Lorentz.SL2C.toRestrictedLorentzGroup_apply_coe_coe, generalizedBoost_mem_restricted, rotations_subset_restricted

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOrthochronous_of_restricted 📖	mathematical	—	IsOrthochronous LorentzGroup lorentzGroupIsGroup restricted	—	—
restricted_eq_identity_component_of_isConnected 📖	—	LorentzGroup instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup lorentzGroupIsGroup restricted	—	—	isProper_on_connected_component isProper_id isOrthochronous_on_connected_component id_isOrthochronous
restricted_normal_subgroup 📖	mathematical	—	LorentzGroup lorentzGroupIsGroup restricted	—	coe_inv isOrthochronous_mul isOrthochronous_inv_iff isOrthochronous_mul_iff

---

← Back to Index