Basic

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

Statistics

Metric	Count
Definitions `boost`, `γ`	2
Theorems `h`, `boost_inl_0_inl_0`, `boost_inl_0_inr_other`, `boost_inl_0_inr_self`, `boost_inr_inr_other`, `boost_inr_other_inl_0`, `boost_inr_other_inr`, `boost_inr_other_inr_self`, `boost_inr_self_inl_0`, `boost_inr_self_inr_other`, `boost_inr_self_inr_self`, `boost_inverse`, `boost_transpose_eq_self`, `boost_transpose_matrix_eq_self`, `boost_zero_eq_id`, `boost_zero_inl_0_inr_nat_succ`, `boost_zero_inl_0_inr_succ`, `boost_zero_inr_0_inr_nat_succ`, `boost_zero_inr_0_inr_succ`, `boost_zero_inr_nat_succ_inl_0`, `boost_zero_inr_nat_succ_inr_0`, `boost_zero_inr_succ_inl_0`, `boost_zero_inr_succ_inr_0`, `boost_zero_inr_succ_inr_succ`, `γ_det_not_zero`, `γ_neg`, `γ_sq`, `γ_zero`	28
Total	30

LorentzGroup

Definitions

Name	Category	Theorems
`boost` 📖	CompOp	33 math math: `boost_inr_self_inl_0`, `boost_inl_0_inr_other`, `boost_zero_inr_0_inr_succ`, `boost_inr_other_inr`, `boost_zero_eq_id`, `boost_zero_inr_nat_succ_inl_0`, `boost_zero_inl_0_inr_succ`, `boost_inr_other_inl_0`, `boost_transpose_eq_self`, `Lorentz.Vector.boost_inr_other_eq`, `SpaceTime.boost_zero_apply_time_space`, `boost_inr_inr_other`, `Lorentz.Vector.boost_time_eq`, `boost_zero_inr_0_inr_nat_succ`, `boost_zero_inl_0_inr_nat_succ`, `boost_inr_other_inr_self`, `Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_succ_succ`, `boost_transpose_matrix_eq_self`, `boost_zero_inr_succ_inr_0`, `SpaceTime.boost_x_smul`, `boost_inr_self_inr_other`, `boost_zero_inr_succ_inl_0`, `Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_zero`, `boost_zero_inr_succ_inr_succ`, `boost_inverse`, `boost_inr_self_inr_self`, `Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_zero_succ`, `Lorentz.Vector.boost_inr_self_eq`, `boost_inl_0_inl_0`, `Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_succ`, `boost_inl_0_inr_self`, `boost_zero_inr_nat_succ_inr_0`, `Lorentz.Vector.boost_toCoord_eq`
`γ` 📖	CompOp	17 math math: `boost_inr_self_inl_0`, `SpaceTime.boost_zero_apply_time_space`, `boost.h`, `Lorentz.Vector.boost_time_eq`, `γ_neg`, `Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_succ_succ`, `SpaceTime.boost_x_smul`, `Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_zero`, `boost_inr_self_inr_self`, `Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_zero_succ`, `Lorentz.Vector.boost_inr_self_eq`, `boost_inl_0_inl_0`, `Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_succ`, `γ_zero`, `boost_inl_0_inr_self`, `γ_sq`, `Lorentz.Vector.boost_toCoord_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boost_inl_0_inl_0` 📖	mathematical	—	`LorentzGroup` `boost` `γ`	—	`boost.h`
`boost_inl_0_inr_other` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost.h`
`boost_inl_0_inr_self` 📖	mathematical	—	`LorentzGroup` `boost` `γ`	—	`boost.h`
`boost_inr_inr_other` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost_transpose_eq_self` `boost_inr_other_inr`
`boost_inr_other_inl_0` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost.h`
`boost_inr_other_inr` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost.h`
`boost_inr_other_inr_self` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost.h`
`boost_inr_self_inl_0` 📖	mathematical	—	`LorentzGroup` `boost` `γ`	—	`boost.h`
`boost_inr_self_inr_other` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost.h`
`boost_inr_self_inr_self` 📖	mathematical	—	`LorentzGroup` `boost` `γ`	—	`boost.h`
`boost_inverse` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `boost`	—	`dual_mem` `inv_eq_dual` `minkowskiMatrix.dual_apply` `minkowskiMatrix.inl_0_inl_0` `boost.h` `γ_neg` `minkowskiMatrix.inr_i_inr_i`
`boost_transpose_eq_self` 📖	mathematical	—	`transpose` `boost`	—	`boost.h`
`boost_transpose_matrix_eq_self` 📖	mathematical	—	`LorentzGroup` `boost`	—	`transpose_val` `boost_transpose_eq_self`
`boost_zero_eq_id` 📖	mathematical	—	`boost` `LorentzGroup` `lorentzGroupIsGroup`	—	`boost.h` `γ_zero`
`boost_zero_inl_0_inr_nat_succ` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost_inl_0_inr_other`
`boost_zero_inl_0_inr_succ` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost_inl_0_inr_other`
`boost_zero_inr_0_inr_nat_succ` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost_inr_self_inr_other`
`boost_zero_inr_0_inr_succ` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost_inr_self_inr_other`
`boost_zero_inr_nat_succ_inl_0` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost_inr_other_inl_0`
`boost_zero_inr_nat_succ_inr_0` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost_inr_other_inr_self`
`boost_zero_inr_succ_inl_0` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost_inr_other_inl_0`
`boost_zero_inr_succ_inr_0` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost_inr_other_inr_self`
`boost_zero_inr_succ_inr_succ` 📖	mathematical	—	`LorentzGroup` `boost`	—	`boost_inr_inr_other`
`γ_det_not_zero` 📖	—	—	—	—	—
`γ_neg` 📖	mathematical	—	`γ`	—	—
`γ_sq` 📖	mathematical	—	`γ`	—	—
`γ_zero` 📖	mathematical	—	`γ`	—	—

LorentzGroup.boost

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`h` 📖	mathematical	—	`LorentzGroup` `LorentzGroup.γ`	—	`LorentzGroup.mem_iff_dual_mul_self` `minkowskiMatrix.dual_apply` `minkowskiMatrix.inl_0_inl_0` `minkowskiMatrix.inr_i_inr_i`

---

← Back to Index