exists_ne_zero — Mathlib

English

For a nontrivial genWeightSpace, there exists a nonzero element x in genWeightSpace M χ. Thus genWeightSpace is nontrivial under mild hypotheses.

Русский

Для ненулевого genWeightSpace существует не нулевой элемент x в genWeightSpace M χ; следовательно, genWeightSpace не тривиально при умеренных условиях.

LaTeX

$$$\\exists x \\in \\mathrm{genWeightSpace}(M, χ), x \\neq 0$$$

Lean4

theorem exists_ne_zero (χ : Weight R L M) : ∃ x ∈ genWeightSpace M χ, x ≠ 0 := by
  simpa [LieSubmodule.eq_bot_iff] using χ.genWeightSpace_ne_bot

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