traceForm_coroot — Mathlib

English

The symmetric image under cartanEquivDual of α belongs to corootSpace α.

Русский

образ α через симметрическое отображение CartanEquivDual принадлежит corootSpace α.

LaTeX

$$$ (cartanEquivDual H).symm(α) ∈ corootSpace(α) $$$

Lean4

theorem traceForm_coroot (α : Weight K H L) (x : H) :
    traceForm K H L (coroot α) x = 2 • (α <| (cartanEquivDual H).symm α)⁻¹ • α x :=
  by
  have : cartanEquivDual H ((cartanEquivDual H).symm α) x = α x := by
    rw [LinearEquiv.apply_symm_apply, Weight.toLinear_apply]
  rw [coroot, map_nsmul, map_smul, LinearMap.smul_apply, LinearMap.smul_apply]
  congr 2

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