ker_corootForm_eq_dualAnnihilator

English

The coroot form kernel is the image of the root span's dual annihilator under the flip map.

Русский

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

LaTeX

$$\\ker P.CorootForm = (P.rootSpan R).dualAnnihilator.map P.flip.toPerfPair.symm$$

Lean4

theorem ker_corootForm_eq_dualAnnihilator :
    LinearMap.ker P.CorootForm = (P.rootSpan R).dualAnnihilator.map P.flip.toPerfPair.symm :=
  P.flip.ker_rootForm_eq_dualAnnihilator

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