Theorems · Theorem · nonassociative algebras

LieAlgebra.Basis.lie_h_h

∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (self : LieAlgebra.Basis ι H) (i j : ι), ⁅self.h i, self.h j⁆ = 0

Defined in

Mathlib.Algebra.Lie.Basis.Basic

Cited by

2 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext

Assumes

FiniteCommRingLieRingLieAlgebra