Mathlib v3 is deprecated. Go to Mathlib v4

Theorem has_continuous_smul_of_algebra_map

Modification history

2022-09-29 12:54
src/topology/algebra/algebra.lean
feat(topology/algebra/algebra): `algebra_clm` does not need a normed space or field (#16690) …
Modified has_continuous_smul_of_algebra_mapView on Github →
2022-03-31 06:51
src/topology/algebra/algebra.lean
refactor(*): rename `topological_ring` to `topological_semiring` and introduce a new `topological_ring` extending `has_continuous_neg` (#12864) …
Modified has_continuous_smul_of_algebra_mapView on Github →
2021-09-02 09:31
src/topology/algebra/algebra.lean
refactor(*): rename {topological,smooth}_semiring to {topological,smooth}_ring (#8902) …
Modified has_continuous_smul_of_algebra_mapView on Github →
2021-03-26 08:06
src/topology/algebra/algebra.lean
refactor(topology/algebra): define `has_continuous_smul`, use for topological semirings and algebras (#6823)
Added has_continuous_smul_of_algebra_mapView on Github →