isFaithful_iff_ker_eq_bot — Mathlib

English

For a Lie algebra L acting on a module M, the action is faithful if and only if the kernel is trivial (equals {0}).

Русский

Для действия Ли-алгебры L на модуле M действие является корректным (faithful) тогда и только тогда, когда ядро действия равно нулю.

LaTeX

$$$\\text{IsFaithful}(R,L,M) \\iff \\mathrm{ker}(R,L,M) = \\{0\\}.$$$

Lean4

theorem isFaithful_iff_ker_eq_bot : IsFaithful R L M ↔ LieModule.ker R L M = ⊥ :=
  by
  rw [isFaithful_iff', LieSubmodule.ext_iff]
  aesop

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