Boosts

📁 Source: PhysLean/SpaceAndTime/SpaceTime/Boosts.lean

Statistics

Metric	Count
Definitions	0
Theorems boost_x_smul, boost_zero_apply_time_space	2
Total	2

SpaceTime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boost_x_smul 📖	mathematical	—	LorentzGroup SpaceTime TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.tensorial LorentzGroup.boost LorentzGroup.γ	—	Lorentz.Vector.smul_eq_sum LorentzGroup.boost_inl_0_inl_0 LorentzGroup.boost_inl_0_inr_self LorentzGroup.boost_inl_0_inr_other LorentzGroup.boost_inr_self_inl_0 LorentzGroup.boost_inr_self_inr_self LorentzGroup.boost_inr_inr_other LorentzGroup.boost_inr_other_inl_0 LorentzGroup.boost_inr_other_inr
boost_zero_apply_time_space 📖	mathematical	—	LorentzGroup SpaceTime TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.tensorial LorentzGroup.boost Time Space Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Time.instNormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.isNormedAddCommGroup Time.instModuleReal Space.instModuleReal toTimeAndSpace LorentzGroup.γ Time.val SpeedOfLight.val Space.val	—	LorentzGroup.boost_inverse Lorentz.Vector.smul_eq_sum toTimeAndSpace_symm_apply_inl toTimeAndSpace_symm_apply_inr LorentzGroup.boost_inl_0_inl_0 LorentzGroup.γ_neg LorentzGroup.boost_inl_0_inr_self LorentzGroup.boost_zero_inl_0_inr_succ LorentzGroup.boost_inr_self_inl_0 LorentzGroup.boost_inr_self_inr_self LorentzGroup.boost_zero_inr_0_inr_succ LorentzGroup.boost_zero_inr_nat_succ_inl_0 LorentzGroup.boost_zero_inr_nat_succ_inr_0 LorentzGroup.boost_inr_inr_other

---

← Back to Index