Topological (semi)rings #
A topological (semi)ring is a (semi)ring equipped with a topology such that all operations are continuous. Besides this definition, this file proves that the topological closure of a subring (resp. an ideal) is a subring (resp. an ideal) and defines products and quotients of topological (semi)rings.
Main Results #
subsemiring.topological_closure: the topological closure of a
subsemiringis itself a
prod_semiring: The product of two topological (semi)rings.
ideal.closure: The closure of an ideal is an ideal.
topological_ring_quotient: The quotient of a topological ring by an ideal is a topological ring.
A topological semiring is a semiring where addition and multiplication are continuous.
The (topological-space) closure of a subsemiring of a topological semiring is itself a subsemiring.
The product topology on the cartesian product of two topological semirings makes the product into a topological semiring.
- to_has_continuous_add : has_continuous_add α
- to_has_continuous_mul : has_continuous_mul α
- continuous_neg : continuous (λ (a : α), -a)
A topological ring is a ring where the ring operations are continuous.
The product topology on the cartesian product of two topological rings makes the product into a topological ring.
The (topological-space) closure of a subring of a topological semiring is itself a subring.