isPell_iff_mem_unitary — Mathlib

English

For any b ∈ ℤ√d, IsPell(b) holds if and only if b belongs to the unitary group of ℤ√d.

Русский

Для любого b ∈ ℤ√d IsPell(b) выполняется тогда, когда b принадлежит группе единичных элементов ℤ√d.

LaTeX

$$$\forall b \in \mathbb{Z}\sqrt{d},\; \text{IsPell}(b) \iff b \in \mathrm{unitary}(\mathbb{Z}\sqrt{d}).$$$

Lean4

theorem isPell_iff_mem_unitary : ∀ {b : ℤ√d}, IsPell b ↔ b ∈ unitary (ℤ√d)
  | ⟨x, y⟩ => by rw [unitary.mem_iff, isPell_norm, mul_comm (star _), and_self_iff]

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