Theorems · Inductive type · Lie groups

IsTopologicalSemiring

(R : Type u_1) → [TopologicalSpace R] → [NonUnitalNonAssocSemiring R] → Prop

A topological semiring is a semiring R where addition and multiplication are continuous. We allow for non-unital and non-associative semirings as well. The IsTopologicalSemiring class should only be instantiated in the presence of a NonUnitalNonAssocSemiring instance; if there is an instance of NonUnitalNonAssocRing, then IsTopologicalRing should be used. Note: in the presence of NonAssocRing, these classes are mathematically equivalent (see IsTopologicalSemiring.continuousNeg_of_mul or IsTopologicalSemiring.toIsTopologicalRing).

Defined in

Mathlib.Topology.Algebra.Ring.Basic

Cited by

442 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

TopologicalSpaceNonUnitalNonAssocSemiring