Injectivity of field extensions

Stream: Is there code for X?

[Jakob Scholbach]

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

[Eric Wieser]

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

[Johan Commelin]

docs#ring_hom.injective ?

[Jakob Scholbach]

Yes!