mem_idealizer

Mathlib.Algebra.Lie.Normalizer

URI: https://scilib.ai/kg/mathlib#LieSubmodule.mem_idealizer

English

x ∈ N.idealizer ⇔ ∀ m ∈ M, [x,m] ∈ N.

Русский

x принадлежит N.idealizer тогда и только тогда, когда для всех m ∈ M выполняется [x,m] ∈ N.

LaTeX

$$$ x \\in N.idealizer \\iff \\forall m : M, [x,m] \\in N $$$

Lean4

@[simp]
theorem mem_idealizer {x : L} : x ∈ N.idealizer ↔ ∀ m : M, ⁅x, m⁆ ∈ N :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru