toIsTopologicalRing — Mathlib

English

From a topological semiring with ring-like structure, one obtains a topological ring structure automatically.

Русский

Из топологической полукольца с кольцевой структурой автоматически получаем топологическое кольцо.

LaTeX

$$$\\text{IsTopologicalRing}(R) \\leftarrow \\text{IsTopologicalSemiring}(R)$$$

Lean4

/-- If `R` is a ring which is a topological semiring, then it is automatically a topological
ring. This exists so that one can place a topological ring structure on `R` without explicitly
proving `continuous_neg`. -/
theorem toIsTopologicalRing [TopologicalSpace R] [NonAssocRing R] (_ : IsTopologicalSemiring R) : IsTopologicalRing R
    where toContinuousNeg := IsTopologicalSemiring.continuousNeg_of_mul

Похожие утверждения