A last nonzero power trace

If a linear functional is nonzero on a nilpotent element, some positive power has nonzero value and every higher power of that element has value zero. This is the reduction in Schrijver's factorial-rank proof of nilpotent-trace vanishing (arXiv:1211.3561, Proposition 4).

structure RS.SinglePowerTrace {A : Type u_1} [Ring A] [Algebra ℂ A] (τ : A →ₗ[ℂ] ℂ) (y : A) : Prop

A nonzero trace whose powers of degree at least two have zero trace. No normalization of the nonzero value is required.

• trace_ne_zero : τ y ≠ 0

  The first power has nonzero trace.

• higher_eq_zero (m : ℕ) : 2 ≤ m → τ (y ^ m) = 0

  All higher powers have zero trace.

theorem RS.exists_singlePowerTrace_pow {A : Type u_1} [Ring A] [Algebra ℂ A] (τ : A →ₗ[ℂ] ℂ) {g : A} (hg : IsNilpotent g) (hτ : τ g ≠ 0) : ∃ (r : ℕ), 1 ≤ r ∧ SinglePowerTrace τ (g ^ r)

A nilpotent element with nonzero trace has a positive power whose first trace is nonzero and whose higher power traces vanish.