Physlib.ClassicalMechanics.RigidBody.AngularMomentum

Imports

/-
Copyright (c) 2026 Giuseppe Sorge. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Giuseppe Sorge
-/
module

public import Physlib.ClassicalMechanics.RigidBody.Basic
public import Physlib.Mathematics.CrossProduct

Angular momentum of a rigid body

For a rigid body rotating with angular velocity ω about its reference point, each body point at position r moves with velocity ω × r, so the body's angular momentum about that point is L = ∫ r × (ω × r) dm. Expanding the double cross product, r × (ω × r) = |r|² ω − (r · ω) r, shows that L is linear in ω with matrix the inertia tensor: L = I ω.

References

Landau and Lifshitz, Mechanics, Section 32.

@[expose] public section

The angular momentum of a rigid body equals its inertia tensor applied to the angular velocity: L = I ω.


theorem angularMomentum_eq_inertiaTensor_mulVec (R : RigidBody 3) (ω : Fin 3 → ℝ) :
    R.angularMomentum ω = R.inertiaTensor *ᵥ ω := byR:RigidBody 3ω:Fin 3 → ℝ⊢ R.angularMomentum ω = R.inertiaTensor *ᵥ ω
  funext iR:RigidBody 3ω:Fin 3 → ℝi:Fin 3⊢ R.angularMomentum ω i = (R.inertiaTensor *ᵥ ω) i
  simp only [angularMomentum, mulVec, dotProduct, inertiaTensor]R:RigidBody 3ω:Fin 3 → ℝi:Fin 3⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ x, R.ρ ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩ * ω x
  have hsmul : ∀ j : Fin 3,
      R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, (x k) ^ 2 - x i * x j,
        ContDiff.contMDiff <| byR:RigidBody 3ω:Fin 3 → ℝi:Fin 3j:Fin 3⊢ ContDiff ℝ ⊤ fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 jR:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ x, R.ρ ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩ * ω x fun_propAll goals completed! 🐙R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ x, R.ρ ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩ * ω x⟩ * ω j
      = R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, (x k) ^ 2 - x i * x j,
        ContDiff.contMDiff <| byR:RigidBody 3ω:Fin 3 → ℝi:Fin 3j:Fin 3⊢ ContDiff ℝ ⊤ fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 jR:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ x, R.ρ ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩ * ω x fun_propAll goals completed! 🐙R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ x, R.ρ ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩ * ω x⟩) := byR:RigidBody 3ω:Fin 3 → ℝ⊢ R.angularMomentum ω = R.inertiaTensor *ᵥ ωR:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ x, R.ρ ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩ * ω x
    intro jR:RigidBody 3ω:Fin 3 → ℝi:Fin 3j:Fin 3⊢ R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
  R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ x, R.ρ ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩ * ω x
    rw [map_smul,R:RigidBody 3ω:Fin 3 → ℝi:Fin 3j:Fin 3⊢ R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
  ω j • R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ x, R.ρ ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩ * ω x smul_eq_mul,R:RigidBody 3ω:Fin 3 → ℝi:Fin 3j:Fin 3⊢ R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
  ω j * R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ x, R.ρ ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩ * ω x mul_commR:RigidBody 3ω:Fin 3 → ℝi:Fin 3j:Fin 3⊢ ω j * R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ =
  ω j * R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ x, R.ρ ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩ * ω x]R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ x, R.ρ ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩ * ω xR:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ x, R.ρ ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩ * ω x
  rw [Finset.sum_congr rfl (fun j _ => hsmul j),R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ j, R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  R.ρ (∑ x, ω x • ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩) ← map_sumR:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  R.ρ (∑ x, ω x • ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩)R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  R.ρ (∑ x, ω x • ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩)]R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ R.ρ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  R.ρ (∑ x, ω x • ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩)
  congr 1e_6R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)⊢ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ =
  ∑ x, ω x • ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩
  ext xe_6R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)x:Space⊢ ⟨fun x => (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i, ⋯⟩ x =
  (∑ x, ω x • ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩) x
  simp only [ContMDiffMap.coeFn_mk]e_6R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)x:Space⊢ (crossProduct (x.val 3)) ((crossProduct ω) (x.val 3)) i =
  (∑ x, ω x • ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩) x
  rw [cross_cross_self_apply,e_6R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)x:Space⊢ (∑ k, x.val 3 k ^ 2) * ω i - (∑ j, x.val 3 j * ω j) * x.val 3 i =
  (∑ x, ω x • ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩) xe_6R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)x:Space⊢ (∑ k, x.val 3 k ^ 2) * ω i - (∑ j, x.val 3 j * ω j) * x.val 3 i =
  ∑ c,
    ContMDiffMap.coeFnAddMonoidHom
      (ω c • ⟨fun x => (if i = c then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 c, ⋯⟩) x ← ContMDiffMap.coeFnAddMonoidHom_apply,e_6R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)x:Space⊢ (∑ k, x.val 3 k ^ 2) * ω i - (∑ j, x.val 3 j * ω j) * x.val 3 i =
  ContMDiffMap.coeFnAddMonoidHom
    (∑ x, ω x • ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩) xe_6R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)x:Space⊢ (∑ k, x.val 3 k ^ 2) * ω i - (∑ j, x.val 3 j * ω j) * x.val 3 i =
  ∑ c,
    ContMDiffMap.coeFnAddMonoidHom
      (ω c • ⟨fun x => (if i = c then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 c, ⋯⟩) x map_sum,e_6R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)x:Space⊢ (∑ k, x.val 3 k ^ 2) * ω i - (∑ j, x.val 3 j * ω j) * x.val 3 i =
  (∑ x,
      ContMDiffMap.coeFnAddMonoidHom
        (ω x • ⟨fun x_1 => (if i = x then 1 else 0) * ∑ k, x_1.val 3 k ^ 2 - x_1.val 3 i * x_1.val 3 x, ⋯⟩))
    xe_6R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)x:Space⊢ (∑ k, x.val 3 k ^ 2) * ω i - (∑ j, x.val 3 j * ω j) * x.val 3 i =
  ∑ c,
    ContMDiffMap.coeFnAddMonoidHom
      (ω c • ⟨fun x => (if i = c then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 c, ⋯⟩) x
    Finset.sum_applye_6R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)x:Space⊢ (∑ k, x.val 3 k ^ 2) * ω i - (∑ j, x.val 3 j * ω j) * x.val 3 i =
  ∑ c,
    ContMDiffMap.coeFnAddMonoidHom
      (ω c • ⟨fun x => (if i = c then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 c, ⋯⟩) xe_6R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)x:Space⊢ (∑ k, x.val 3 k ^ 2) * ω i - (∑ j, x.val 3 j * ω j) * x.val 3 i =
  ∑ c,
    ContMDiffMap.coeFnAddMonoidHom
      (ω c • ⟨fun x => (if i = c then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 c, ⋯⟩) x]e_6R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)x:Space⊢ (∑ k, x.val 3 k ^ 2) * ω i - (∑ j, x.val 3 j * ω j) * x.val 3 i =
  ∑ c,
    ContMDiffMap.coeFnAddMonoidHom
      (ω c • ⟨fun x => (if i = c then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 c, ⋯⟩) x
  simp only [ContMDiffMap.coeFnAddMonoidHom_apply, ContMDiffMap.coe_smul, Pi.smul_apply,
    ContMDiffMap.coeFn_mk, smul_eq_mul]e_6R:RigidBody 3ω:Fin 3 → ℝi:Fin 3hsmul:∀ (j : Fin 3),
  R.ρ ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩ * ω j =
    R.ρ (ω j • ⟨fun x => (if i = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 j, ⋯⟩)x:Space⊢ (∑ k, x.val 3 k ^ 2) * ω i - (∑ j, x.val 3 j * ω j) * x.val 3 i =
  ∑ x_1, ω x_1 * ((if i = x_1 then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 i * x.val 3 x_1)
  fin_cases ie_6.«0»R:RigidBody 3ω:Fin 3 → ℝx:Spacehsmul:∀ (j : Fin 3),
  R.ρ
        ⟨fun x =>
          (if (fun i => i) ⟨0, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨0, ⋯⟩) * x.val 3 j,
          ⋯⟩ *
      ω j =
    R.ρ
      (ω j •
        ⟨fun x =>
          (if (fun i => i) ⟨0, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨0, ⋯⟩) * x.val 3 j,
          ⋯⟩)⊢ (∑ k, x.val 3 k ^ 2) * ω ((fun i => i) ⟨0, ⋯⟩) - (∑ j, x.val 3 j * ω j) * x.val 3 ((fun i => i) ⟨0, ⋯⟩) =
  ∑ x_1,
    ω x_1 *
      ((if (fun i => i) ⟨0, ⋯⟩ = x_1 then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨0, ⋯⟩) * x.val 3 x_1)e_6.«1»R:RigidBody 3ω:Fin 3 → ℝx:Spacehsmul:∀ (j : Fin 3),
  R.ρ
        ⟨fun x =>
          (if (fun i => i) ⟨1, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨1, ⋯⟩) * x.val 3 j,
          ⋯⟩ *
      ω j =
    R.ρ
      (ω j •
        ⟨fun x =>
          (if (fun i => i) ⟨1, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨1, ⋯⟩) * x.val 3 j,
          ⋯⟩)⊢ (∑ k, x.val 3 k ^ 2) * ω ((fun i => i) ⟨1, ⋯⟩) - (∑ j, x.val 3 j * ω j) * x.val 3 ((fun i => i) ⟨1, ⋯⟩) =
  ∑ x_1,
    ω x_1 *
      ((if (fun i => i) ⟨1, ⋯⟩ = x_1 then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨1, ⋯⟩) * x.val 3 x_1)e_6.«2»R:RigidBody 3ω:Fin 3 → ℝx:Spacehsmul:∀ (j : Fin 3),
  R.ρ
        ⟨fun x =>
          (if (fun i => i) ⟨2, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨2, ⋯⟩) * x.val 3 j,
          ⋯⟩ *
      ω j =
    R.ρ
      (ω j •
        ⟨fun x =>
          (if (fun i => i) ⟨2, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨2, ⋯⟩) * x.val 3 j,
          ⋯⟩)⊢ (∑ k, x.val 3 k ^ 2) * ω ((fun i => i) ⟨2, ⋯⟩) - (∑ j, x.val 3 j * ω j) * x.val 3 ((fun i => i) ⟨2, ⋯⟩) =
  ∑ x_1,
    ω x_1 *
      ((if (fun i => i) ⟨2, ⋯⟩ = x_1 then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨2, ⋯⟩) * x.val 3 x_1) <;>e_6.«0»R:RigidBody 3ω:Fin 3 → ℝx:Spacehsmul:∀ (j : Fin 3),
  R.ρ
        ⟨fun x =>
          (if (fun i => i) ⟨0, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨0, ⋯⟩) * x.val 3 j,
          ⋯⟩ *
      ω j =
    R.ρ
      (ω j •
        ⟨fun x =>
          (if (fun i => i) ⟨0, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨0, ⋯⟩) * x.val 3 j,
          ⋯⟩)⊢ (∑ k, x.val 3 k ^ 2) * ω ((fun i => i) ⟨0, ⋯⟩) - (∑ j, x.val 3 j * ω j) * x.val 3 ((fun i => i) ⟨0, ⋯⟩) =
  ∑ x_1,
    ω x_1 *
      ((if (fun i => i) ⟨0, ⋯⟩ = x_1 then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨0, ⋯⟩) * x.val 3 x_1)e_6.«1»R:RigidBody 3ω:Fin 3 → ℝx:Spacehsmul:∀ (j : Fin 3),
  R.ρ
        ⟨fun x =>
          (if (fun i => i) ⟨1, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨1, ⋯⟩) * x.val 3 j,
          ⋯⟩ *
      ω j =
    R.ρ
      (ω j •
        ⟨fun x =>
          (if (fun i => i) ⟨1, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨1, ⋯⟩) * x.val 3 j,
          ⋯⟩)⊢ (∑ k, x.val 3 k ^ 2) * ω ((fun i => i) ⟨1, ⋯⟩) - (∑ j, x.val 3 j * ω j) * x.val 3 ((fun i => i) ⟨1, ⋯⟩) =
  ∑ x_1,
    ω x_1 *
      ((if (fun i => i) ⟨1, ⋯⟩ = x_1 then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨1, ⋯⟩) * x.val 3 x_1)e_6.«2»R:RigidBody 3ω:Fin 3 → ℝx:Spacehsmul:∀ (j : Fin 3),
  R.ρ
        ⟨fun x =>
          (if (fun i => i) ⟨2, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨2, ⋯⟩) * x.val 3 j,
          ⋯⟩ *
      ω j =
    R.ρ
      (ω j •
        ⟨fun x =>
          (if (fun i => i) ⟨2, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨2, ⋯⟩) * x.val 3 j,
          ⋯⟩)⊢ (∑ k, x.val 3 k ^ 2) * ω ((fun i => i) ⟨2, ⋯⟩) - (∑ j, x.val 3 j * ω j) * x.val 3 ((fun i => i) ⟨2, ⋯⟩) =
  ∑ x_1,
    ω x_1 *
      ((if (fun i => i) ⟨2, ⋯⟩ = x_1 then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨2, ⋯⟩) * x.val 3 x_1) simp [Fin.sum_univ_three]e_6.«2»R:RigidBody 3ω:Fin 3 → ℝx:Spacehsmul:∀ (j : Fin 3),
  R.ρ
        ⟨fun x =>
          (if (fun i => i) ⟨2, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨2, ⋯⟩) * x.val 3 j,
          ⋯⟩ *
      ω j =
    R.ρ
      (ω j •
        ⟨fun x =>
          (if (fun i => i) ⟨2, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨2, ⋯⟩) * x.val 3 j,
          ⋯⟩)⊢ (x.val 3 0 ^ 2 + x.val 3 1 ^ 2 + x.val 3 2 ^ 2) * ω 2 -
    (x.val 3 0 * ω 0 + x.val 3 1 * ω 1 + x.val 3 2 * ω 2) * x.val 3 2 =
  -(ω 0 * (x.val 3 2 * x.val 3 0)) + -(ω 1 * (x.val 3 2 * x.val 3 1)) +
    ω 2 * (x.val 3 0 ^ 2 + x.val 3 1 ^ 2 + x.val 3 2 ^ 2 - x.val 3 2 * x.val 3 2) <;>e_6.«0»R:RigidBody 3ω:Fin 3 → ℝx:Spacehsmul:∀ (j : Fin 3),
  R.ρ
        ⟨fun x =>
          (if (fun i => i) ⟨0, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨0, ⋯⟩) * x.val 3 j,
          ⋯⟩ *
      ω j =
    R.ρ
      (ω j •
        ⟨fun x =>
          (if (fun i => i) ⟨0, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨0, ⋯⟩) * x.val 3 j,
          ⋯⟩)⊢ (x.val 3 0 ^ 2 + x.val 3 1 ^ 2 + x.val 3 2 ^ 2) * ω 0 -
    (x.val 3 0 * ω 0 + x.val 3 1 * ω 1 + x.val 3 2 * ω 2) * x.val 3 0 =
  ω 0 * (x.val 3 0 ^ 2 + x.val 3 1 ^ 2 + x.val 3 2 ^ 2 - x.val 3 0 * x.val 3 0) + -(ω 1 * (x.val 3 0 * x.val 3 1)) +
    -(ω 2 * (x.val 3 0 * x.val 3 2))e_6.«1»R:RigidBody 3ω:Fin 3 → ℝx:Spacehsmul:∀ (j : Fin 3),
  R.ρ
        ⟨fun x =>
          (if (fun i => i) ⟨1, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨1, ⋯⟩) * x.val 3 j,
          ⋯⟩ *
      ω j =
    R.ρ
      (ω j •
        ⟨fun x =>
          (if (fun i => i) ⟨1, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨1, ⋯⟩) * x.val 3 j,
          ⋯⟩)⊢ (x.val 3 0 ^ 2 + x.val 3 1 ^ 2 + x.val 3 2 ^ 2) * ω 1 -
    (x.val 3 0 * ω 0 + x.val 3 1 * ω 1 + x.val 3 2 * ω 2) * x.val 3 1 =
  -(ω 0 * (x.val 3 1 * x.val 3 0)) + ω 1 * (x.val 3 0 ^ 2 + x.val 3 1 ^ 2 + x.val 3 2 ^ 2 - x.val 3 1 * x.val 3 1) +
    -(ω 2 * (x.val 3 1 * x.val 3 2))e_6.«2»R:RigidBody 3ω:Fin 3 → ℝx:Spacehsmul:∀ (j : Fin 3),
  R.ρ
        ⟨fun x =>
          (if (fun i => i) ⟨2, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨2, ⋯⟩) * x.val 3 j,
          ⋯⟩ *
      ω j =
    R.ρ
      (ω j •
        ⟨fun x =>
          (if (fun i => i) ⟨2, ⋯⟩ = j then 1 else 0) * ∑ k, x.val 3 k ^ 2 - x.val 3 ((fun i => i) ⟨2, ⋯⟩) * x.val 3 j,
          ⋯⟩)⊢ (x.val 3 0 ^ 2 + x.val 3 1 ^ 2 + x.val 3 2 ^ 2) * ω 2 -
    (x.val 3 0 * ω 0 + x.val 3 1 * ω 1 + x.val 3 2 * ω 2) * x.val 3 2 =
  -(ω 0 * (x.val 3 2 * x.val 3 0)) + -(ω 1 * (x.val 3 2 * x.val 3 1)) +
    ω 2 * (x.val 3 0 ^ 2 + x.val 3 1 ^ 2 + x.val 3 2 ^ 2 - x.val 3 2 * x.val 3 2) ringAll goals completed! 🐙