Theorems · Theorem · number theory
Pell.IsFundamental.x_mul_y_le_y_mul_x
∀ {d : ℤ} {a₁ : Pell.Solution₁ d},
Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 1 < a.x → 0 < a.y → a.x * a₁.y ≤ a.y * a₁.x- Defined in
- Mathlib.NumberTheory.Pell
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 50 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- mul_oneproof · cited by 3,885
- add_zeroproof · cited by 2,707
- absproof · cited by 1,814
- zero_lt_oneproof · cited by 598
- LT.lt.transproof · cited by 370
- mul_powproof · cited by 220
- sub_nonnegproof · cited by 167
- abs_of_posproof · cited by 114
- abs_mulproof · cited by 98
- Pell.Solution₁statement and proof · cited by 50
- Pell.Solution₁.xstatement and proof · cited by 42
- Pell.Solution₁.ystatement and proof · cited by 40
Cited by3
Results whose statement or proof uses this declaration.
- Pell.IsFundamental.mul_inv_x_lt_xproof · cited by 1
- Pell.IsFundamental.mul_inv_x_posproof · cited by 1
- Pell.IsFundamental.mul_inv_y_nonnegproof · cited by 1