Theorems · Theorem · number theory

LinearRecurrence.sol_eq_of_eq_init

Deprecated since 2026-04-16Use LinearRecurrence.eq_iff_eqOn_range_order instead.

∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R) (u v : ℕ → R),
  E.IsSolution u → E.IsSolution v → (u = v ↔ Set.EqOn u v ↑(Finset.range E.order))

Alias of LinearRecurrence.eq_iff_eqOn_range_order. Two solutions are equal iff their initial conditions are equal.

Defined in

Mathlib.Algebra.LinearRecurrence

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiring