not_divides_sq

Mathlib.NumberTheory.Zsqrtd.Basic

URI: https://scilib.ai/kg/mathlib#Zsqrtd.not_divides_sq

English

For nonsquare d and any x,y ∈ ℕ, (x+1)^2 ≠ d (y+1)^2.

Русский

Для ненквадратного d и любых x,y ∈ ℕ имеется (x+1)^2 ≠ d (y+1)^2.

LaTeX

$$$$\forall d \in \mathbb{N},\; [\text{Nonsquare}(d)]\forall x,y \in \mathbb{N},\; (x+1)^2 \neq d (y+1)^2.$$$$

Lean4

theorem not_divides_sq (x y) : (x + 1) * (x + 1) ≠ d * (y + 1) * (y + 1) := fun e =>
  by
  have t := (divides_sq_eq_zero e).left
  contradiction

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

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

Разделы

Аффилиация

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