Skip to content

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
Merged

feat(ClassicalMechanics): add rotational kinetic energy and prove T = ½ω·Iω#1377
jstoobysmith merged 3 commits into
leanprover-community:masterfrom
giuseppesorge:rigidbody-rotational-kinetic-energy

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

ae9e69b
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning
Lean based style linters
succeeded Jul 8, 2026 in 7m 13s