feat(LaplaceRungeLenzVector): prove `angularMomentum_commutation_lrl`#991

Open

pitmonticone wants to merge 4 commits intoleanprover-community:masterfrom

pitmonticone:aristotle-laplacerungelenzvector

Commits on Mar 14, 2026

feat(LaplaceRungeLenzVector): prove `angularMomentum_commutation_lrl`

pitmonticone
and
Aristotle-Harmonic
committed

Commits on Mar 15, 2026

refactor(LaplaceRungeLenzVector): address review comments

pitmonticone
and
Aristotle-Harmonic
committed
fix(LaplaceRungeLenzVector): restore split simp calls (combining breaks rw)

pitmonticone
and
Aristotle-Harmonic
committed

Commits on Mar 17, 2026

refactor(LaplaceRungeLenzVector): remove unused simp args, drop unused have

pitmonticone
and
Aristotle-Harmonic
committed