isPell_norm — Mathlib

English

An element b ∈ ℤ√d satisfies IsPell(b) if and only if b times its conjugate equals 1.

Русский

Элемент b ∈ ℤ√d удовлетворяет IsPell(b) если и только если b умножить на его сопряжённое равно единице.

LaTeX

$$$\text{IsPell}(b) \iff b \cdot \text{star}(b) = 1.$$$

Lean4

theorem isPell_norm : ∀ {b : ℤ√d}, IsPell b ↔ b * star b = 1
  | ⟨x, y⟩ => by simp [Zsqrtd.ext_iff, IsPell, mul_comm]; ring_nf

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