English
Let E be a LinearRecurrence over a commutative semiring R. A sequence u: N → R is a solution of E if, for every n, u(n+order) equals the sum of the coefficients times the corresponding previous terms: u(n+order) = ∑ i : Fin order, E.coeffs i · u(n+i).
Русский
Пусть E — линейная рекуррентность над коммутативным полем R. Последовательность u: ℕ → R называется решением E, если для всякого n выполняется u(n+order) = ∑ i : Fin(order) E.coeffs i · u(n+i).
LaTeX
$$$\text{IsSolution}(u) := \forall n, u(n+E.order) = \sum_{i : Fin\ E.order} E.coeffs\ i \cdot u(n+i)$$$
Lean4
/-- We 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`. -/
def IsSolution (u : ℕ → R) :=
∀ n, u (n + E.order) = ∑ i, E.coeffs i * u (n + i)
