Theorems · Theorem · nonassociative algebras

LieAlgebra.lieCharacterEquivLinearDual_symm_apply

∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [inst_3 : IsLieAbelian L]
  (ψ : Module.Dual R L), LieAlgebra.lieCharacterEquivLinearDual.symm ψ = { toLinearMap := ψ, map_lie' := ⋯ }

Defined in

Mathlib.Algebra.Lie.Character

Cited by

0 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Quot.sound

Assumes

CommRingLieRingLieAlgebraIsLieAbelian