genWeightSpaceChain_neg — Mathlib

English

Weight chain is invariant under negation: genWeightSpaceChain M (−χ1) χ2 (−q) (−p) = genWeightSpaceChain M χ1 χ2 p q.

Русский

Цепь весов инвариантна по отношению к отрицанию: genWeightSpaceChain M (−χ1) χ2 (−q) (−p) = genWeightSpaceChain M χ1 χ2 p q.

LaTeX

$$$\text{genWeightSpaceChain}(M, -χ_1, χ_2, -q, -p) = \text{genWeightSpaceChain}(M, χ_1, χ_2, p, q)$$$

Lean4

@[simp]
theorem genWeightSpaceChain_neg : genWeightSpaceChain M (-χ₁) χ₂ (-q) (-p) = genWeightSpaceChain M χ₁ χ₂ p q :=
  by
  let e : ℤ ≃ ℤ := neg_involutive.toPerm
  simp_rw [genWeightSpaceChain, ← e.biSup_comp (Ioo p q)]
  simp [e, -mem_Ioo]

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