solSpace_rank — Mathlib

English

The dimension of the solution space equals the order of the recurrence, i.e., solSpace is of dimension E.order.

Русский

Размерность пространства решений равна порядку рекуррентности: solSpace имеет размерность order(E).

LaTeX

$$Module.rank R E.solSpace = E.order$$

Lean4

/-- The dimension of `E.solSpace` is `E.order`. -/
theorem solSpace_rank : Module.rank R E.solSpace = E.order :=
  letI := nontrivial_of_invariantBasisNumber R
  @rank_fin_fun R _ _ E.order ▸ E.toInit.rank_eq

Похожие утверждения