Integer combinations in the additive closure of a family

This file records when an integer combination ∑ i, c i • v i of a finite family v lies in the additive submonoid generated by the family: when all coefficients are nonnegative, and, up to sign, when all coefficients have the same sign. These are the integer-coefficient companions of AddSubmonoid.mem_closure_range_iff_of_fintype, which describes the closure through natural coefficients.

Main results

• TauCeti.sum_smul_mem_closure: a combination with nonnegative integer coefficients lies in the additive closure of the family.
• TauCeti.sum_smul_mem_or_neg_mem_closure: a combination whose coefficients all have the same sign lies in the additive closure of the family, or its negative does.

theorem TauCeti.sum_smul_mem_closure {κ : Type u_1} {M : Type u_2} [Fintype κ] [SubtractionCommMonoid M] (v : κ → M) (c : κ → ℤ) (hc : ∀ (i : κ), 0 ≤ c i) : ∑ i : κ, c i • v i ∈ AddSubmonoid.closure (Set.range v)

A combination of a finite family with nonnegative integer coefficients lies in the additive closure of the family.

theorem TauCeti.sum_smul_mem_or_neg_mem_closure {κ : Type u_1} {M : Type u_2} [Fintype κ] [SubtractionCommMonoid M] (v : κ → M) (c : κ → ℤ) (hc : (∀ (i : κ), 0 ≤ c i) ∨ ∀ (i : κ), c i ≤ 0) : ∑ i : κ, c i • v i ∈ AddSubmonoid.closure (Set.range v) ∨ -∑ i : κ, c i • v i ∈ AddSubmonoid.closure (Set.range v)

A combination of a finite family whose integer coefficients all have the same sign lies in the additive closure of the family, or its negative does.