Mathlib v3 is deprecated. Go to Mathlib v4

Theorem topological_semiring.has_continuous_neg_of_mul

Modification history

2022-03-31 06:51
src/topology/algebra/ring.lean
refactor(*): rename `topological_ring` to `topological_semiring` and introduce a new `topological_ring` extending `has_continuous_neg` (#12864) …
Added topological_semiring.has_continuous_neg_of_mulView on Github →