Boosts

📁 Source: PhysLean/Electromagnetism/Kinematics/Boosts.lean

Statistics

Metric	Count
Definitions	0
Theorems electricField_apply_x_boost_succ, electricField_apply_x_boost_zero, magneticFieldMatrix_apply_x_boost_succ_succ, magneticFieldMatrix_apply_x_boost_zero_succ	4
Total	4

Electromagnetism.ElectromagneticPotential

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
electricField_apply_x_boost_succ 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	electricField LorentzGroup TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.tensorial LorentzGroup.boost LorentzGroup.γ Time.val SpeedOfLight.val Space.val magneticFieldMatrix	—	electricField_eq_fieldStrengthMatrix fieldStrengthMatrix_equivariant LorentzGroup.boost_zero_inr_succ_inl_0 LorentzGroup.boost_inl_0_inl_0 LorentzGroup.boost_zero_inr_succ_inr_0 LorentzGroup.boost_zero_inr_succ_inr_succ LorentzGroup.boost_inl_0_inr_self fieldStrengthMatrix_diag_eq_zero LorentzGroup.boost_zero_inl_0_inr_succ fieldStrengthMatrix_inl_inr_eq_electricField fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix SpaceTime.boost_zero_apply_time_space SpaceTime.time_toTimeAndSpace_symm SpaceTime.space_toTimeAndSpace_symm
electricField_apply_x_boost_zero 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	electricField LorentzGroup TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.tensorial LorentzGroup.boost LorentzGroup.γ Time.val SpeedOfLight.val Space.val	—	electricField_eq_fieldStrengthMatrix fieldStrengthMatrix_equivariant LorentzGroup.boost_inr_self_inl_0 LorentzGroup.boost_inl_0_inl_0 fieldStrengthMatrix_diag_eq_zero LorentzGroup.boost_inr_self_inr_self LorentzGroup.boost_zero_inr_0_inr_succ LorentzGroup.boost_inl_0_inr_self LorentzGroup.boost_zero_inl_0_inr_succ fieldStrengthMatrix_antisymm LorentzGroup.γ_sq SpaceTime.boost_zero_apply_time_space
magneticFieldMatrix_apply_x_boost_succ_succ 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	magneticFieldMatrix LorentzGroup TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.tensorial LorentzGroup.boost LorentzGroup.γ Time.val SpeedOfLight.val Space.val	—	magneticFieldMatrix_eq fieldStrengthMatrix_equivariant LorentzGroup.boost_zero_inr_succ_inl_0 LorentzGroup.boost_zero_inr_succ_inr_0 LorentzGroup.boost_zero_inr_succ_inr_succ SpaceTime.boost_zero_apply_time_space
magneticFieldMatrix_apply_x_boost_zero_succ 📖	mathematical	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector	magneticFieldMatrix LorentzGroup TensorSpecies.Tensorial.smulAction realLorentzTensor.Color lorentzGroupIsGroup realLorentzTensor realLorentzTensor.Color.up Lorentz.Vector.instAddCommMonoid Lorentz.Vector.tensorial LorentzGroup.boost LorentzGroup.γ Time.val SpeedOfLight.val Space.val electricField	—	magneticFieldMatrix_eq fieldStrengthMatrix_equivariant LorentzGroup.boost_zero_inr_succ_inl_0 LorentzGroup.boost_inr_self_inl_0 LorentzGroup.boost_zero_inr_succ_inr_0 LorentzGroup.boost_zero_inr_succ_inr_succ LorentzGroup.boost_inr_self_inr_self fieldStrengthMatrix_diag_eq_zero LorentzGroup.boost_zero_inr_0_inr_succ fieldStrengthMatrix_inl_inr_eq_electricField fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix SpaceTime.boost_zero_apply_time_space SpaceTime.time_toTimeAndSpace_symm SpaceTime.space_toTimeAndSpace_symm

---

← Back to Index