Theorems · Theorem · number theory
Pell.pellZd_succ_succ
∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.pellZd a1 (n + 2) + Pell.pellZd a1 n = ↑(2 * a) * Pell.pellZd a1 (n + 1)- Defined in
- Mathlib.NumberTheory.PellMatiyasevic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 43 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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
- MulZeroClass.mul_zeroproof · cited by 2,091
- MulZeroClass.zero_mulproof · cited by 1,625
- pow_oneproof · cited by 894
- Nat.cast_mulproof · cited by 309
- Zsqrtdstatement · cited by 105
- Zsqrtd.improof · cited by 54
- Zsqrtd.reproof · cited by 53
- Pell.xnproof · cited by 44
- Pell.ynproof · cited by 37
- Zsqrtd.extproof · cited by 18
Cited by1
Results whose statement or proof uses this declaration.
- Pell.xy_succ_succproof · cited by 2