Ideal API duplicated

Stream: mathlib4

[Artie Khovanov]

I noticed the Submodule operations simplify to the (defeq) Ideal operations when the module is equal to the underlying ring. This means we can't use tactics like simp or aesop to make use of the much more complete Submodule API when proving membership in an Ideal. Of course, I could just copy the lemmas across, but that would add duplication. Given Ideal is just meant to be an abbrev, is this duplication intentional, and how can it be solved?

[Andrew Yang]

I’d say the current approach is just to duplicate.

[Artie Khovanov]

hm OK

[Eric Wieser]

map is not the same operation on ideals

[Artie Khovanov]

fine but eg span is
is my point

[Artie Khovanov]

and the simp-normal form is Ideal.span so the API is duplicated

[Eric Wieser]

Agreed with Andrew that duplicating the API is not so bad an option, as long as the Ideal one is proved with the span one