Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-26 08:06 03f0bb1f

View on Github →

refactor(topology/algebra): define has_continuous_smul, use for topological semirings and algebras (#6823)

Estimated changes

added theorem continuous_algebra_map
modified theorem continuous_map.smul_apply
deleted theorem continuous.smul
deleted theorem continuous_on.smul
deleted theorem continuous_smul
deleted theorem filter.tendsto.smul
deleted theorem is_open_map_smul_of_unit
deleted theorem tendsto_smul
deleted def topological_module
added theorem continuous.const_smul
added theorem continuous.smul
added theorem continuous_at.smul
added theorem continuous_on.smul
added theorem filter.tendsto.smul
added theorem is_closed_map_smul'
added theorem is_closed_map_smul
added theorem is_open_map_smul'
added theorem is_open_map_smul
added theorem tendsto_const_smul_iff