mem_maxTrivSubmodule — Mathlib

English

An element m belongs to the maximal trivial submodule if and only if every Lie action bracket with m vanishes: ∀ x ∈ L, [x,m] = 0.

Русский

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

LaTeX

$$$m\\in \\maxTrivSubmodule R L M \\iff \\forall x\\in L,\\,[x,m]=0$$$

Lean4

@[simp]
theorem mem_maxTrivSubmodule (m : M) : m ∈ maxTrivSubmodule R L M ↔ ∀ x : L, ⁅x, m⁆ = 0 :=
  Iff.rfl

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