instLieRing — Mathlib

Lean4
/-- Note that here we turn the `Mul` coming from the `NonUnitalNonAssocSemiring` structure
on `lib R X` into a `Bracket` on `FreeLieAlgebra`. -/
instance : LieRing (FreeLieAlgebra R X)
    where
  bracket := Quot.map₂ (· * ·) (fun _ _ _ => Rel.mul_left _) fun _ _ _ => Rel.mul_right _
  add_lie := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; change Quot.mk _ _ = Quot.mk _ _; simp_rw [add_mul]
  lie_add := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; change Quot.mk _ _ = Quot.mk _ _; simp_rw [mul_add]
  lie_self := by rintro ⟨a⟩; exact Quot.sound (Rel.lie_self a)
  leibniz_lie := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; exact Quot.sound (Rel.leibniz_lie a b c)
Похожие утверждения