Subring inclusion

Stream: maths

[Adam Topaz]

Suppose I have a ring R and a (bundled) subring S : subring R. What's the name for the canonical inclusion S ->+* R? I'm sure this is in mathlib, but I can't seem to find it in ring_theory.subring

[Adam Topaz]

Got it. It's called subring.subtype for some reason...

[Johan Commelin]

@Adam Topaz Yup, those foo.subtype names are really confusing. I think we should rename all of them. But never got around to doing it.