eq_zero_of_d_neg — Mathlib

English

If d < 0, then in any Pell solution a.x = 0 or a.y = 0.

Русский

Если d < 0, то в любом решении Пелля a.x = 0 или a.y = 0.

LaTeX

$$$$ d < 0 \Rightarrow \forall a \in Pell.Solution_1(d), a.x = 0 \lor a.y = 0. $$$$

Lean4

/-- When `d` is negative, then `x` or `y` must be zero in a solution. -/
theorem eq_zero_of_d_neg (h₀ : d < 0) (a : Solution₁ d) : a.x = 0 ∨ a.y = 0 :=
  by
  have h := a.prop
  contrapose! h
  have h1 := sq_pos_of_ne_zero h.1
  have h2 := sq_pos_of_ne_zero h.2
  nlinarith

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