mem_genWeightSpaceOf — Mathlib

English

If y ∈ W(L, χ1, x) and m ∈ W(M, χ2, x), then the bracket [y,m] lies in W(M, χ1+χ2, x). This expresses that action by a weight vector on a weight vector produces a weight vector of the sum weight.

Русский

Если y в W(L, χ1, x) и m в W(M, χ2, x), то скобка [y,m] принадлежит W(M, χ1+χ2, x). Это выражение говорит, что действие веса на вес порождает вес суммы.

LaTeX

$$$ y \\in \\mathbb{W}(L, χ_1, x),\\ m \\in \\mathbb{W}(M, χ_2, x) \\Rightarrow [y,m] \\in \\mathbb{W}(M, χ_1+χ_2, x) $$$

Lean4

theorem mem_genWeightSpaceOf (χ : R) (x : L) (m : M) :
    m ∈ genWeightSpaceOf M χ x ↔ ∃ k : ℕ, ((toEnd R L M x - χ • ↑1) ^ k) m = 0 := by simp [genWeightSpaceOf]

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