range_eq_ker

Mathlib.Topology.Algebra.Module.LinearMap

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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