Zulip Chat Archive

Stream: Is there code for X?

Topic: Injectivity of field extensions


view this post on Zulip Jakob Scholbach (Mar 20 2021 at 20:31):

In the context of two fields F and L, and [algebra F L], do we have a statement function.injective (algebra_map F L) ?

view this post on Zulip Eric Wieser (Mar 20 2021 at 20:37):

Yes, perhaps docs#algebra_map_injective but I don't remember the name

view this post on Zulip Johan Commelin (Mar 20 2021 at 20:46):

docs#ring_hom.injective ?

view this post on Zulip Jakob Scholbach (Mar 20 2021 at 20:46):

Yes!


Last updated: May 16 2021 at 05:21 UTC