feat(Momentum): prove `momentumOperatorSchwartz_isSymmetric`#990

Merged

jstoobysmith merged 7 commits intoleanprover-community:masterfrom

pitmonticone:aristotle-momentum

Mar 20, 2026

Commits on Mar 14, 2026

feat(Momentum): prove `momentumOperatorSchwartz_isSymmetric`

pitmonticone
and
Aristotle-Harmonic
committed

Commits on Mar 16, 2026

refactor(Momentum): remove private def derivSchwartz, use local let

pitmonticone
and
Aristotle-Harmonic
committed

Commits on Mar 19, 2026

golf(Momentum): shorten momentumOperatorSchwartz_isSymmetric proof

pitmonticone
and
Aristotle-Harmonic
committed
golf(Momentum): fold unfold and integral_neg into simp only

pitmonticone
and
Aristotle-Harmonic
committed

Commits on Mar 20, 2026