coweightEquiv_apply — Mathlib

English

For any e : RootPairing.Equiv P Q and n : N₂, the coweightEquiv acts by the image under e: coweightEquiv P Q e n = e.toHom.coweightMap n.

Русский

Для любого e: RootPairing.Equiv P Q и n: N₂ отображение ковейтов действует как образ через e: coweightEquiv P Q e n = e.toHom.coweightMap n.

LaTeX

$$$coweightEquiv(P,Q,e)(n) = e.toHom.coweightMap(n)$$$

Lean4

@[simp]
theorem coweightEquiv_apply (e : RootPairing.Equiv P Q) (n : N₂) : coweightEquiv P Q e n = e.toHom.coweightMap n :=
  rfl

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