d_nonsquare

Mathlib.NumberTheory.Pell

URI: https://scilib.ai/kg/mathlib#Pell.IsFundamental.d_nonsquare

← MathLib Explorer

English

If a fundamental Pell solution exists, then d is not a square.

Русский

Если существует фундаментальное решение Пелля, то d не является квадратом.

LaTeX

$$$\neg \IsSquare(d)$$$

Lean4

/-- If a fundamental solution exists, then `d` must be a non-square. -/
theorem d_nonsquare {a : Solution₁ d} (h : IsFundamental a) : ¬IsSquare d :=
  d_nonsquare_of_one_lt_x h.1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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