Commit 2022-09-29 12:54 2e09d790

View on Github →

feat(topology/algebra/algebra): algebra_clm does not need a normed space or field (#16690) This also clean up the variables in the topology/algebra/algebra.lean file, to ensure that the type variables come first (as this is a useful convention for when using @ notation).

Estimated changes

Modified src/analysis/normed_space/basic.lean

deleted def algebra_map_clm

deleted theorem algebra_map_clm_coe

deleted theorem algebra_map_clm_to_linear_map

Modified src/analysis/normed_space/exponential.lean

Modified src/analysis/normed_space/spectrum.lean

Modified src/topology/algebra/algebra.lean

added def algebra_map_clm

added theorem algebra_map_clm_coe

added theorem algebra_map_clm_to_linear_map

modified theorem continuous_algebra_map

modified theorem continuous_algebra_map_iff_smul

modified theorem has_continuous_smul_of_algebra_map