English
For all R and b, c, d ∈ R and k ∈ ℤ, the product complEDS₂(b,c,d,k) · b equals normEDS(k-1)^2 · normEDS(k+2) − normEDS(k-2) · normEDS(k+1)^2.
Русский
Для любых R и b, c, d ∈ R и целого k выполняется: complEDS₂(b,c,d,k) · b = normEDS(b,c,d,k-1)^2 · normEDS(b,c,d,k+2) − normEDS(b,c,d,k-2) · normEDS(b,c,d,k+1)^2.
LaTeX
$$$\operatorname{complEDS}_2(b,c,d,k) \cdot b = \operatorname{normEDS}(b,c,d,k-1)^2 \cdot \operatorname{normEDS}(b,c,d,k+2) - \operatorname{normEDS}(b,c,d,k-2) \cdot \operatorname{normEDS}(b,c,d,k+1)^2$$$
Lean4
theorem complEDS₂_mul_b (k : ℤ) :
complEDS₂ b c d k * b =
normEDS b c d (k - 1) ^ 2 * normEDS b c d (k + 2) - normEDS b c d (k - 2) * normEDS b c d (k + 1) ^ 2 :=
by
induction k using Int.negInduction with
| nat
k =>
simp_rw [complEDS₂, normEDS, Int.even_add, Int.even_sub, even_two, iff_true, Int.not_even_one, iff_false]
split_ifs <;> ring1
| neg ih =>
simp_rw [complEDS₂_neg, ← sub_neg_eq_add, ← neg_sub', ← neg_add', normEDS_neg, ih]
ring1
