topologicalAddGroup — Mathlib

English

A submodule S of a topological R-module M inherits a natural topological additive group structure, i.e., S is a topological additive group under the subspace topology.

Русский

Подмодуль S топологического R-модуля M наследует естественную топологическую структуру аддитивной группы; то есть S является топологической аддитивной группой подвыборки.

LaTeX

$$$S \text{ is a topological additively-closed subgroup of } M$.$$

Lean4

instance topologicalAddGroup {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M]
    [IsTopologicalAddGroup M] (S : Submodule R M) : IsTopologicalAddGroup S :=
  inferInstanceAs (IsTopologicalAddGroup S.toAddSubgroup)

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