Theorems · Theorem · commutative algebra

IsLinearTopology.hasBasis_twoSidedIdeal

∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R],
  (nhds 0).HasBasis (fun I => ↑I ∈ nhds 0) fun I => ↑I

If a ring R is linearly ordered as a left and right module over itself, then it has a basis of neighborhoods of zero made of two-sided ideals. This is usually called a linearly topologized ring, but we do not add a specific spelling: you should use [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] instead.

Defined in

Mathlib.Topology.Algebra.LinearTopology

Cited by

3 results in Mathlib

Foundations

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

Assumes

RingTopologicalSpaceIsLinearTopologyIsLinearTopology