Theorems · Theorem · number theory

Pell.IsFundamental.mul_inv_y_nonneg

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

If we multiply a positive solution with the inverse of a fundamental solution, the y-coordinate remains nonnegative.

Defined in

Mathlib.NumberTheory.Pell

Cited by

1 results in Mathlib

Foundations

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