eigenspace_zero

Mathlib.LinearAlgebra.Eigenspace.Basic

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

← MathLib Explorer

English

The zero-eigenspace equals the kernel of f, i.e., f.eigenspace 0 = ker f.

Русский

Эйгенпространство нуля совпадает с ядром f: f.eigenspace 0 = ker f.

LaTeX

$$f.\text{eigenspace}(0) = \ker f$$

Lean4

@[simp]
theorem eigenspace_zero (f : End R M) : f.eigenspace 0 = LinearMap.ker f := by
  simp only [eigenspace, ← Nat.cast_one (R := ℕ∞), genEigenspace_zero_nat, pow_one]

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

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

Разделы

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

Аффилиация

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