d_pos — Mathlib

English

For any a > 1 (in natural numbers), the associated Pell parameter d(a) is positive.

Русский

Для любого a > 1 (в натуральных), соответствующий параметр Пелля d(a) положителен.

LaTeX

$$$\forall a \in \mathbb{N},\; a > 1 \Rightarrow d(a) > 0.$$$

Lean4

@[simp]
theorem d_pos : 0 < d a1 :=
  tsub_pos_of_lt
    (mul_lt_mul a1 (le_of_lt a1) (by decide) (Nat.zero_le _) : 1 * 1 < a * a)
      -- TODO(lint): Fix double namespace issue

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