sum_antidiagonal_card_esymm_psum_eq_zero

English

The sum over the antidiagonal of a certain signed product of esymm and psum vanishes; more precisely, the weighted sum in the antisymmetric combination equals zero.

Русский

Сумма по антидиагонали с соответствующими знаками даёт нулевое значение для полиномов esymm и psum в соответствующей комбинации.

LaTeX

$$$\sum a \in \operatorname{antidiagonal}(\lvert \sigma\rvert), (-1)^{a.\text{fst}} \mathrm{esymm}\, \sigma\, R a.\text{fst} \cdot \mathrm{psum}\, \sigma\, R a.\textsnd = 0$$$

Lean4

theorem sum_antidiagonal_card_esymm_psum_eq_zero :
    ∑ a ∈ antidiagonal (Fintype.card σ), (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd = 0 :=
  by
  let k := Fintype.card σ
  suffices (-1 : MvPolynomial σ R) ^ (k + 1) * ∑ a ∈ antidiagonal k, (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd = 0
    by simpa using this
  simp [k, ← sum_filter_add_sum_filter_not (antidiagonal k) (fun a ↦ a.fst < k), ← mul_esymm_eq_sum, mul_add,
    ← mul_assoc, ← pow_add, mul_comm ↑k (esymm σ R k)]

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