Linear combinations stay in a submodule

Stream: Is there code for X?

[Sophie Morel]

Is there a lemma in the library that says that a linear combination of elements of a submodule is still in the submodule ? I wanted to use that result when doing one of the lftcm2020 linear algebra exercises, but I only found submodule.sum_mem that works for a sum, and submodule.smul_mem that works for a scalar product. (There's a related result called finsupp.mem_span_iff_total that says that the span of a family if the set of its linear combinations, but you'd need to combine it with the fact that a submodule is the span of the family of all its elements. Also, it assumes that the base semiring is a ring for some reason, which I don't think is necessary.) Anyway, I ended up adding this in my local copy of module.lean :

lemma linear_combination_mem {t : finset ι} {f : ι → M} (r : ι → R) :
(∀ c ∈ t, f c ∈ p) → (∑ i in t, r i • f i) ∈ p :=
λ hyp, submodule.sum_mem _ (λ i hi, submodule.smul_mem _ _ (hyp i hi))

(Just after smul_mem_iff' on line 504. Here R is a semiring, M is a semimodule over R, ι is a type, p is a submodule of M.)

[Anne Baanen]

I don't believe this lemma existed yet - the model solution uses a combination of sum_mem and smul_mem as in your proof for linear_combination_mem.

[Kevin Buzzard]

@Sophie Morel this would be a helpful PR and if you golf it a bit by changing : (∀ c ∈ t, f c ∈ p) → to (hyp : ∀ c ∈ t, f c ∈ p) : and deleting λ hyp, ("move as much as possible to the left of the colon") then it looks mathlib-ready. Do you have push rights to non-master branches of mathlib? If you don't know, then you probably don't -- what is your github login?

[Johan Commelin]

@Sophie Morel Also, small tip: if you want syntax highlighting in your Zulip posts, then you can use #backticks like so

```
lean code goes here
```

[Sophie Morel]

@Johan Commelin Thanks !

[Sophie Morel]

@Kevin Buzzard, do you mean something like this :

lemma linear_combination_mem {t : finset ι} {f : ι → M} (r : ι → R)
    (hyp : ∀ c ∈ t, f c ∈ p) : (∑ i in t, r i • f i) ∈ p :=
submodule.sum_mem _ (λ i hi, submodule.smul_mem  _ _ (hyp i hi))

My github login is smorel394, and I am pretty confident that I don't have push rights to anything.

[Kevin Buzzard]

@maintainers could Sophie have push rights to non-master branches of mathlib?

[Kevin Buzzard]

Yes that looks great. A three line PR adding a missing lemma in an appropriate place is the best kind of PR. The maintainers have a better eye than I do however

[Chris Hughes]

Kevin Buzzard said:

@maintainers could Sophie have push rights to non-master branches of mathlib?

Done

[Sophie Morel]

@Kevin Buzzard @Chris Hughes Thank ! I'll try to figure out the git stuff after dinner. (Scott told me about this page https://leanprover-community.github.io/contribute/index.html, so I should be ok.)