Theorems · Definition · number theory
LinearRecurrence.solSpace
{R : Type u_1} → [inst : CommSemiring R] → LinearRecurrence R → Submodule R (ℕ → R)The space of solutions of E, as a Submodule over R of the module ℕ → R.
- Defined in
- Mathlib.Algebra.LinearRecurrence
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Submodulestatement · cited by 7,192
- Set.ofPredproof · cited by 6,101
- LinearRecurrencestatement and proof · cited by 21
- LinearRecurrence.IsSolutionproof · cited by 11
Cited by8
Results whose statement or proof uses this declaration.
- LinearRecurrence.basisstatement · cited by 4
- LinearRecurrence.eq_iff_eqOn_range_orderproof · cited by 2
- LinearRecurrence.toInitstatement and proof · cited by 1
- Real.coe_fib_eq'proof · cited by 1
- LinearRecurrence.is_sol_iff_mem_solSpacestatement · cited by 1
- LinearRecurrence.repr_basis_applystatement and proof · cited by 0
- LinearRecurrence.repr_basis_eqstatement and proof · cited by 0
- LinearRecurrence.solSpace_rankstatement · cited by 0