rootForm_self_eq_zero_iff — Mathlib

English

The kernel of CorootForm equals the image of the dual annihilator of rootSpan under the flip map.

Русский

Ядро CorootForm равно образ двойного аннигилирующего подпространства корневого Span через разворот попаривания.

LaTeX

$$P.ker_corootForm_eq_dualAnnihilator$$

Lean4

theorem rootForm_self_eq_zero_iff {x : M} : P.RootForm x x = 0 ↔ x ∈ LinearMap.ker P.RootForm :=
  P.RootForm.apply_apply_same_eq_zero_iff P.zero_le_rootForm P.rootForm_symmetric

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