ad_apply_eq_zero_iff — Mathlib

English

For a finite-dimensional Killing Lie algebra, ad x = 0 implies x = 0, i.e., the adjoint map is injective.

Русский

Для конечномерной Killing-алгебры отображение adjoint инъективно: ad x = 0 тогда и только тогда, когда x = 0.

LaTeX

$$$\forall x \in L:\ ad_{R,L}(x) = 0 \iff x = 0.$$$

Lean4

@[simp]
theorem ad_apply_eq_zero_iff (x : L) : ad R L x = 0 ↔ x = 0 :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
  rwa [← LieHom.mem_ker, ad_ker_eq_center, LieAlgebra.center_eq_bot, LieSubmodule.mem_bot] at h

Похожие утверждения