Ring homomorphism of fields is injective

Stream: new members

[Sebastian Monnet]

I'd like to use the fact that a ring homomorphism between fields is injective. This must already by in mathlib somewhere, but I can't find it. Does anyone know where it is?

[Arthur Paulino]

Have you tried stating it and then closing the goal with library_search? Sometimes it works

[Kevin Buzzard]

example (K L : Type) [field K] [field L] [algebra K L] : function.injective (algebra_map K L) := by library_search

works for me, and tells me it's ring_hom.injective

[Kevin Buzzard]

Half the problem with questions like this is that there are often different ways to state the theorem, so it's usually best if you state a sorried mwe

[Sebastian Monnet]

Ahh library search is a great trick - thank you!

[Sebastian Monnet]

Kevin Buzzard said:

Half the problem with questions like this is that there are often different ways to state the theorem, so it's usually best if you state a sorried mwe

Okay will do that in future