Apply

📁 Source: PhysLean/Relativity/LorentzGroup/Boosts/Apply.lean

Statistics

Metric	Count
Definitions	0
Theorems boost_inr_other_eq, boost_inr_self_eq, boost_time_eq, boost_toCoord_eq	4
Total	4

Lorentz.Vector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boost_inr_other_eq 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up instAddCommMonoid instModuleReal tensorial LorentzGroup.boost	—	smul_eq_sum LorentzGroup.boost_inr_other_inl_0 LorentzGroup.boost_inr_other_inr
boost_inr_self_eq 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up instAddCommMonoid instModuleReal tensorial LorentzGroup.boost LorentzGroup.γ	—	smul_eq_sum LorentzGroup.boost_inr_self_inl_0 LorentzGroup.boost_inr_self_inr_other LorentzGroup.boost_inr_self_inr_self
boost_time_eq 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up instAddCommMonoid instModuleReal tensorial LorentzGroup.boost LorentzGroup.γ	—	smul_eq_sum LorentzGroup.boost_inl_0_inl_0 LorentzGroup.boost_inl_0_inr_other LorentzGroup.boost_inl_0_inr_self
boost_toCoord_eq 📖	mathematical	—	LorentzGroup Lorentz.Vector TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up instAddCommMonoid instModuleReal tensorial LorentzGroup.boost LorentzGroup.γ	—	boost_time_eq boost_inr_self_eq boost_inr_other_eq

---

← Back to Index