English
If a ring R is linearly topologized both as a left and as a right module, then neighborhoods of zero have a basis by two-sided ideals.
Русский
Если кольцо R линейно топологизировано слева и справа, окрестности нуля образуют база по двусторонним идеалам.
LaTeX
$$$ (\\mathcal{N}0).HasBasis (I : TwoSidedIdeal R \\mapsto (I:Set R) \\in 𝓝 0) (I:Set R) $$$
Lean4
/-- 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. -/
theorem hasBasis_twoSidedIdeal [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] :
(𝓝 (0 : R)).HasBasis (fun I : TwoSidedIdeal R ↦ (I : Set R) ∈ 𝓝 0) (fun I : TwoSidedIdeal R ↦ (I : Set R)) :=
hasBasis_subbimodule R Rᵐᵒᵖ |>.to_hasBasis
(fun I ⟨hI, hRI, hRI'⟩ ↦ ⟨.mk' I (zero_mem _) add_mem neg_mem (hRI _ _) (hRI' _ _), by simpa using hI, by simp⟩)
(fun I hI ↦ ⟨I.asIdeal.toAddSubgroup, ⟨hI, I.mul_mem_left, fun r x hx ↦ I.mul_mem_right x (r.unop) hx⟩, subset_rfl⟩)
