Zulip Chat Archive

Stream: maths

Topic: Subring inclusion


view this post on Zulip 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

view this post on Zulip Adam Topaz (Aug 31 2020 at 21:36):

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

view this post on Zulip 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