topologicalSpaceModule — Mathlib

English

There is a natural adic topology on an R-module M induced by I, defined as adicModuleTopology.

Русский

Существует естественная адическая топология на R-модуле M, индуцированная I, задаваемая как adicModuleTopology.

LaTeX

$$$\text{topologicalSpaceModule}(M) = (I).adicModuleTopology M$$$

Lean4

/-- The adic topology on an `R` module coming from the ideal `WithIdeal.I`.
This cannot be an instance because `R` cannot be inferred from `M`. -/
def topologicalSpaceModule (M : Type*) [AddCommGroup M] [Module R M] : TopologicalSpace M :=
  (i : Ideal R).adicModuleTopology M

Похожие утверждения