IsEllSequence — Mathlib

English

If W is an elliptic sequence, then for any scalar x in R, the sequence x•W is also elliptic.

Русский

Если W — эллиптическая последовательность, то для любого скаляра x в R последовательность x•W тоже эллиптическая.

LaTeX

$$$ IsEllSequence(W) \Rightarrow IsEllSequence(x\cdot W) \quad(\text{for all } x\in R) $$$

Lean4

/-- The proposition that a sequence indexed by integers is an elliptic sequence. -/
def IsEllSequence : Prop :=
  ∀ m n r : ℤ, W (m + n) * W (m - n) * W r ^ 2 = W (m + r) * W (m - r) * W n ^ 2 - W (n + r) * W (n - r) * W m ^ 2

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