mem_zeroRootSubalgebra — Mathlib

English

For an element χ ∈ zeroRootSubalgebra R L H, this is equivalent to the condition that for all m in H, there exists k with (toEnd R H L y)^k x = 0 describing zero weight behavior.

Русский

Для элемента χ ∈ zeroRootSubalgebra R L H равносильно условию, что для каждого m∈H существует k, такое что (toEnd R H L y)^k x = 0, что описывает нулевой вес.

LaTeX

$$mem_zeroRootSubalgebra : x ∈ zeroRootSubalgebra R L H ↔ ∀ y ∈ H, ∃ k : ℕ, (toEnd R H L y ^ k) x = 0$$

Lean4

theorem mem_zeroRootSubalgebra (x : L) : x ∈ zeroRootSubalgebra R L H ↔ ∀ y : H, ∃ k : ℕ, (toEnd R H L y ^ k) x = 0 :=
  by
  change x ∈ rootSpace H 0 ↔ _
  simp only [mem_genWeightSpace, Pi.zero_apply, zero_smul, sub_zero]

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