sign_excenterWeights_singleton_neg

English

For Nat.AtLeastTwo n, the sign of s.excenterWeights { i } i is -1 for any i.

Русский

При Nat.AtLeastTwo n знак s.excenterWeights { i } i равен -1 для любого i.

LaTeX

$$$\operatorname{sign}\bigl(s.excenterWeights \{ i \} i\bigr) = -1$$$

Lean4

theorem sign_excenterWeights_singleton_neg [Nat.AtLeastTwo n] (i : Fin (n + 1)) :
    SignType.sign (s.excenterWeights { i } i) = -1 :=
  by
  simp_rw [excenterWeights, Pi.smul_apply, smul_eq_mul, sign_mul]
  convert one_mul _
  · rw [sign_eq_one_iff, inv_pos]
    exact s.sum_excenterWeightsUnnorm_singleton_pos i
  · simp [excenterWeightsUnnorm]

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