therefore
Sign up
Open navigation

Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 1 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

1 result

Clear filters
Project-declaredLean 4.32.0

Angular Velocity Tensor transpose

RigidBodyMotion.angularVelocityTensor_transpose

Plain-language statement

The angular velocity tensor is skew-symmetric, Ī©įµ€ = -Ī©: it lies in the Lie algebra š”°š”¬(d). This is the litmus check that Ī© = į¹˜ Rįµ€ is a genuine angular-velocity tensor, and follows by differentiating the orthogonality identity R Rįµ€ = 1.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record