basic): add `alg_(hom|equiv).map_matrix` (#8527)

Commit

4 years ago

feat(data/matrix/basic): add `alg_(hom|equiv).map_matrix` (#8527) This also adds a few standalone lemmas about `algebra_map`.

Author

eric-wieser

Parents