coweightEquiv_symm_coweightMap — Mathlib

English

The inverse of the coweightEquiv acts by sending the image under e.toHom.coweightMap back to n: (coweightEquiv P Q e).symm (e.toHom.coweightMap n) = n.

Русский

Обратный ковейтовый эквивалент отправляет образ под действием e.toHom.coweightMap обратно к n: (coweightEquiv P Q e).symm (e.toHom.coweightMap n) = n.

LaTeX

$$$\bigl(coweightEquiv(P,Q,e)\bigr)^{-1}\Bigl( e.toHom.coweightMap(n) \Bigr) = n$$$

Lean4

@[simp]
theorem coweightEquiv_symm_coweightMap (e : RootPairing.Equiv P Q) (n : N₂) :
    (coweightEquiv P Q e).symm (e.toHom.coweightMap n) = n :=
  (LinearEquiv.symm_apply_eq (coweightEquiv P Q e)).mpr rfl

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