reflection_apply_root' — Mathlib

English

The dual annihilator of the coroot span maps to the infimum of kernels of coroot maps.

Русский

Дуальный аннигилирующий корорта отображает переход к пересечению ядров корорт отображений.

LaTeX

$$$(P.corootSpan R).dualAnnihilator.map P.toPerfPair.symm = \biginf_i ker(P.coroot' i)$$$

Lean4

theorem reflection_apply_root' (S : Type*) [CommRing S] [Algebra S R] [Module S M] [IsScalarTower S R M]
    [P.IsValuedIn S] : P.reflection i (P.root j) = P.root j - (P.pairingIn S j i) • P.root i := by
  rw [reflection_apply_root, ← P.algebraMap_pairingIn S, algebraMap_smul]

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