Documentation Verification Report

ToVector

📁 Source: PhysLean/Relativity/LorentzGroup/ToVector.lean

Statistics

Metric	Count
Definitions `toVector`	1
Theorems `one_le_abs_timeComponent`, `smul_timeComponent_eq_toVector_minkowskiProduct`, `toVector_apply`, `toVector_continuous`, `toVector_eq_basis_iff_timeComponent_eq_one`, `toVector_eq_fun`, `toVector_minkowskiProduct_self`, `toVector_mul`, `toVector_neg`, `toVector_timeComponent`	10
Total	11

LorentzGroup

Definitions

Name	Category	Theorems
`toVector` 📖	CompOp	12 math math: `toVector_continuous`, `not_isOrthochronous_iff_toVector_timeComponet_nonpos`, `toVector_eq_fun`, `toVector_apply`, `toVector_neg`, `toVector_minkowskiProduct_self`, `toVector_timeComponent`, `smul_timeComponent_eq_toVector_minkowskiProduct`, `toVector_eq_basis_iff_timeComponent_eq_one`, `toVector_mul`, `toVector_rotation`, `isOrthochronous_iff_toVector_timeComponet_nonneg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_le_abs_timeComponent` 📖	mathematical	—	`LorentzGroup`	—	`toVector_timeComponent` `toVector_minkowskiProduct_self` `Lorentz.Vector.minkowskiProduct_self_le_timeComponent_sq`
`smul_timeComponent_eq_toVector_minkowskiProduct` 📖	mathematical	—	`Lorentz.Vector.timeComponent` `LorentzGroup` `Lorentz.Vector` `TensorSpecies.Tensorial.smulAction` `realLorentzTensor.Color` `lorentzGroupIsGroup` `realLorentzTensor` `realLorentzTensor.Color.up` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.tensorial` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.minkowskiProduct` `toVector`	—	`Lorentz.Vector.smul_eq_sum` `Lorentz.Vector.minkowskiProduct_eq_timeComponent_spatialPart` `dual_mem` `inv_eq_dual` `toVector_apply` `minkowskiMatrix.dual_apply` `minkowskiMatrix.inl_0_inl_0` `minkowskiMatrix.inr_i_inr_i`
`toVector_apply` 📖	mathematical	—	`toVector` `LorentzGroup`	—	`Lorentz.Vector.smul_eq_sum` `Lorentz.Vector.basis_apply`
`toVector_continuous` 📖	mathematical	—	`LorentzGroup` `Lorentz.Vector` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `Lorentz.Vector.isNormedAddCommGroup` `toVector`	—	`toVector_eq_fun` `Lorentz.Vector.continuous_of_apply`
`toVector_eq_basis_iff_timeComponent_eq_one` 📖	mathematical	—	`toVector` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.basis` `LorentzGroup`	—	`toVector_timeComponent` `Lorentz.Vector.basis_apply` `toVector_minkowskiProduct_self` `Lorentz.Vector.smul_eq_sum` `toVector_apply` `Lorentz.Vector.minkowskiProduct_self_eq_timeComponent_spatialPart`
`toVector_eq_fun` 📖	mathematical	—	`toVector` `LorentzGroup`	—	`toVector_apply`
`toVector_minkowskiProduct_self` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.minkowskiProduct` `toVector`	—	`Lorentz.Vector.minkowskiProduct_invariant` `Lorentz.Vector.minkowskiProduct_basis_right` `minkowskiMatrix.inl_0_inl_0` `Lorentz.Vector.basis_apply`
`toVector_mul` 📖	mathematical	—	`toVector` `LorentzGroup` `lorentzGroupIsGroup` `Lorentz.Vector` `TensorSpecies.Tensorial.smulAction` `realLorentzTensor.Color` `realLorentzTensor` `realLorentzTensor.Color.up` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.tensorial`	—	`toVector.eq_1`
`toVector_neg` 📖	mathematical	—	`toVector` `LorentzGroup` `instNegElemMatrixSumFinOfNatNatReal` `Lorentz.Vector` `Lorentz.Vector.instAddCommGroup`	—	`Lorentz.Vector.neg_smul`
`toVector_timeComponent` 📖	mathematical	—	`Lorentz.Vector.timeComponent` `toVector` `LorentzGroup`	—	`toVector_apply`

---

← Back to Index