Theorems · Theorem · nonassociative algebras

LieDerivation.SMulBracketCommClass.smul_bracket_comm

∀ {S : Type u_4} {L : Type u_5} {α : Type u_6} {inst : SMul S α} {inst_1 : LieRing L} {inst_2 : AddCommGroup α}
  {inst_3 : LieRingModule L α} [self : LieDerivation.SMulBracketCommClass S L α] (s : S) (l : L) (a : α),
  s • ⁅l, a⁆ = ⁅l, s • a⁆

• and ⁅⬝, ⬝⁆ are left commutative

Defined in

Mathlib.Algebra.Lie.Derivation.Basic

Cited by

0 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

LieDerivation.SMulBracketCommClass