## Stream: maths

### Topic: Subring inclusion

#### Adam Topaz (Aug 31 2020 at 21:33):

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 (Aug 31 2020 at 21:36):

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

#### Johan Commelin (Sep 01 2020 at 03:28):

@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.

Last updated: May 11 2021 at 15:12 UTC