Theorems · Definition · number theory
LinearRecurrence.IsSolution
{R : Type u_1} → [inst : CommSemiring R] → LinearRecurrence R → (ℕ → R) → PropWe say that a sequence u is solution of LinearRecurrence order coeffs when we have
u (n + order) = ∑ i : Fin order, coeffs i * u (n + i) for any n.
- Defined in
- Mathlib.Algebra.LinearRecurrence
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Finset.sumproof · cited by 5,195
- Finset.univproof · cited by 3,473
- LinearRecurrencestatement and proof · cited by 21
- LinearRecurrence.orderproof · cited by 17
- LinearRecurrence.coeffsproof · cited by 7
Cited by12
Results whose statement or proof uses this declaration.
- LinearRecurrence.solSpaceproof · cited by 6
- LinearRecurrence.eq_iff_eqOn_range_orderstatement and proof · cited by 2
- LinearRecurrence.geom_sol_iff_root_charPolystatement and proof · cited by 2
- Real.fib_isSol_fibRecstatement and proof · cited by 1
- Real.coe_fib_eq'proof · cited by 1
- Real.geom_goldenConj_isSol_fibRecstatement · cited by 1
- Real.geom_goldenRatio_isSol_fibRecstatement · cited by 1
- LinearRecurrence.eq_mk_of_is_sol_of_eq_initstatement and proof · cited by 1
- LinearRecurrence.is_sol_iff_mem_solSpacestatement · cited by 1
- LinearRecurrence.sol_eq_of_eq_initstatement · cited by 0
- LinearRecurrence.eq_mk_of_is_sol_of_eq_init'statement and proof · cited by 0
- LinearRecurrence.is_sol_mkSolstatement · cited by 0