Ideal span vs submodule span

Stream: mathlib4

[Brendan Seamas Murphy]

I just saw a chain of rewrites that had Ideal.submodule_span_eq in it because a previous definition used R ∙ a instead of Ideal.span {a}. This notation is shorter and more convenient, but it does sort of abuse the defeq Ideal R = Submodule R R (maybe I wouldn't worry as much about this if Ideal was an abbrev or if Ideal.map and Submodule.map weren't different) and causes some awkwardness with rw. Should existing instances of Submodule.span R in places where an Ideal R is expected be refactored to Ideal.span or am I making a mountain out of a molehill?

[Johan Commelin]

I agree this is an issue, but I would also be sad to see the nice notation go...

[Brendan Seamas Murphy]

Honestly I'm not a fan of it with how many dots are floating around already... But enough people like it and it's widely used enough that I'm not going to advocate removing it

[Eric Wieser]

Is docs#Ideal not an abbrev?

[Brendan Seamas Murphy]

Oh wait it is, I have no idea what I was looking at when I said that

[Brendan Seamas Murphy]

Probably Ideal.span