Range equiv quotient by ker

Stream: Is there code for X?

[Pierre-Alexandre Bazin]

variables {R M N : Type*} [ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N]
example (f : N →ₗ[R] M) : (N ⧸ f.ker) ≃ₗ[R] f.range := sorry

do we have anything that tranforms f into a linear equiv this way ?

[Daniel Packer]

Is docs#linear_map.quot_ker_equiv_range what you're looking for?

[Eric Wieser]

Does library_search find that for you?

[Eric Wieser]

I guess you have to have it imported for that to work, and it's a leaf file that you might not have seen before.

[Pierre-Alexandre Bazin]

library_search couldn't find it, but that was indeed because I was lacking the import

[Riccardo Brasca]

Note that you can now search for "first isomorphism theorem" in the search bar, and several results show up.

[Riccardo Brasca]

This is strangely called " first isomorphism law" in the doc, but at least you can guess its real name.