mem_ideal_span_range_iff_exists_finsupp

English

For finite α, an element x ∈ R lies in span(Set.range v) iff there exists c : α →₀ R with (c.sum (λ i a, a * v i)) = x.

Русский

Пусть α конечен. Тогда элемент x ∈ R принадлежит span(Set.range v), если существует c : α →₀ R such that ∑ i (c i) · v i = x.

LaTeX

$$$x \\in \\operatorname{span}(\\operatorname{Set.range} v) \\\\iff \\exists c : \\alpha \\rightarrow_{0} R, (c.sum \\; (\\lambda i\\ a. a \\cdot v(i))) = x$$$

Lean4

theorem mem_ideal_span_range_iff_exists_finsupp {x : R} {v : α → R} :
    x ∈ Ideal.span (Set.range v) ↔ ∃ c : α →₀ R, (c.sum fun i a => a * v i) = x :=
  Finsupp.mem_span_range_iff_exists_finsupp

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