CrossProduct

📁 Source: PhysLean/SpaceAndTime/Space/CrossProduct.lean

Statistics

Metric	Count
Definitions «term_⨯ₑ₃_»	1
Theorems fderiv_cross_commute, inner_cross_self, inner_self_cross, time_deriv_cross_commute	4
Total	5

Space

Definitions

Name	Category	Theorems
«term_⨯ₑ₃_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fderiv_cross_commute 📖	mathematical	Time Time.instAddCommGroup Time.instModuleReal Time.instSeminormedAddCommGroup	Time.instOfNat	—	Time.fderiv_euclid crossProduct.eq_1 Time.differentiable_euclid
inner_cross_self 📖	—	—	—	—	—
inner_self_cross 📖	—	—	—	—	—
time_deriv_cross_commute 📖	mathematical	Time Time.instAddCommGroup Time.instModuleReal Time.instSeminormedAddCommGroup	Time.deriv	—	Time.deriv.eq_1 fderiv_cross_commute

---

← Back to Index