genEigenspace_zero_nat — Mathlib

English

For a natural exponent k ∈ ℕ, the 0-th generalized eigenspace of f at μ equals the kernel of f^k: genEigenspace μ 0 = ker(f^k).

Русский

Для натурального показателя k верна равенство: genEigenspace μ 0 = ker(f^k).

LaTeX

$$$f\,\mathrm{genEigenspace}(0,k) = \ker(f^{k})$$$

Lean4

@[simp]
theorem genEigenspace_zero_nat (f : End R M) (k : ℕ) : f.genEigenspace 0 k = LinearMap.ker (f ^ k) := by ext;
  simp [mem_genEigenspace_nat]

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