d_pos

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

If x, y ∈ ℕ and x^2 = d y^2 with d nonsquare, then x = 0 and y = 0.

Русский

Если x^2 = d y^2 для натуральных x, y и d ненквадратное, то x = 0 и y = 0.

LaTeX

$$$$\forall d \in \mathbb{N},\; [\text{Nonsquare}(d)]\Rightarrow \forall x,y \in \mathbb{N},\; x^2 = d y^2 \Rightarrow x=0 \land y=0.$$$$

Lean4

theorem d_pos : 0 < d :=
  lt_of_le_of_ne (Nat.zero_le _) <| Ne.symm <| Nonsquare.ns d 0

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

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

Разделы

Аффилиация

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