Documentation Verification Report

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` `Time.instSeminormedAddCommGroup` `Time.instAddCommGroup` `Time.instModuleReal` `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