## Stream: Is there code for X?

### Topic: mem.span

#### Scott Morrison (Sep 08 2020 at 10:51):

(The linear algebra code makes me so sad...)

I have x ∈ submodule.span R S for some S : set M, and module R M.

How to I obtain a formula for x as a linear combination of finitely many elements of S? (Ideally in a way that it's then convenient to do induction on the size of that linear combination?)

#### Scott Morrison (Sep 08 2020 at 10:51):

I feel like grepping for linear combination should reveal this, but ...

#### Scott Morrison (Sep 08 2020 at 10:52):

The fact that the word "combination" doesn't even appear in linear_algebra.basic seems worrying.

#### Johan Commelin (Sep 08 2020 at 10:52):

Isn't there something like finsupp.total or something like that?

#### Markus Himmel (Sep 08 2020 at 10:53):

Does docs#submodule.span_induction help?

#### Anne Baanen (Sep 08 2020 at 10:54):

This is called docs#finsupp.mem_span_iff_total

#### Anne Baanen (Sep 08 2020 at 10:57):

finsupp.total does mention the words "linear combination" in its docstring, by the way :)

#### Scott Morrison (Sep 08 2020 at 11:03):

But even this has some business about an image of a set v '' s...

#### Scott Morrison (Sep 08 2020 at 11:04):

I have to make my set look like that? :-(

#### Scott Morrison (Sep 08 2020 at 11:06):

It seems submodule.span_induction will work smoothly for me.

#### Adam Topaz (Sep 08 2020 at 12:12):

I got frustrated with something like this a little while ago for another project I was working on, and ended up proving this

I could try to clean it up and integrate it into mathlib with a small PR if people think it is actually useful.

#### Filippo A. E. Nuccio (Oct 30 2020 at 17:21):

Has this finally got merged into mathlib?

#### Adam Topaz (Oct 30 2020 at 18:03):

No :(
It's still unclear what form of this should belong in mathlib (if at all!)

#### Adam Topaz (Oct 30 2020 at 18:04):

I guess some general stuff about linear combinations (defined as lists as in the above link) should also be added.

#### Filippo A. E. Nuccio (Oct 30 2020 at 18:46):

Ah, that's a pity. I am trying to build a proof using that every element in a product of modules is a linear combination and your file would be extremely useful.

#### Adam Topaz (Oct 30 2020 at 18:50):

I think this docs#finsupp.mem_span_iff_total is the way to do such things with what's in mathlib, as the above comments suggest.

#### Filippo A. E. Nuccio (Oct 30 2020 at 18:51):

Yes, I saw it. Your file looks much more transparent to me, though. Thanks again for the ref, at any rate.

#### Adam Topaz (Oct 30 2020 at 18:51):

Filippo A. E. Nuccio said:

Yes, I saw it. Your file looks much more transparent to me, though. Thanks again for the ref, at any rate.

I agree, of course.

#### Filippo A. E. Nuccio (Oct 31 2020 at 17:46):

Following the above discussion with @Adam Topaz , I was thinking about creating a lemma to the effect that the product of two ideals (or two R-submodules contained in a R-algebra A) consists of all linear combinations of products of an element of the first module times an element of the second module. But of course I don't want to reinvent the wheel, so I would like to double check that this does not exist already.

#### Johan Commelin (Oct 31 2020 at 18:00):

I think linear combinations need some love. I don't know exactly what, but whatever we have at the moment in mathlib is just not very intuitive to use.

#### Johan Commelin (Oct 31 2020 at 18:01):

But I don't have the time to experiment with this.

#### Johan Commelin (Oct 31 2020 at 18:01):

Probably it's not something that you get right at the first attempt. So maybe we just need several people to try things out. And hopefully it will converge to something useful.

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:02):

I see. I will write down something for the above result, then, and we'll see if it is somehow useful.

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:02):

At any rate, my impression with @Adam Topaz 's file is that it was useful and very nice. Yet (unless I misread it) it still does not immediately contain the result about products of sub-modules that I was referring to.

#### Adam Topaz (Oct 31 2020 at 18:03):

Personally I think defining linear combinations as lists (as in the above file) is very intuitive

#### Mario Carneiro (Oct 31 2020 at 18:05):

Johan Commelin said:

I think linear combinations need some love. I don't know exactly what, but whatever we have at the moment in mathlib is just not very intuitive to use.

As one of the authors of this part of the library I would be interested to know what the pain points are

#### Mario Carneiro (Oct 31 2020 at 18:06):

I think that finsupp is actually the mathematically correct way to represent the type of linear combinations, because unlike lists they have the right equality relation

#### Adam Topaz (Oct 31 2020 at 18:07):

how would you represent a linear combination where two of the vectors are the same?

#### Mario Carneiro (Oct 31 2020 at 18:08):

{v1 * (a - b)}?

#### Mario Carneiro (Oct 31 2020 at 18:09):

You can always express a linear combination as (l.map (\lam (vi, ai), finsupp.single vi ai)).sum where l is a list of vectors and coefficients that is not necessarily injective in the vi

#### Mario Carneiro (Oct 31 2020 at 18:10):

the summing of finsupps handles the job of putting all the coefficients of some fixed v into the same bucket

#### Adam Topaz (Oct 31 2020 at 18:11):

Okay. That's one point that's not intuitive for me.

#### Adam Topaz (Oct 31 2020 at 18:11):

Of course, I agree this can be done with finsupp, but I think representing them as lists is much closer to what I think of as a linear combination mathematically.

#### Mario Carneiro (Oct 31 2020 at 18:12):

The finsupp is just the normal form

#### Mario Carneiro (Oct 31 2020 at 18:12):

just like how polynomial only represents the polynomials in normal form

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:12):

In particular, as a mathematician, the set over which I sum is often "irrelevant". I fully appreciate that it cannot be really irrelevant, but my impression is that this aspect plays a major role in finsupp.

#### Mario Carneiro (Oct 31 2020 at 18:12):

if you have a list, you can sum the list

#### Adam Topaz (Oct 31 2020 at 18:13):

But two polynomials are equal if and only if their coefficients are the same, and this is not true for the finsupp representation of linear combinations

it is

#### Adam Topaz (Oct 31 2020 at 18:13):

Why is 1 * v + 0 * v the same as 1 * v ?

#### Adam Topaz (Oct 31 2020 at 18:14):

one is a linear combination of two vectors, and the other is a linear combination of one vector

#### Mario Carneiro (Oct 31 2020 at 18:14):

Okay we're clearly having a miscommunication then

probably :)

#### Mario Carneiro (Oct 31 2020 at 18:14):

that's not a linear combination of two vectors

#### Mario Carneiro (Oct 31 2020 at 18:15):

that's a linear combination of one vector

#### Adam Topaz (Oct 31 2020 at 18:15):

Oh, I would say it's a linear comb of two vectors which just so happen to be the same

#### Mario Carneiro (Oct 31 2020 at 18:15):

The thing is, the finsupp allows you to pick a more abstract notion of indexing type than just the vectors themselves

#### Mario Carneiro (Oct 31 2020 at 18:16):

In fact, this was a problem in the early versions of the linalg library that needed a major refactor

#### Adam Topaz (Oct 31 2020 at 18:16):

Oh, I thought you were identifying linear combinations with funsupp functions from the module to the ring

So did I.

#### Mario Carneiro (Oct 31 2020 at 18:16):

That depends on your use case

#### Mario Carneiro (Oct 31 2020 at 18:17):

Usually, when you have a basis, the basis vectors are themselves given by I -> V where I is an abstract indexing set

#### Adam Topaz (Oct 31 2020 at 18:17):

If you define it as a funsupp from some index type \iota to R \times M, that would be great, but I dont think what exists in mathlib right now actually does this.

#### Mario Carneiro (Oct 31 2020 at 18:17):

so you want the linear combinations to instead be I ->0 R

#### Adam Topaz (Oct 31 2020 at 18:18):

This docs#finsupp.mem_span_iff_total is a good example

#### Mario Carneiro (Oct 31 2020 at 18:19):

If you look at docs#finsupp.total (which is the "forgetful functor" from linear combinations of vectors to vectors), you will see that there is an abstract indexing type alpha

Yeah, I see now

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:20):

But what should I "normally" chose as alpha? Nat?

#### Mario Carneiro (Oct 31 2020 at 18:20):

That depends on where the vectors come from

#### Reid Barton (Oct 31 2020 at 18:20):

Is this how finsupp.total was always defined?

no

#### Mario Carneiro (Oct 31 2020 at 18:21):

It was once the way Adam said, V ->0 R

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:21):

Mario Carneiro said:

That depends on where the vectors come from

Well, in my case at hand they are all elements of a ring, I am trying to say that every element of I * J (both ideals in R) is a linear combination of things, one from I and the other from J.

#### Mario Carneiro (Oct 31 2020 at 18:22):

As in, just two things?

#### Mario Carneiro (Oct 31 2020 at 18:22):

For that you don't need linear combinations at all, you just write a * x + b * y

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:23):

Well, no, they are of the form $\sum _{i \in A} x_i * y_i$ for some (finite) $A$

#### Adam Topaz (Oct 31 2020 at 18:23):

That's the thing, with this finsupp formulation it's so cumbersome to state facts like "every element in the span of a set is a linear combination of the elements of the set"

#### Mario Carneiro (Oct 31 2020 at 18:24):

you can still do that though?

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:24):

Same thing for the generic element of $M\otimes N$.

#### Mario Carneiro (Oct 31 2020 at 18:24):

if you really want to put in I = V you can

#### Mario Carneiro (Oct 31 2020 at 18:24):

@Filippo A. E. Nuccio what's the type of A

#### Mario Carneiro (Oct 31 2020 at 18:25):

Oh I understand now

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:25):

Mario Carneiro said:

Filippo A. E. Nuccio what's the type of A

A finite subset of $\mathbb{N}$, typically (at least in my mind, I can come up with more complicated things; for instance I can index them over all elements in $R$)

#### Mario Carneiro (Oct 31 2020 at 18:26):

I think the indexing set in your example is ↑I × ↑J

#### Mario Carneiro (Oct 31 2020 at 18:26):

if you have a #mwe I can make something that typechecks

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:28):

Mario Carneiro said:

I think the indexing set in your example is ↑I × ↑J

Possibly; but a part from being potentially very huge it seems hard to compare it with elements in $I*J$ *which I can see as $\mathrm{Span}(I*J)$ and would be indexed on $I*J$ (product of ideals, not cartesian product).

#### Mario Carneiro (Oct 31 2020 at 18:29):

being potentially very huge

It's just the index set, the range of possibilities for the vectors. These are usually infinite

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:29):

For the https://leanprover-community.github.io/mwe.html: Well, I don't have it yet... I was figuring out how to prove my claim that every element of the product can be written in that way, and got lost in finsupp (with all the due respect, as I would have been totally incapable of coming up with anything, so no criticism at all is meant here)

#### Mario Carneiro (Oct 31 2020 at 18:30):

I mean if you can provide something with the context of your problem

#### Mario Carneiro (Oct 31 2020 at 18:30):

like imports and variables

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:31):

Sure, give me a sec.

#### Reid Barton (Oct 31 2020 at 18:31):

docs#submodule.span_smul_span is pretty close to your statement

#### Reid Barton (Oct 31 2020 at 18:32):

since if I : ideal R then I = ideal.span (I : set R)

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:32):

Reid Barton said:

docs#submodule.span_smul_span is pretty close to your statement

Indeed, it is. I was starting from there to try to construct the proof, but got a bit lost and begun wondering if what I was doing was worth it.

#### Mario Carneiro (Oct 31 2020 at 18:32):

Yeah I was going to point out next that this combination doesn't look very linear because there is no coefficient

#### Reid Barton (Oct 31 2020 at 18:33):

You don't need a coefficient because $2 \ge 1$--but it might be better to allow one anyways for uniformity

#### Reid Barton (Oct 31 2020 at 18:34):

If you multiply together n ideals then you need to allow a coefficient from R when n=0

#### Mario Carneiro (Oct 31 2020 at 18:36):

In that case, I would want to go for a more inductive formulation: if I = ideal.span (set.range a) and J = ideal.span (set.range b) then I * J = ideal.span (set.range (\lam (i,j), a i * b j)

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:37):

This seems very nice, and I can take a = (I : set R) and b = (J : set R)

#### Reid Barton (Oct 31 2020 at 18:37):

Filippo, I'm curious what you intend to do next after applying this statement about linear combinations--normally I think the span formulation would be better

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:39):

Reid Barton said:

Filippo, I'm curious what you intend to do next after applying this statement about linear combinations--normally I think the span formulation would be better

Well, I'm trying to prove the statement that for an invertible module M, M * (1 / M ) \le 1. Which is immediate if I can take an element in M * 1/M and write it as a linear combination $\sum x_i y_i$ with $x_i\in M$ and $y_i \in 1/M$, so that $x_iy_i\in R$ by definition of $1/M$

#### Reid Barton (Oct 31 2020 at 18:39):

Then you don't want to deal with linear combinations explicitly

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:40):

Well, what do you mean by "explicitely"?

#### Reid Barton (Oct 31 2020 at 18:40):

just use the fact that if M is an R-submodule of something and S \sub M then span S \sub M

#### Reid Barton (Oct 31 2020 at 18:41):

I mean you don't need to mention things like finsupp.total

#### Johan Commelin (Oct 31 2020 at 18:41):

apply submodule.span_le

#### Johan Commelin (Oct 31 2020 at 18:41):

assuming that M * (1/M) is defined as a span (which I think it is).

#### Reid Barton (Oct 31 2020 at 18:42):

You can use the "universal algebra-style" characterization of the span (i.e. linear combinations) of S as the smallest ideal/submodule containing S

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:43):

Well, that's what I was trying to do, but could not understand how to use the definition of the product to come up with elements.

#### Filippo A. E. Nuccio (Oct 31 2020 at 18:44):

instance : has_mul (submodule R A) :=
⟨λ M N, ⨆ s : M, N.map $algebra.lmul R A s.1⟩  #### Reid Barton (Oct 31 2020 at 18:45): I agree the definition of the product is less convenient (though you could presumably do a similar argument with it) #### Mario Carneiro (Oct 31 2020 at 18:45): docs#ideal.mul_le #### Reid Barton (Oct 31 2020 at 18:45): i.e., it's a ⨆ so to prove it's \le 1 means to prove each summand is \le 1 #### Johan Commelin (Oct 31 2020 at 18:45): Mario Carneiro said: docs#ideal.mul_le This doesn't work, I guess. because it's not about ideals. #### Mario Carneiro (Oct 31 2020 at 18:46): What is the type of anything? #### Filippo A. E. Nuccio (Oct 31 2020 at 18:46): Exactly, it's about submodules in a R-algebra #### Mario Carneiro (Oct 31 2020 at 18:46): #mwe please #### Filippo A. E. Nuccio (Oct 31 2020 at 18:46): both are submodules A R #### Filippo A. E. Nuccio (Oct 31 2020 at 18:46): Mario Carneiro said: #mwe please Working on it... #### Johan Commelin (Oct 31 2020 at 18:46): Can you use extract_goal to create the lemma that you want to prove? #### Mario Carneiro (Oct 31 2020 at 18:47): docs#submodule.mul_le #### Johan Commelin (Oct 31 2020 at 18:47): Then I can post a 5-line proof, and Mario will golf it into a 42-character proof #### Kevin Buzzard (Oct 31 2020 at 18:47): I was about to say the same as Reid. Consider how one might define the subgroup generated by a subset X of an abelian group A. I can think of three ways to do it. 1) intersection of all the subgroups of A that contain X 2) custom inductive type. Elements of X are in, 0 is in, sum of two elements which are in is in, negation of an element which is in, is in 3) something involving the image of some finsupp #### Filippo A. E. Nuccio (Oct 31 2020 at 18:49): Johan Commelin said: Then I can post a 5-line proof, and Mario will golf it into a 42-character proof Is this what you mean? import algebra.algebra.basic example {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] {I : submodule R A} : I * 1 / I ≤ 1 := begin admit, end  #### Mario Carneiro (Oct 31 2020 at 18:49): imports? #### Kevin Buzzard (Oct 31 2020 at 18:49): But what in practice does one want from these things? When I first learnt about inductive types etc I got super-excited about the idea of (2) and how the recursor was generated automatically and looked mathematically useful #### Kevin Buzzard (Oct 31 2020 at 18:50): But now more and more I am realising the power of (1). It's quite pleasant to prove things about definition (1) #### Filippo A. E. Nuccio (Oct 31 2020 at 18:51): But can you work with them "explicitely"? Or at least, would you admit it takes a bit to change our "usual" elements-based proofs into that language? #### Filippo A. E. Nuccio (Oct 31 2020 at 18:51): Which, of course, I am willing to...but still trying to learn. #### Mario Carneiro (Oct 31 2020 at 18:51): The idea behind having a big API is so that you can use any of (1) (2) or (3) depending on your current use case #### Kevin Buzzard (Oct 31 2020 at 18:51): You can construct the recursor yourself #### Filippo A. E. Nuccio (Oct 31 2020 at 18:52): What do you mean? #### Reid Barton (Oct 31 2020 at 18:53): right, in practice you want whichever one of the three is the most convenient in a given situation. Textbooks in (say) commutative algebra will often use (3) everywhere even when using (1) is logically more efficient, because it costs so little to write $\sum_i x_i y_i$ on a page #### Mario Carneiro (Oct 31 2020 at 18:53): Your #mwe doesn't work #### Mario Carneiro (Oct 31 2020 at 18:53): Try copying it into a new file #### Mario Carneiro (Oct 31 2020 at 18:53): import algebra.algebra.operations universes u v example {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] {I : submodule R A} : I * 1 / I ≤ 1 := begin admit, end  #### Johan Commelin (Oct 31 2020 at 18:54): import algebra.algebra.operations example {R A : Type*} [comm_semiring R] [comm_semiring A] [algebra R A] {I : submodule R A} : I * (1 / I) ≤ 1 := begin rw submodule.mul_le, intros m hm n hn, rw [submodule.mem_div_iff_forall_mul_mem] at hn, rw mul_comm, exact hn m hm, end  #### Johan Commelin (Oct 31 2020 at 18:54): 5 lines, as promised #### Johan Commelin (Oct 31 2020 at 18:54): Note that I changed the import, and added (..) around 1 / I #### Filippo A. E. Nuccio (Oct 31 2020 at 18:54): Great, I tried for the whole morning... :silence: #### Kevin Buzzard (Oct 31 2020 at 18:55): Then inspect the proof carefully and figure out what you were missing #### Filippo A. E. Nuccio (Oct 31 2020 at 18:55): Sure, I will. Thanks. #### Kevin Buzzard (Oct 31 2020 at 18:55): As a beginner I would always unfold everything #### Kevin Buzzard (Oct 31 2020 at 18:56): And I have learnt more recently that whilst this teaches you a lot about how lean and type theory works #### Kevin Buzzard (Oct 31 2020 at 18:56): It is almost never the optimal way to prove things, because the way to prove things is to use the API #### Kevin Buzzard (Oct 31 2020 at 18:57): The way to prove things is to prove them mathematically and then to try and translate your 5 line maths proof into Lean #### Filippo A. E. Nuccio (Oct 31 2020 at 18:58): Well, that's what I was trying, but got stuck with my elements-based proof, as Reid said. #### Filippo A. E. Nuccio (Oct 31 2020 at 18:58): But I see your point, thanks. #### Kevin Buzzard (Oct 31 2020 at 18:59): My PhD student Ashvni made a short PR today about subalgebras and submodules and I think her proof was six lines long, and also used submodule.mul_le #### Kevin Buzzard (Oct 31 2020 at 19:00): Things like mul_le are great examples of the tricks that you can do when working with products of ideals #### Johan Commelin (Oct 31 2020 at 19:00): import algebra.algebra.operations open submodule example {R A : Type*} [comm_semiring R] [comm_semiring A] [algebra R A] {I : submodule R A} : I * (1 / I) ≤ 1 := mul_le.2$ λ m hm n hn, (mul_comm n m) ▸ (mem_div_iff_forall_mul_mem.2 hn m hm)


80 chars... :worried:

#### Kevin Buzzard (Oct 31 2020 at 19:00):

The triangle works!

#### Reid Barton (Oct 31 2020 at 19:02):

4 of those ()s look unnecessary

#### Reid Barton (Oct 31 2020 at 19:02):

which is all of them I guess

#### Johan Commelin (Oct 31 2020 at 19:02):

Ooh, I don't need the parens... and I can rename hm and hn to h and H.

That's 72 chars

#### Mario Carneiro (Oct 31 2020 at 19:02):

example {R A : Type*} [comm_semiring R] [comm_semiring A] [algebra R A] {I : submodule R A} :
I * (1 / I) ≤ 1 :=
mul_le.2 $by finish [mem_div_iff_forall_mul_mem]  #### Johan Commelin (Oct 31 2020 at 19:02): Is that 42? #### Mario Carneiro (Oct 31 2020 at 19:02): 49 #### Johan Commelin (Oct 31 2020 at 19:03): (deleted) #### Mario Carneiro (Oct 31 2020 at 19:03): by finish [mul_le, mem_div_iff_forall_mul_mem] is 47 #### Johan Commelin (Oct 31 2020 at 19:04): and slow... #### Johan Commelin (Oct 31 2020 at 19:04): I guess we need to rename mem_div_iff_forall_mul_mem to something shorter :rofl: #### Mario Carneiro (Oct 31 2020 at 19:05): rfl #### Mario Carneiro (Oct 31 2020 at 19:05): I think it could just be mem_div_iff since it's the definition #### Johan Commelin (Oct 31 2020 at 19:06): That would even bring it below chars #### Johan Commelin (Oct 31 2020 at 19:07): What would happen if J and Lean had a child? #### Mario Carneiro (Oct 31 2020 at 19:07): L #### Johan Commelin (Oct 31 2020 at 19:07): We'd have seriously weird unicode symbols for tactics like finish #### Filippo A. E. Nuccio (Oct 31 2020 at 19:10): Mario Carneiro said: example {R A : Type*} [comm_semiring R] [comm_semiring A] [algebra R A] {I : submodule R A} : I * (1 / I) ≤ 1 := mul_le.2$ by finish [mem_div_iff_forall_mul_mem]


#### Johan Commelin (Oct 31 2020 at 19:11):

It just means "put parentheses around everything that follows me".

#### Johan Commelin (Oct 31 2020 at 19:12):

It doesn't even save us a character. But if you use it multiple times, then it avoids ending the line with )))))

Ah, ok!

#### Filippo A. E. Nuccio (Oct 31 2020 at 19:13):

AH, go(ogle)t it!

#### Kevin Buzzard (Oct 31 2020 at 19:13):

Multiplication has higher priority than addition so we all know what a+b*c means

Well, to see

#### Kevin Buzzard (Oct 31 2020 at 19:16):

https://xenaproject.wordpress.com/2019/01/20/a-word-on-bidmas/

#### Kevin Buzzard (Oct 31 2020 at 19:17):

mul_le is the universal property of product of ideals. If you use the universal property you don't have to get your hands dirty with elements

Right.

#### Filippo A. E. Nuccio (Oct 31 2020 at 19:20):

I'll have stuff to work on during my locked-down Sunday - thanks!

#### Mario Carneiro (Oct 31 2020 at 19:22):

Kevin Buzzard said:

\$ literally means "do nothing, with priority 1" ie very low

It doesn't mean "do nothing", it means application, although adjacency (i.e. nothing) is also notation for application

#### Kevin Buzzard (Nov 04 2020 at 13:51):

This issue has come up again -- @Ashvni Narayanan has run into it. The proof that if all nonzero ideals are invertible in a comm ring R then R is Noetherian goes like this: Say $I$ is a non-zero ideal. Then $I\times I^{-1}=1$ so there exists $a_i\in I$ and $b_i\in I^{-1}$ such that $\sum_i a_i b_i = 1$ (a finite sum); multiplying both sides by an element of $I$ now shows that the $a_i$ generate $I$.

#### Kevin Buzzard (Nov 04 2020 at 13:52):

This time I don't immediately see how to use mul_le to get around this.

#### Kevin Buzzard (Nov 04 2020 at 16:29):

OK I think that there is a very natural proof of what Ashvni needs if we had the following weaker theorem: if $R$ is a ring and $M$ is an $R$-module (or semiwhathaveyou) and $S\subseteq M$ is a subset, and if $x$ is in span S then there's a finite subset $S'\subseteq S$ such that $x$ is in span S'. Do we have _this_? I can't spot it in mathlib.

#### Kevin Buzzard (Nov 04 2020 at 16:35):

This shouldn't be hard to prove using span_induction. Let's say this isn't in mathlib. Should we put in the version which has S' a finset or the version with S' a set which is also finite?

#### Kevin Buzzard (Nov 04 2020 at 17:06):

lemma submodule.mem_span_finset_of_mem_span (S : set M) (x : M) (hx : x ∈ span R S) :
∃ S' : finset M, (↑S' : set M) ⊆ S ∧ x ∈ span R (↑S' : set M) :=


I can prove this; is this the right form for mathlib?

#### Mario Carneiro (Nov 04 2020 at 18:54):

I would suggest using a finite set, because you only ever use it in the form (↑S' : set M). If the user wants it to be in that form then they can apply the theorem to unfold finite into that

#### Kevin Buzzard (Nov 04 2020 at 22:52):

Thanks. The proof was also nothing but coercions and I needed classical to take a union of two finsets (although perhaps I'll also need it to take a union of two finite sets)

Last updated: May 19 2021 at 00:40 UTC