trace_h_eq_zero — Mathlib

English

The main endomorphism trace vanishing result holds for the Geck construction, finalizing the trace identity.

Русский

Основное тождество нулевого следа для Geck-конструкции завершено.

LaTeX

$$trace_toEnd_eq_zero (x) : trace = 0$$

Lean4

@[simp]
theorem trace_h_eq_zero : (h i).trace = 0 := by
  letI _i := P.indexNeg
  suffices ∑ j, P.pairingIn ℤ j i = 0
    by
    simp only [h_eq_diagonal, Matrix.trace_diagonal, Fintype.sum_sum_type, Finset.univ_eq_attach, Sum.elim_inl,
      Pi.zero_apply, Finset.sum_const_zero, Sum.elim_inr, zero_add]
    norm_cast
  suffices ∑ j, P.pairingIn ℤ (-j) i = ∑ j, P.pairingIn ℤ j i from eq_zero_of_neg_eq <| by simpa using this
  let σ : ι ≃ ι := Function.Involutive.toPerm _ neg_involutive
  exact σ.sum_comp (P.pairingIn ℤ · i)

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