Theorems · Theorem · number theory

Pell.IsFundamental.y_le_y

∀ {d : ℤ} {a₁ : Pell.Solution₁ d}, Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 1 < a.x → 0 < a.y → a₁.y ≤ a.y

The y-coordinate of a fundamental solution is a lower bound for the y-coordinate of any positive solution.

Defined in

Mathlib.NumberTheory.Pell

Cited by

1 results in Mathlib

Foundations

Depth 49 from the axioms · uses propext, Classical.choice, Quot.sound