complEDS₂_neg — Mathlib

English

For all b,c,d and k ∈ ℤ, complEDS₂(b,c,d)(-k) = complEDS₂(b,c,d)(k).

Русский

Для любых b,c,d и k ∈ ℤ выполняется complEDS₂(b,c,d)(-k) = complEDS₂(b,c,d)(k).

LaTeX

$$$$\text{complEDS}_2(b,c,d)(-k) = \text{complEDS}_2(b,c,d)(k).$$$$

Lean4

@[simp]
theorem complEDS₂_neg (k : ℤ) : complEDS₂ b c d (-k) = complEDS₂ b c d k :=
  by
  simp_rw [complEDS₂, ← neg_add', ← sub_neg_eq_add, ← neg_sub', preNormEDS_neg, even_neg]
  ring1

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