Theorems · Theorem · nonassociative algebras

LieRinehartRing.leibniz_mul_right

∀ {A₁ : Type u_2} {L₁ : Type u_3} [inst : CommRing A₁] [inst_1 : LieRing L₁] [inst_2 : Module A₁ L₁]
  [inst_3 : LieRingModule L₁ A₁] [LieRinehartRing A₁ L₁] (x : L₁) (a b : A₁), ⁅x, a * b⁆ = a • ⁅x, b⁆ + ⁅x, a⁆ * b

Defined in

Mathlib.Algebra.LieRinehartAlgebra.Defs

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

CommRingLieRingModuleLieRingModuleLieRinehartRing