LightLike

Statistics

Metric	Count
Definitions	0
Theorems `causalCharacter_zero`, `causallyPrecedes_refl`, `lightLike_iff_norm_sq_zero`, `lightlike_eq_spatial_norm_of_eq_time`, `lightlike_spatial_parallel_implies_proportional`	5
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`causalCharacter_zero` 📖	mathematical	—	`causalCharacter` `Lorentz.Vector` `instAddCommGroup` `CausalCharacter.lightLike`	—	—
`causallyPrecedes_refl` 📖	mathematical	—	`causallyPrecedes`	—	`apply_sub` `causalCharacter_zero`
`lightLike_iff_norm_sq_zero` 📖	mathematical	—	`causalCharacter` `CausalCharacter.lightLike` `Lorentz.Vector` `isNormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `instAddCommGroup` `minkowskiProduct`	—	—
`lightlike_eq_spatial_norm_of_eq_time` 📖	mathematical	`causalCharacter` `CausalCharacter.lightLike` `timeComponent`	`spatialPart`	—	`minkowskiProduct_toCoord` `lightLike_iff_norm_sq_zero`
`lightlike_spatial_parallel_implies_proportional` 📖	—	`causalCharacter` `CausalCharacter.lightLike` `Lorentz.Vector` `isNormedAddCommGroup` `instAddCommMonoid` `instModuleReal`	—	—	`minkowskiProduct_toCoord` `lightLike_iff_norm_sq_zero`

---