Theorems · Inductive type · nonassociative algebras

LieDerivation.SMulBracketCommClass

(S : Type u_4) →
  (L : Type u_5) →
    (α : Type u_6) → [SMul S α] → [inst : LieRing L] → [inst_1 : AddCommGroup α] → [LieRingModule L α] → Prop

A typeclass mixin saying that scalar multiplication and Lie bracket are left commutative.

Defined in

Mathlib.Algebra.Lie.Derivation.Basic

Cited by

4 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

SMulLieRingAddCommGroupLieRingModule