Theorems · Theorem · number theory

LinearRecurrence.eq_mk_of_is_sol_of_eq_init

∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R) {u : ℕ → R} {init : Fin E.order → R},
  E.IsSolution u → (∀ (n : Fin E.order), u ↑n = init n) → ∀ (n : ℕ), u n = E.mkSol init n

If u is a solution to E and init designates its first E.order values, then ∀ n, u n = E.mkSol init n.

Defined in

Mathlib.Algebra.LinearRecurrence

Cited by

1 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiring