English
Let e be a Lie algebra isomorphism from L to L'. Then the Killing forms satisfy κ'(e x, e y) = κ(x, y) for all x, y ∈ L.
Русский
Пусть e — изоморфизм Ли-алгебра от L к L'. Тогда Killing‑формы κ и κ' удовлетворяют κ'(e x, e y) = κ(x, y) для всех x, y ∈ L.
LaTeX
$$$\\forall e:\\ L \\xrightarrow{\\text{Lie}} L',\\; \\forall x,y \\in L:\\ κ'(e x, e y)=κ(x,y).$$$
Lean4
/-- Given an equivalence `e` of Lie algebras from `L` to `L'`, and elements `x y : L`, the
respective Killing forms of `L` and `L'` satisfy `κ'(e x, e y) = κ(x, y)`. -/
@[simp]
theorem killingForm_of_equiv_apply (e : L ≃ₗ⁅R⁆ L') (x y : L) : killingForm R L' (e x) (e y) = killingForm R L x y := by
simp_rw [killingForm_apply_apply, ← LieAlgebra.conj_ad_apply, ← LinearEquiv.conj_comp, LinearMap.trace_conj']
