coweightMap_coweightEquiv_symm — Mathlib

English

For all n ∈ N, e.toHom.coweightMap ((coweightEquiv P Q e).symm n) = n.

Русский

Для всех n из N выполняется e.toHom.coweightMap ((coweightEquiv P Q e).symm n) = n.

LaTeX

$$$\forall n,\; e.toHom.coweightMap\bigl((coweightEquiv(P,Q,e)).symm(n)\bigr) = n$$$

Lean4

@[simp]
theorem coweightMap_coweightEquiv_symm (e : RootPairing.Equiv P Q) (n : N) :
    e.toHom.coweightMap ((coweightEquiv P Q e).symm n) = n :=
  by
  rw [← coweightEquiv_apply]
  exact LinearEquiv.apply_symm_apply (coweightEquiv P Q e) n

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