# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Multiplication of sets

#### Ashvni Narayanan (Nov 09 2020 at 17:54):

I have

```
↑q' * ↑q ⊆ {1}
```

where `q`

and `q'`

are submodules, and the `coe`

lifts them to sets. I want to turn it into

```
↑(q' * q) ⊆ {1}
```

I can't seem to find anything of the form `coe_mul`

. Any help is appreciated, thank you!

Edit : It turns out that Lean automatically converts `↑(q' * q)`

into `↑q' * ↑q`

. However, I don't see why this is true for submodules.

#### Eric Wieser (Nov 09 2020 at 17:55):

In this case Ithink you can just use `change ↑(_ * _) ⊆ _`

and lean will rewrite along definitions for you

#### Adam Topaz (Nov 09 2020 at 17:56):

Can you provide a #mwe ?

#### Adam Topaz (Nov 09 2020 at 17:57):

What is the multiplication of submodules? (I assume these are fractional ideals, or something?)

#### Ashvni Narayanan (Nov 09 2020 at 17:58):

Eric Wieser said:

In this case Ithink you can just use

`change ↑(_ * _) ⊆ _`

and lean will rewrite along definitions for you

It remains the same..

#### Ashvni Narayanan (Nov 09 2020 at 18:00):

Ashvni Narayanan said:

Eric Wieser said:

In this case Ithink you can just use

`change ↑(_ * _) ⊆ _`

and lean will rewrite along definitions for youIt remains the same..

If I write it as `((q' * q) : set _) ⊆ _ `

, it remains unchanged, however it gives me an error if I use `↑(q' * q) ⊆ {1}`

instead (I presume that this is because `coe`

is unspecified in this case).

#### Reid Barton (Nov 09 2020 at 18:08):

I think you want `((q' * q) : submodule _ _)`

, perhaps with a second cast to `set _`

if required

#### Ashvni Narayanan (Nov 09 2020 at 18:08):

Adam Topaz said:

Can you provide a #mwe ?

This isn't an mwe, but it is what I am working with.

#### Reid Barton (Nov 09 2020 at 18:08):

(Or `(q' * q : submodule _ _)`

)

#### Kevin Buzzard (Nov 09 2020 at 18:18):

If there is a multiplication defined on `set X`

where X is an R-algebra then it will presumably be pointwise multiplication, and hence will not agree with multiplication of submodules, which will be the submodule generated by the set multiplication

#### Ashvni Narayanan (Nov 09 2020 at 19:14):

I managed to get rid of subsets and am working in submodules. Thank you!

#### Eric Wieser (Nov 09 2020 at 20:55):

I'm running into something very similar now - is there a lemma like

```
lemma mul_subset_closure {A : Type*} [monoid A] (s : set A) : s * s ⊆ submonoid.closure s :=
begin
rw set.subset_def,
intros x hx,
rw submonoid.mem_coe,
obtain ⟨p, q, hp, hq, rfl⟩ := set.mem_mul.mp hx,
exact submonoid.mul_mem _ (submonoid.subset_closure hp) (submonoid.subset_closure hq),
end
```

somewhere in mathlib? If not, is that a suitable name?

#### Floris van Doorn (Nov 09 2020 at 23:06):

I would use this:

```
import algebra.module.submodule algebra.pointwise
open set
namespace submonoid
lemma mul_subset {M : Type*} [monoid M] {s t : set M} {S : submonoid M}
(hs : s ⊆ S) (ht : t ⊆ S) : s * t ⊆ S :=
by { rintro _ ⟨p, q, hp, hq, rfl⟩, exact submonoid.mul_mem _ (hs hp) (ht hq) }
lemma mul_subset_closure {A : Type*} [monoid A] {s t u : set A}
(hs : s ⊆ u) (ht : t ⊆ u) : s * t ⊆ submonoid.closure u :=
mul_subset (subset.trans hs submonoid.subset_closure) (subset.trans ht submonoid.subset_closure)
end submonoid
```

If you also want the lemma you mentioned, I would call it `mul_self_subset_closure`

.

#### Floris van Doorn (Nov 09 2020 at 23:07):

To answer your question explicitly: no, I don't think these lemmas are in mathlib.

#### Eric Wieser (Nov 09 2020 at 23:09):

Nice generalizations, thanks

#### Eric Wieser (Nov 09 2020 at 23:11):

Would you be willing to PR those, or would you prefer to leave that to me?

#### Floris van Doorn (Nov 09 2020 at 23:27):

I did it: #4960

Last updated: May 16 2021 at 05:21 UTC