Theorems · Theorem · nonassociative algebras

two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add

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

Defined in

Mathlib.Algebra.Jordan.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocCommRingIsCommJordan