exists_genWeightSpace_smul_add_eq_bot

English

There exists k > 0 such that genWeightSpace M (k • χ1 + χ2) = ⊥ for nilpotent L and χ1 ≠ 0.

Русский

Существует k > 0 такое, что genWeightSpace M (k • χ1 + χ2) = ⊥ при нильпотентности L и χ1 ≠ 0.

LaTeX

$$$\exists k \in \mathbb{Z}, k > 0 \,\wedge\; genWeightSpace(M, k \cdot χ_1 + χ_2) = 0$$$

Lean4

theorem exists_genWeightSpace_smul_add_eq_bot : ∃ k > 0, genWeightSpace M (k • χ₁ + χ₂) = ⊥ :=
  (Nat.eventually_pos.and <| eventually_genWeightSpace_smul_add_eq_bot M χ₁ χ₂ hχ₁).exists

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