Theorems · Theorem · nonassociative algebras

sum_lie

∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] {ι : Type u_1}
  (s : Finset ι) (f : ι → L) (m : M), ⁅∑ i ∈ s, f i, m⁆ = ∑ i ∈ s, ⁅f i, m⁆

Defined in

Mathlib.Algebra.Lie.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

LieRingAddCommGroupLieRingModule