mathlib
5b702ec3 - chore(linear_algebra/basic): move map_comap_eq into submodule namespace (#9160)

Commit
4 years ago
chore(linear_algebra/basic): move map_comap_eq into submodule namespace (#9160) We change the following lemmas from the `linear_map` namespace into the `submodule` namespace - map_comap_eq - comap_map_eq - map_comap_eq_self - comap_map_eq_self This is consistent with `subgroup.map_comap_eq`, and the lemmas are about `submodule.map` so it make sense to keep them in the submodule namespace.
Author
Parents
Loading