openAddSubgroup — Mathlib

English

For each n, the subgroup I^n M forms an open additive subgroup of the R-module M under the adic topology.

Русский

Для каждого n подгруппа I^n M является открытой аддитивной подгруппой модуля M в адической топологии.

LaTeX

$$$\\text{openAddSubgroup}(n) :\\; @OpenAddSubgroup R _ I.adicTopology$$$

Lean4

/-- The elements of the basis of neighborhoods of zero for the `I`-adic topology
on an `R`-module `M`, seen as open additive subgroups of `M`. -/
def openAddSubgroup (n : ℕ) : @OpenAddSubgroup R _ I.adicTopology :=
  by
  letI := I.adicTopology
  refine ⟨(I ^ n).toAddSubgroup, ?_⟩
  convert (I.adic_basis.toRing_subgroups_basis.openAddSubgroup n).isOpen
  change (↑(I ^ n) : Set R) = ↑(I ^ n • (⊤ : Ideal R))
  simp

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