projection_ker

Mathlib.LinearAlgebra.Projection

URI: https://scilib.ai/kg/mathlib#Submodule.IsCompl.projection_ker

English

The kernel of hpq.projection is q.

Русский

Ядро hpq.projection равно q.

LaTeX

$$$\ker(hpq.projection)=q$$$

Lean4

@[simp]
theorem projection_ker (hpq : IsCompl p q) : ker hpq.projection = q := by simp [projection, ker_comp]

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

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

Разделы

Аффилиация

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