ker_eq_range

Mathlib.LinearAlgebra.Projection

URI: https://scilib.ai/kg/mathlib#LinearMap.IsIdempotentElem.ker_eq_range

← MathLib Explorer

English

For an idempotent endomorphism p, the kernel of p equals the image of I − p.

Русский

Для идемпотентного эндоморфизма p ядро p равно образу I − p.

LaTeX

$$$ \ker(p) = \operatorname{Im}(I - p) $$$

Lean4

theorem ker_eq_range {E : Type*} [AddCommGroup E] [Module S E] {p : E →ₗ[S] E} (hp : IsIdempotentElem p) :
    LinearMap.ker p = LinearMap.range (1 - p) := by simpa using hp.one_sub.range_eq_ker.symm

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

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

Разделы

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

Аффилиация

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