solSpace — Mathlib

English

The solution space of E, viewed as an R-submodule of all sequences, has dimension equal to the order of E.

Русский

Пространство решений E, рассматриваемое как подмодуль над R внутри множества последовательностей, имеет размерность, равную порядку E.

LaTeX

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

Lean4

/-- The space of solutions of `E`, as a `Submodule` over `R` of the module `ℕ → R`. -/
def solSpace : Submodule R (ℕ → R) where
  carrier := {u | E.IsSolution u}
  zero_mem' n := by simp
  add_mem' {u v} hu hv n := by simp [mul_add, sum_add_distrib, hu n, hv n]
  smul_mem' a u hu n := by simp [hu n, mul_sum]; congr; ext; ac_rfl

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