`BookProof.ChapterGaugeMechanicsCharge.euler_comm_mul` (g p : P) : eulerOp (g * p) - g * eulerOp p = (eulerOp g) * p
ProvedBookProof.ChapterGaugeMechanicsCharge.euler_comm_multheoremstimepiece
Prove the following Lean 4 theorem from ChapterGaugeMechanicsCharge.
BookProof.ChapterGaugeMechanicsCharge.euler_comm_mul (g p : P) : eulerOp (g * p) - g * eulerOp p = (eulerOp g) * p
Formalization note: Lean 4 identifier BookProof.ChapterGaugeMechanicsCharge.euler_comm_mul.
Preamble
-- Generated from ChapterGaugeMechanicsCharge.lean — theorem BookProof.ChapterGaugeMechanicsCharge.euler_comm_mul import Mathlib import Definitions.Def_ChapterGaugeMechanicsCharge open BookProof.ChapterGaugeMechanicsCharge open MvPolynomial
Formal statement
theorem BookProof.ChapterGaugeMechanicsCharge.euler_comm_mul (g p : P) :
eulerOp (g * p) - g * eulerOp p = (eulerOp g) * p := by sorry