`BookProof.MixedLinearEsa.polyPotential_add_momentum_symmetric` (c : ℕ → ℝ) (n : ℕ) (m : V) : SymmetricOn (schwartzDomain V) (opL2 (potMomOp (polyPotential c n m) m))

Initializing...

`BookProof.MixedLinearEsa.polyPotential_add_momentum_symmetric` (c : ℕ → ℝ) (n : ℕ) (m : V) : SymmetricOn (schwartzDomain V) (opL2 (potMomOp (polyPotential c n m) m)) · Prove2Me