flipEquiv — Mathlib

English

The flip equivalence provides a structured isomorphism between RootSystem ι R N M and RootSystem ι R M N, realized by sending P to P.flip.

Русский

Эквивалентность разворота задаёт структурное тождество между RootSystem ι R N M и RootSystem ι R M N, реализуемое отправкой P в P.flip.

LaTeX

$$$ \mathrm{RootSystem\;flipEquiv} : RootSystem_{\iota,R,N,M} \simeq RootSystem_{\iota,R,M,N} $$$

Lean4

/-- `RootSystem.flip` as an equivalence. -/
@[simps]
def _root_.RootSystem.flipEquiv : RootSystem ι R N M ≃ RootSystem ι R M N
    where
  toFun P := P.flip
  invFun P := P.flip

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