Theorems · Theorem · commutative algebra

IsLinearTopology.mk_of_hasBasis

∀ (R : Type u_1) {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] {ι : Sort u_4} {S : Type u_5} [inst_4 : SetLike S M] [SMulMemClass S R M]
  [AddSubmonoidClass S M] {p : ι → Prop} {s : ι → S}, ((nhds 0).HasBasis p fun i => ↑(s i)) → IsLinearTopology R M

To show that M is linearly-topologized as an R-module, it suffices to show that it has a basis of neighborhoods of zero made of R-submodules. Note: for technical reasons detailed in the module docstring, Lean sometimes struggles to find the right SMulMemClass instance. See IsLinearTopology.mk_of_hasBasis' for a more explicit variant.

Defined in

Mathlib.Topology.Algebra.LinearTopology

Cited by

3 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleTopologicalSpaceSetLikeSMulMemClassAddSubmonoidClass