apply_eq_zero_of_isNilpotent — Mathlib

English

If the endomorphism toEnd x is nilpotent on the weight space and R has no zero divisors on M and R is reduced, then χ(x) = 0 for all weights χ.

Русский

Если эндоморфизм toEnd x нильпотент на весовом пространстве и R не имеет нулевых делителей на M, и R редуцирован, то для всех весов χ выполняется χ(x) = 0.

LaTeX

$$IsNilpotent (toEnd R L M x) ⇒ ∀ χ, χ x = 0$$

Lean4

theorem apply_eq_zero_of_isNilpotent [NoZeroSMulDivisors R M] [IsReduced R] (x : L)
    (h : _root_.IsNilpotent (toEnd R L M x)) (χ : Weight R L M) : χ x = 0 :=
  ((χ.hasEigenvalueAt x).isNilpotent_of_isNilpotent h).eq_zero

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