flip_flip — Mathlib

English

The flip operation on a root system induces an equivalence between the swapped root systems, i.e., there is a natural isomorphism between RootSystem ι R N M and RootSystem ι R M N.

Русский

Операция разворота в корневой системе задаёт естественную эквивалентность между избыточными корневыми системами: RootSystem ι R N M и RootSystem ι R M N.

LaTeX

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

Lean4

@[simp]
protected theorem _root_.RootSystem.flip_flip (P : RootSystem ι R M N) : P.flip.flip = P :=
  rfl

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