Theorems · Theorem · Lie groups

IsSemitopologicalSemiring.toIsSemitopologicalRing

∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonAssocRing R],
  IsSemitopologicalSemiring R → IsSemitopologicalRing R

If R is a ring which is a semitopological semiring, then it is automatically a semitopological 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 17 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceNonAssocRing