flip — Mathlib

English

If P is a root system of type (ι,R,M,N), then interchanging M and N yields a root system of type (ι,R,N,M).

Русский

Если P является корневой системой типа (ι,R,M,N), то переброс ролей пространств M и N даёт корневую систему типа (ι,R,N,M).

LaTeX

$$$ P.flip : RootSystem_{\iota,R,N,M} \to RootSystem_{\iota,R,M,N} $$$

Lean4

/-- If we interchange the roles of `M` and `N`, we still have a root system. -/
protected def _root_.RootSystem.flip (P : RootSystem ι R M N) : RootSystem ι R N M :=
  { toRootPairing := P.toRootPairing.flip
    span_root_eq_top := P.span_coroot_eq_top
    span_coroot_eq_top := P.span_root_eq_top }

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