Mathlib Map

Theorems · Definition · number theory

Pell.IsPell

{d : ℤ} → ℤ√d → Prop

The property of being a solution to the Pell equation, expressed as a property of elements of ℤ√d.

Defined in
Mathlib.NumberTheory.PellMatiyasevic
Cited by
9 results in Mathlib
Foundations
Depth 14 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Pell.isPell_norm · cited by 3Pell.isPell_normPell.isPell_pellZd · cited by 2Pell.isPell_pellZdPell.eq_pellZd · cited by 1Pell.eq_pellZdPell.eq_pell_lem · cited by 1Pell.eq_pell_lemPell.isPell_nat · cited by 1Pell.isPell_natPell.isPell_iff_mem_unitary · cited by 0Pell.isPell_iff_mem_unita…Pell.isPell_mul · cited by 0Pell.isPell_mulPell.isPell_one · cited by 0Pell.isPell_onePell.isPell_star · cited by 0Pell.isPell_starZsqrtd · cited by 105ZsqrtdPell.IsPellCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Zsqrtdstatement and proof · cited by 105

Cited by9

Results whose statement or proof uses this declaration.