English
If f HasUnifEigenvalue μ k for some exponent k and m > 0, then f HasUnifEigenvalue μ m for any positive exponent m.
Русский
Если μ является обобщённым собственным значением f для некоторого показателя k, и m>0, то μ является обобщённым собственным значением f для любого положительного показателя m.
LaTeX
$$$\forall f: \mathrm{End}_R M,\; \mu \in R,\; k,m \in \mathbb{N}_\infty,\; 0 < m \Rightarrow \text{HasUnifEigenvalue } f\, \mu\, k \Rightarrow \text{HasUnifEigenvalue } f\, \mu\, m$$$
Lean4
/-- A generalized eigenvalue for some exponent `k` is also
a generalized eigenvalue for positive exponents. -/
theorem lt {f : End R M} {μ : R} {k m : ℕ∞} (hm : 0 < m) (hk : f.HasUnifEigenvalue μ k) : f.HasUnifEigenvalue μ m :=
by
apply HasUnifEigenvalue.le (k := 1) (Order.one_le_iff_pos.mpr hm)
intro contra; apply hk
rw [genEigenspace_one, LinearMap.ker_eq_bot] at contra
rw [eq_bot_iff]
intro x hx
rw [mem_genEigenspace] at hx
rcases hx with ⟨l, -, hx⟩
rwa [LinearMap.ker_eq_bot.mpr] at hx
rw [Module.End.coe_pow (f - μ • 1) l]
exact Function.Injective.iterate contra l
