Commit 2023-04-11 12:30 d98ece28

View on Github →

feat: port Algebra.LinearRecurrence (#3380)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/LinearRecurrence.lean

added def LinearRecurrence.IsSolution

added def LinearRecurrence.charPoly

added theorem LinearRecurrence.eq_mk_of_is_sol_of_eq_init'

added theorem LinearRecurrence.eq_mk_of_is_sol_of_eq_init

added theorem LinearRecurrence.geom_sol_iff_root_charPoly

added theorem LinearRecurrence.is_sol_iff_mem_solSpace

added theorem LinearRecurrence.is_sol_mkSol

added def LinearRecurrence.mkSol

added theorem LinearRecurrence.mkSol_eq_init

added def LinearRecurrence.solSpace

added theorem LinearRecurrence.solSpace_rank

added theorem LinearRecurrence.sol_eq_of_eq_init

added def LinearRecurrence.toInit

added def LinearRecurrence.tupleSucc

added structure LinearRecurrence