Theorems · Theorem · Lie groups

IsTopologicalSemiring.toIsTopologicalRing

∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonAssocRing R], IsTopologicalSemiring R → IsTopologicalRing R

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.

Defined in

Mathlib.Topology.Algebra.Ring.Basic

Cited by

0 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceNonAssocRing