feat(Commutation): prove `angularMomentumSqr_commutation_angularMomentum`#989

Open

pitmonticone wants to merge 2 commits intoleanprover-community:masterfrom

pitmonticone:aristotle-commutation

Commits on Mar 14, 2026

feat(Commutation): prove `angularMomentumSqr_commutation_angularMomentum`

pitmonticone
and
Aristotle-Harmonic
committed

Commits on Mar 16, 2026

refactor(Commutation): combine consecutive simp only calls

pitmonticone
and
Aristotle-Harmonic
committed