flip — Mathlib

English

Reversing the flip operation yields the original RootPairing.

Русский

Обратное применение операции flip возвращает исходное RootPairing.

LaTeX

$$$$ P.flip.flip = P $$$$

Lean4

/-- If we interchange the roles of `M` and `N`, we still have a root pairing. -/
@[simps!, simps toLinearMap]
protected def flip : RootPairing ι R N M
    where
  toLinearMap := P.toLinearMap.flip
  root := P.coroot
  coroot := P.root
  root_coroot_two := P.root_coroot_two
  reflectionPerm := P.reflectionPerm
  reflectionPerm_root := P.reflectionPerm_coroot
  reflectionPerm_coroot := P.reflectionPerm_root

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