English
For all integers m, normEDS(2m+1) equals normEDS(m+2) · normEDS(m)^3 − normEDS(m−1) · normEDS(m+1)^3.
Русский
Для любого целого m выполняется: normEDS(b,c,d,2m+1) = normEDS(b,c,d,m+2) · normEDS(b,c,d,m)^3 − normEDS(b,c,d,m−1) · normEDS(b,c,d,m+1)^3.
LaTeX
$$$\operatorname{normEDS}(b,c,d,2m+1) = \operatorname{normEDS}(b,c,d,m+2) \cdot \operatorname{normEDS}(b,c,d,m)^3 - \operatorname{normEDS}(b,c,d,m-1) \cdot \operatorname{normEDS}(b,c,d,m+1)^3$$$
Lean4
theorem normEDS_odd (m : ℤ) :
normEDS b c d (2 * m + 1) =
normEDS b c d (m + 2) * normEDS b c d m ^ 3 - normEDS b c d (m - 1) * normEDS b c d (m + 1) ^ 3 :=
by
simp_rw [normEDS, preNormEDS_odd, if_neg m.not_even_two_mul_add_one, Int.even_add, Int.even_sub, even_two, iff_true,
Int.not_even_one, iff_false]
split_ifs <;> ring1
