Theorems · Theorem · commutative algebra

MvPowerSeries.LinearTopology.hasBasis_nhds_zero

∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace R] [IsLinearTopology R R]
  [IsLinearTopology Rᵐᵒᵖ R],
  (nhds 0).HasBasis (fun Id => ↑Id.1 ∈ nhds 0) fun Id => ↑(MvPowerSeries.LinearTopology.basis σ R Id)

If the ring R is endowed with a linear topology, then the sets ↑basis σ R (J, d), for J : TwoSidedIdeal R which are neighborhoods of 0 : R and d : σ →₀ ℕ, constitute a basis of neighborhoods of 0 : MvPowerSeries σ R for the product topology.

Defined in

Mathlib.RingTheory.MvPowerSeries.LinearTopology

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingTopologicalSpaceIsLinearTopologyIsLinearTopology