Theorems · Theorem · nonassociative algebras

sum_lie_sum

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

Defined in

Mathlib.Algebra.Lie.Basic

Cited by

0 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LieRingAddCommGroupLieRingModule