subalgebra.coe_top and friends

Stream: general

[Scott Morrison]

Currently src#subalgebra.coe_top reads

@[simp] theorem coe_top : (⊤ : subalgebra R A).to_submodule = ⊤ :=
submodule.ext $ λ x, iff_of_true mem_top trivial

It seems to me there's another theorem equally deserving that name, replacing to_submodule with to_subsemiring.

Similarly, coe_bot is above the coercion to set. This is all a bit confusing, and in any case incomplete.

Any suggestions about a good naming scheme for such lemmas? (@Eric Wieser?)

[Eric Wieser]

top_to_submodule, to match docs#submodule.top_to_add_submonoid?

[Eric Wieser]

There's not a coe in that statement at all!

[Eric Wieser]

(docs#submodule.coe_top says ↑⊤ = set.univ, which is what I'd expect it to say)