complEDS'_even — Mathlib

English

For every natural m, the even step relation holds: complEDS'(b,c,d,k,2(m+1)) = complEDS'(b,c,d,k,m+1) · complEDS₂(b,c,d)((m+1)·k).

Русский

Для каждого натурального m выполняется: complEDS'(b,c,d,k,2(m+1)) = complEDS'(b,c,d,k,m+1) · complEDS₂(b,c,d)((m+1)·k).

LaTeX

$$$\operatorname{complEDS}'(b,c,d,k,2\,(m+1)) = \operatorname{complEDS}'(b,c,d,k,m+1) \cdot \operatorname{complEDS}_2(b,c,d)((m+1)\,k)$$$

Lean4

theorem complEDS'_even (m : ℕ) :
    complEDS' b c d k (2 * (m + 1)) = complEDS' b c d k (m + 1) * complEDS₂ b c d ((m + 1) * k) := by
  rw [show 2 * (m + 1) = 2 * m + 2 by rfl, complEDS', dif_pos <| even_two_mul m, m.mul_div_cancel_left two_pos,
    Nat.cast_succ]

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