## Stream: maths

### Topic: submodule.span or ideal.span?

#### Kevin Buzzard (Jul 07 2020 at 12:24):

In ring_theory.principal_ideal_domain the lemma is_maximal_of_irreducible has the conclusion that submodule.span R {p} is maximal. But there are no modules in sight, it's just rings. Why is submodule.span used when ideal.span could be used? Of course they're defeq, but is there a reason to prefer one over the other? Is there a "simp normal form" for ideals, and this normal form is that they are submodules?

#### Johan Commelin (Jul 07 2020 at 12:47):

I dunno... I would just change it to ideal.span if that's convenient.

#### Kevin Buzzard (Jul 07 2020 at 13:03):

I don't need to change it, the reason I'm asking is that I'm writing another lemma about an ideal generated by an element of a DVR and I'm trying to figure out how to state it

#### Chris Hughes (Jul 07 2020 at 14:12):

It's probably because it's old and ideal.span didn't exist at that point.

Last updated: May 12 2021 at 08:14 UTC