Theorems · Theorem · nonassociative algebras

DirectSum.lie_of_of_ne

∀ {ι : Type v} (L : ι → Type w) [inst : (i : ι) → LieRing (L i)] [inst_1 : DecidableEq ι] {i j : ι},
  i ≠ j → ∀ (x : L i) (y : L j), ⁅(DirectSum.of L i) x, (DirectSum.of L j) y⁆ = 0

Defined in

Mathlib.Algebra.Lie.DirectSum

Cited by

1 results in Mathlib

Foundations

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

Assumes

LieRingDecidableEq