mem_ker — Mathlib

English

An element x of L lies in the kernel of the action on M if and only if x acts trivially on every m ∈ M, i.e., ∀ m ∈ M, [x,m] = 0.

Русский

Элемент x ∈ L принадлежит ядру действия на M тогда и только тогда, когда он действует тривиально на каждом m ∈ M, т.е. ∀ m ∈ M, [x,m] = 0.

LaTeX

$$$x\\in\\mathrm{ker}(R,L,M) \\iff \\forall m\\in M,\\,[x,m]=0$$$

Lean4

@[simp]
protected theorem mem_ker (x : L) : x ∈ LieModule.ker R L M ↔ ∀ m : M, ⁅x, m⁆ = 0 := by
  simp only [LieModule.ker, LieHom.mem_ker, LinearMap.ext_iff, LinearMap.zero_apply, toEnd_apply_apply]

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