height_reflectionPerm_self — Mathlib

English

Under the index-negation symmetry, b.height(-i) equals the negative of b.height(i).

Русский

При симметрии относительно отражения индекса, высота при -i равна минусу высоты при i.

LaTeX

$$b.height (-i) = - b.height i$$

Lean4

theorem height_reflectionPerm_self (i : ι) :
    letI := P.indexNeg
    b.height (-i) = -b.height i :=
  by
  letI := P.indexNeg
  obtain ⟨f, hf₀, hf₁, hf₂⟩ := b.exists_root_eq_sum_int i
  have hf₃ : P.root (-i) = ∑ j ∈ b.support, (-f) j • P.root j := by simpa
  simp only [height_eq_sum hf₂, height_eq_sum hf₃, Pi.neg_apply, Finset.sum_neg_distrib]

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