submodule.span or ideal.span?

Stream: maths

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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