feat(ClassicalMechanics): add the angular velocity vector of a rigid body

[giuseppesorge]

This PR adds the angular velocity vector ω of a rigid body, the three-dimensional counterpart of the angular velocity tensor Ω = Ṙ Rᵀ added in #1353.

In three dimensions the skew-symmetric tensor Ω ∈ 𝔰𝔬(3) is dual to a vector ω via the hat map (Physlib.Mathematics.CrossProductMatrix), characterised by [ω]ₓ = Ω. This is the angular velocity ω in the Landau–Lifshitz decomposition v = V + ω × r.

Physlib/Mathematics/CrossProductMatrix.lean

• crossProductMatrix_crossProductVee: on skew-symmetric matrices the hat map is a right inverse of the vee map (Aᵀ = -A → [Aᵛ]ₓ = A). Together with the existing crossProductVee_crossProductMatrix (left inverse) this exhibits ℝ³ ≃ 𝔰𝔬(3).

Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean (for RigidBodyMotion 3)

• angularVelocity ω := (angularVelocityTensor)ᵛ, with angularVelocity_eq;
• crossProductMatrix_angularVelocity: [ω]ₓ = Ω (uses the skew-symmetry of Ω, hence the differentiability hypothesis);
• angularVelocity_of_orientation_const: a body of constant orientation has ω = 0.

API-map.yaml

• marks the angular velocity of rotation requirement done, and (already present from feat(ClassicalMechanics): add RigidBodyMotion with centre-of-mass velocity #1320) the centre-of-mass velocity requirement;
• extends the Overview to cover the rigid-body motion API.

Toward #893. Depends only on merged work (#1320, #1324, #1353).

All declarations reduce to [propext, Classical.choice, Quot.sound].

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[jstoobysmith]

Great - looks good. Approved.