Theorem LinearRecurrence.mkSol_injective

Modification history

2026-04-16 22:32
Mathlib/Algebra/LinearRecurrence.lean
feat(Algebra/LinearRecurrence): define a standard basis for the solution space of a linear recurrence (#35285) …
Added LinearRecurrence.mkSol_injectiveView on Github →