Theorems · Theorem · nonassociative algebras

two_nsmul_lie_lmul_lmul_add_add_eq_zero

∀ {A : Type u_1} [inst : NonUnitalNonAssocCommRing A] [IsCommJordan A] (a b c : A),
  2 •
      (⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (b * c)⁆ +
          ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (c * a)⁆ +
        ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (a * b)⁆) =
    0

Defined in

Mathlib.Algebra.Jordan.Basic

Cited by

0 results in Mathlib

Foundations

Depth 44 from the axioms · uses propext, Quot.sound

Assumes

NonUnitalNonAssocCommRingIsCommJordan