mathlib documentation


structure topological_semiring (α : Type u) [topological_space α] [semiring α] :

A topological semiring is a semiring where addition and multiplication are continuous.


In a topological ring, the left-multiplication add_monoid_hom is continuous.

In a topological ring, the right-multiplication add_monoid_hom is continuous.

def ideal.closure {α : Type u_1} [topological_space α] [comm_ring α] [topological_ring α] :
ideal αideal α

The closure of an ideal in a topological ring as an ideal.

theorem ideal.coe_closure {α : Type u_1} [topological_space α] [comm_ring α] [topological_ring α] (S : ideal α) :

theorem quotient_ring_saturate {α : Type u_1} [comm_ring α] (N : ideal α) (s : set α) :
( N) ⁻¹' (( N) '' s) = ⋃ (x : N), (λ (y : α), x.val + y) '' s