IsDivSequence — Mathlib

English

A sequence W : ℤ → R is an Elliptic Divisibility Sequence if it is both an elliptic sequence and a divisibility sequence.

Русский

Последовательность W : ℤ → R является Эллиптической Последовательностью Делимости, если она одновременно эллиптическая и последовательность делимости.

LaTeX

$$$ IsEllDivSequence(W) \equiv (IsEllSequence(W) \land IsDivSequence(W)) $$$

Lean4

/-- The proposition that a sequence indexed by integers is a divisibility sequence. -/
def IsDivSequence : Prop :=
  ∀ m n : ℕ, m ∣ n → W m ∣ W n

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