mathlib
2fa82513 - refactor(*): rename {topological,smooth}_semiring to {topological,smooth}_ring (#8902)

Commit
4 years ago
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`.
Author
Parents
Loading