ker_eq_range

Mathlib.Topology.Algebra.Module.LinearMap

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

← MathLib Explorer

English

For an idempotent p, the kernel of p equals the range of (1 − p).

Русский

Для идемпотентного p ядро p совпадает с образом (1 − p).

LaTeX

$$$\text{IsIdempotentElem}(p) \Rightarrow \ker(p) = \operatorname{range}(1 - p)$$$

Lean4

theorem ker_eq_range {p : M →L[R] M} (hp : IsIdempotentElem p) : LinearMap.ker p = LinearMap.range (1 - p) :=
  LinearMap.IsIdempotentElem.ker_eq_range hp.toLinearMap

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

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

Разделы

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

Аффилиация

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