no goals
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
⊢ ↑χ ⁅x, y⁆ = 0
rw [LieHom.map_lie, LieRing.of_associative_ring_bracket, mul_comm, sub_self]