`BookProof.FreeFieldConstraint.constraint_commutation_identity_field` (D H φ0 : R) (hDH : bracket D H = 0) : bracket (bracket D φ0) H = - bracket D (bracket H φ0)
ProvedBookProof.FreeFieldConstraint.constraint_commutation_identity_fieldtheoremstimepiece
Prove the following Lean 4 theorem from ChapterFreeFieldConstraint.
BookProof.FreeFieldConstraint.constraint_commutation_identity_field (D H φ0 : R) (hDH : bracket D H = 0) : bracket (bracket D φ0) H = - bracket D (bracket H φ0)
Formalization note: Lean 4 identifier BookProof.FreeFieldConstraint.constraint_commutation_identity_field.
Preamble
-- Generated from ChapterFreeFieldConstraint.lean — theorem BookProof.FreeFieldConstraint.constraint_commutation_identity_field
import Mathlib
import Definitions.Def_ChapterFreeFieldConstraint
open BookProof.FreeFieldConstraint
variable {R : Type*} [Ring R]Formal statement
theorem BookProof.FreeFieldConstraint.constraint_commutation_identity_field (D H φ0 : R) (hDH : bracket D H = 0) :
bracket (bracket D φ0) H = - bracket D (bracket H φ0) := by sorry