Theorems · Theorem · nonassociative algebras

LieModule.trace_toEnd_mul_eq_zero_of_traceForm_eq_zero

∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.traceForm R L M = 0 →
    ∀ (y : Module.End R M),
      (∀ z ∈ (LieModule.toEnd R L M).range, ⁅y, z⁆ ∈ (LieModule.toEnd R L M).range) →
        ∀ x ∈ LieAlgebra.derivedSeries R L 1, (LinearMap.trace R M) ((LieModule.toEnd R L M) x * y) = 0

Defined in

Mathlib.Algebra.Lie.TraceForm

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebraAddCommGroupModuleLieRingModuleLieModule