Velocity

📁 Source: PhysLean/Units/WithDim/Velocity.lean

Statistics

Metric	Count
Definitions Velocity	1
Theorems	0
Total	1

Lorentz

Definitions

Name	Category	Theorems
Velocity 📖	CompOp	33 math math: LorentzGroup.genBoostAux₁_basis_genBoostAux₂_minkowskiProduct, Velocity.mem_iff, Velocity.norm_spatialPart_le_timeComponent, Velocity.minkowskiProduct_continuous_fst, Velocity.minkowskiProduct_self_eq_one, Velocity.norm_spatialPart_sq_eq, Velocity.ext_iff, LorentzGroup.generalizedBoost_apply_expand, LorentzGroup.generalizedBoost_timeComponent_eq, LorentzGroup.genBoostAux₁_toMatrix_apply, LorentzGroup.toVelocity_continuous, LorentzGroup.genearlizedBoost_apply_basis, LorentzGroup.genBoostAux₁_add_genBoostAux₂_minkowskiProduct, Velocity.timeComponent_pos, Velocity.minkowskiProduct_continuous_snd, Velocity.zero_timeComponent, Velocity.timeComponent_nonneg, LorentzGroup.generalizedBoost_continuous_snd, Velocity.isPathConnected, LorentzGroup.generalizedBoost_apply_eq_minkowskiProduct, LorentzGroup.generalizedBoost_continuous_fst, LorentzGroup.generalizedBoost_apply_snd, LorentzGroup.generalizedBoost_apply_mul_one_plus_contr, LorentzGroup.genBoostAux₂_toMatrix_apply, LorentzGroup.genBoostAux₁_basis_minkowskiProduct, LorentzGroup.generalizedBoost_apply_eq_toCoord, LorentzGroup.genBoostAux₂_basis_minkowskiProduct, LorentzGroup.genBoostAux₂_apply_basis, LorentzGroup.genBoostAux₁_apply_basis, Velocity.zero_le_minkowskiProduct, LorentzGroup.basis_minkowskiProduct_genBoostAux₁_add_genBoostAux₂, LorentzGroup.generalizedBoost_apply_fst, Velocity.timeComponent_abs

---

← Back to Index