English
Interchanging roots and coroots, one still obtains a base of a root pairing. The flipped base b.flip has the same support and the root/coroot roles are swapped.
Русский
Замена ролей корней и коракорот приводит к новой базисной пары корней; базис b.flip имеет ту же опору, а роли корня и коракорота поменяны местами.
LaTeX
$$$\\text{flip: BaseBase} \\ (b.flip) \\text{ has }\\text{support}(b.flip)=\\text{support}(b),\\text{ and root/coroot swap.}$$$
Lean4
/-- Interchanging roots and coroots, one still has a base of a root pairing. -/
@[simps]
protected def flip : P.flip.Base where
support := b.support
linearIndepOn_root := b.linearIndepOn_coroot
linearIndepOn_coroot := b.linearIndepOn_root
root_mem_or_neg_mem := b.coroot_mem_or_neg_mem
coroot_mem_or_neg_mem := b.root_mem_or_neg_mem
