mathlib3
8f9efd68 - feat(topology/algebra/module/character_space): provide instances of `continuous_linear_map_class`, `non_unital_alg_hom_class` and `alg_hom_class` (#16178)

Commit
3 years ago
feat(topology/algebra/module/character_space): provide instances of `continuous_linear_map_class`, `non_unital_alg_hom_class` and `alg_hom_class` (#16178) This updates `character_space` to utilize the new hom classes `continuous_linear_map_class`, `non_unital_alg_hom_class` and `alg_hom_class`. Also performs some minor housekeeping related to `simp` lemmas.
Author
Parents
Loading