# Zulip Chat Archive

## Stream: maths

### Topic: trivial submodules

#### Thomas Browning (Jun 23 2020 at 23:28):

If I understand things correctly, `submodule R M`

is a type consisting of submodules of M. Is there a name for the zero submodule and the whole submodule? For example, how you would make this code work?

```
import algebra.module
definition simple (𝕜 : Type*) [field 𝕜] (V : Type*) [add_comm_group V] [module 𝕜 V] :=
(∀ W : submodule 𝕜 V, /-(W=0) ∨ (W=V)-/)
```

#### Chris Hughes (Jun 23 2020 at 23:29):

\bot and \top

#### Thomas Browning (Jun 23 2020 at 23:32):

Maybe I need to import some mathlib file, but lean doesn't know that `submodule 𝕜 V`

has \bot and \top.

```
definition simple (𝕜 : Type*) [field 𝕜] (V : Type*) [add_comm_group V] [module 𝕜 V] :=
(∀ W : submodule 𝕜 V, (W=⊥) ∨ (W=⊤))
```

#### Chris Hughes (Jun 23 2020 at 23:32):

I think `import linear_algebra.basic`

should be enough.

#### Nico Courts (Jun 23 2020 at 23:33):

Yup! That did it for me. Thanks!

#### Kevin Buzzard (Jun 24 2020 at 06:16):

The decision was made to use lattice notation for bundled types like this and initially I was concerned that it would make it hard for newcomers, but given that mathematicians have so many different notations for the lattice operations in different circumstances I eventually ended up realising that teaching mathematicians about lattice notation might actually be a better idea. Sum of submodules is `\lub`

and intersection is`\glb`

and these are the simp normal forms

Last updated: May 18 2021 at 08:14 UTC