Stream: Is there code for X?
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) ?
Eric Wieser (Mar 20 2021 at 20:37):
perhaps docs#algebra_map_injective but I don't remember the name
Johan Commelin (Mar 20 2021 at 20:46):
Jakob Scholbach (Mar 20 2021 at 20:46):
Last updated: May 16 2021 at 05:21 UTC