Mathlib v3 is deprecated. Go to Mathlib v4

Theorem topological_ring_of_smooth

Modification history

2022-03-31 06:51
src/geometry/manifold/algebra/structures.lean
refactor(*): rename `topological_ring` to `topological_semiring` and introduce a new `topological_ring` extending `has_continuous_neg` (#12864) …
Deleted topological_ring_of_smoothView on Github →
2021-09-02 09:31
src/geometry/manifold/algebra/structures.lean
refactor(*): rename {topological,smooth}_semiring to {topological,smooth}_ring (#8902) …
Modified topological_ring_of_smoothView on Github →
2021-03-07 10:18
src/geometry/manifold/algebra/structures.lean
refactor(geometry/manifold): drop some unused arguments (#6545) …
Added topological_ring_of_smoothView on Github →