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