feat(ClassicalMechanics): add rotational kinetic energy and prove T = ½ω·Iω - #1377

Merged

jstoobysmith merged 3 commits into

leanprover-community:masterfrom

giuseppesorge:rigidbody-rotational-kinetic-energy

Jul 8, 2026

Commits on Jul 7, 2026

feat(ClassicalMechanics): add rotational kinetic energy and prove T = ½ω·Iω

giuseppesorge
and
Claude Opus 4.8
committed
bd41619
refactor(ClassicalMechanics): address review — golf + extract smoothness lemma

giuseppesorge
and
Claude Opus 4.8
committed
3adcc35

Commits on Jul 8, 2026

refactor(Mathematics): move the cross-product smoothness lemma to CrossProduct

giuseppesorge
and
Claude Opus 4.8
committed
ae9e69b