genEigenspace_one

Mathlib.LinearAlgebra.Eigenspace.Basic

URI: https://scilib.ai/kg/mathlib#Module.End.genEigenspace_one

← MathLib Explorer

English

The generalized eigenspace at exponent 1 equals the kernel of f − μ·id.

Русский

Обобщённое собственное пространство при степени 1 равно ядру (f − μI).

LaTeX

$$$$ f.genEigenspace\\, μ\\, 1 = \\ker(f - μ\\cdot 1). $$$$

Lean4

theorem genEigenspace_one {f : End R M} {μ : R} : f.genEigenspace μ 1 = LinearMap.ker (f - μ • 1) := by
  rw [← Nat.cast_one, genEigenspace_nat, pow_one]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru