## 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)-/)


\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