Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-02 09:31 2fa82513

View on Github →

refactor(*): rename {topological,smooth}_semiring to {topological,smooth}_ring (#8902) A topological semiring that is a ring, is a topological ring. A smooth semiring that is a ring, is a smooth ring. This PR renames:

topological_semiring -> topological_ring
smooth_semiring -> smooth_ring It drops the existing topological_ring and smooth_ring.

Estimated changes

Modified src/analysis/normed_space/basic.lean

Modified src/geometry/manifold/algebra/smooth_functions.lean

Modified src/geometry/manifold/algebra/structures.lean

modified theorem topological_ring_of_smooth

deleted theorem topological_semiring_of_smooth

Modified src/topology/algebra/algebra.lean

modified theorem continuous_algebra_map

modified theorem continuous_algebra_map_iff_smul

modified theorem has_continuous_smul_of_algebra_map

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/algebra/polynomial.lean

Modified src/topology/algebra/ring.lean

Modified src/topology/algebra/uniform_ring.lean

Modified src/topology/continuous_function/algebra.lean

Modified src/topology/continuous_function/polynomial.lean

Modified src/topology/instances/nnreal.lean

Modified src/topology/instances/real.lean