Commit 2026-04-16 22:32 c60a4d0e

View on Github →

feat(Algebra/LinearRecurrence): define a standard basis for the solution space of a linear recurrence (#35285) Also mkSol is injective.

Estimated changes

Modified Mathlib/Algebra/LinearRecurrence.lean

added def LinearRecurrence.basis

added theorem LinearRecurrence.eq_iff_eqOn_range_order

added theorem LinearRecurrence.mkSol_injective

added theorem LinearRecurrence.repr_basis_apply

added theorem LinearRecurrence.repr_basis_eq

modified theorem LinearRecurrence.solSpace_rank

deleted theorem LinearRecurrence.sol_eq_of_eq_init

Modified Mathlib/NumberTheory/Real/GoldenRatio.lean