isPell_star

Mathlib.NumberTheory.PellMatiyasevic

URI: https://scilib.ai/kg/mathlib#Pell.isPell_star

English

Same statement as above: the set of Pell solutions is closed under multiplication.

Русский

То же самое: множество решений Пелля замкнуто относительно умножения.

LaTeX

$$$\forall d,\; (\forall b,c:\\mathbb{Z}\sqrt{d},\; \text{IsPell}(b) \to \text{IsPell}(c) \to \text{IsPell}(b c)).$$$

Lean4

theorem isPell_star : ∀ {b : ℤ√d}, IsPell b ↔ IsPell (star b)
  | ⟨x, y⟩ => by simp [IsPell]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru