basic): add `alg_hom.of_linear_map` and lemmas (#8151)

Commit

4 years ago

chore(algebra/algebra/basic): add `alg_hom.of_linear_map` and lemmas (#8151) This lets me golf `complex.lift` a little

Author

eric-wieser

Parents