complEDS_neg — Mathlib

English

For integer m, the even step relation holds: complEDS(b,c,d,k,2m) = complEDS(b,c,d,k,m) · complEDS₂(b,c,d)(m·k).

Русский

Для целого m выполняется: complEDS(b,c,d,k,2m) = complEDS(b,c,d,k,m) · complEDS₂(b,c,d)(m·k).

LaTeX

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

Lean4

@[simp]
theorem complEDS_neg (n : ℤ) : complEDS b c d k (-n) = -complEDS b c d k n := by simp [complEDS]

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