Commit 2022-08-22 23:29 8f9efd68

View on Github →

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.

Estimated changes

Modified src/topology/algebra/module/character_space.lean

deleted theorem weak_dual.character_space.coe_apply

added theorem weak_dual.character_space.coe_coe

added theorem weak_dual.character_space.coe_to_clm

added theorem weak_dual.character_space.coe_to_non_unital_alg_hom

deleted theorem weak_dual.character_space.continuous

deleted theorem weak_dual.character_space.map_add

deleted theorem weak_dual.character_space.map_mul

deleted theorem weak_dual.character_space.map_one

deleted theorem weak_dual.character_space.map_smul

deleted theorem weak_dual.character_space.map_zero

deleted theorem weak_dual.character_space.to_clm_apply

modified def weak_dual.character_space.to_non_unital_alg_hom