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