Theorems · Definition · number theory
Pell.IsFundamental
{d : ℤ} → Pell.Solution₁ d → PropWe define a solution to be fundamental if it has x > 1 and y > 0
and its x is the smallest possible among solutions with x > 1.
- Defined in
- Mathlib.NumberTheory.Pell
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Pell.Solution₁statement and proof · cited by 50
- Pell.Solution₁.xproof · cited by 42
- Pell.Solution₁.yproof · cited by 40
Cited by19
Results whose statement or proof uses this declaration.
- Pell.IsFundamental.d_posstatement and proof · cited by 6
- Pell.IsFundamental.x_mul_y_le_y_mul_xstatement and proof · cited by 3
- Pell.IsFundamental.x_posstatement and proof · cited by 3
- Pell.IsFundamental.eq_zpow_or_neg_zpowstatement and proof · cited by 2
- Pell.IsFundamental.exists_of_not_isSquarestatement · cited by 2
- Pell.IsFundamental.y_strictMonostatement and proof · cited by 2
- Pell.IsFundamental.eq_pow_of_nonnegstatement and proof · cited by 1
- Pell.IsFundamental.mul_inv_x_lt_xstatement and proof · cited by 1
- Pell.IsFundamental.mul_inv_x_posstatement and proof · cited by 1
- Pell.IsFundamental.mul_inv_y_nonnegstatement and proof · cited by 1
- Pell.IsFundamental.x_le_xstatement and proof · cited by 1
- Pell.IsFundamental.y_le_ystatement and proof · cited by 1