mem_ωConjLieSubmodule_iff

Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

URI: https://scilib.ai/kg/mathlib#RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff

English

Membership in ωConjLieSubmodule N is equivalent to membership of (ω b) · x in N.

Русский

Принадлежность к ωConjLieSubmodule N эквивалентна принадлежности (ω b) · x к N.

LaTeX

$$$x \\in \\omegaConjLieSubmodule N \\iff (\\omega b) \\cdot x \\in N$$$

Lean4

@[simp]
theorem mem_ωConjLieSubmodule_iff {x : b.support ⊕ ι → R} : x ∈ ωConjLieSubmodule N ↔ (ω b) *ᵥ x ∈ N :=
  Iff.rfl

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

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

Разделы

Аффилиация

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