Theorems · Theorem · nonassociative algebras

DirectSum.lie_of

∀ {ι : Type v} (L : ι → Type w) [inst : (i : ι) → LieRing (L i)] [inst_1 : DecidableEq ι] {i j : ι} (x : L i) (y : L j),
  ⁅(DirectSum.of L i) x, (DirectSum.of L j) y⁆ = if hij : i = j then (DirectSum.of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0

Defined in

Mathlib.Algebra.Lie.DirectSum

Cited by

0 results in Mathlib

Foundations

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

Assumes

LieRingDecidableEq