English
For all integers m, normEDS(2m) · b equals normEDS(m−1)^2 · normEDS(m) · normEDS(m+2) − normEDS(m−2) · normEDS(m) · normEDS(m+1)^2.
Русский
Для целых m: normEDS(b,c,d,2m) · b = normEDS(b,c,d,m−1)^2 · normEDS(b,c,d,m) · normEDS(b,c,d,m+2) − normEDS(b,c,d,m−2) · normEDS(b,c,d,m) · normEDS(b,c,d,m+1)^2.
LaTeX
$$$\operatorname{normEDS}(b,c,d,2m) \cdot b = \operatorname{normEDS}(b,c,d,m-1)^2 \cdot \operatorname{normEDS}(b,c,d,m) \cdot \operatorname{normEDS}(b,c,d,m+2) - \operatorname{normEDS}(b,c,d,m-2) \cdot \operatorname{normEDS}(b,c,d,m) \cdot \operatorname{normEDS}(b,c,d,m+1)^2$$$
Lean4
theorem normEDS_even (m : ℤ) :
normEDS b c d (2 * m) * b =
normEDS b c d (m - 1) ^ 2 * normEDS b c d m * normEDS b c d (m + 2) -
normEDS b c d (m - 2) * normEDS b c d m * normEDS b c d (m + 1) ^ 2 :=
by
rw [← normEDS_mul_complEDS₂, mul_assoc, complEDS₂_mul_b]
ring1
