toRing_subgroups_basis — Mathlib

English

A RingSubgroupsBasis B yields a NonarchimedeanRing structure on the underlying ring with the induced topology.

Русский

База RingSubgroupsBasis B задаёт неархимедову топологию кольца на основе B.

LaTeX

$$From RingSubgroupsBasis B one obtains a NonarchimedeanRing with topology hB.topology.$$

Lean4

theorem toRing_subgroups_basis (hB : SubmodulesRingBasis B) : RingSubgroupsBasis fun i => (B i).toAddSubgroup :=
  by
  apply RingSubgroupsBasis.of_comm (fun i => (B i).toAddSubgroup) hB.inter hB.mul
  intro a i
  rcases hB.leftMul a i with ⟨j, hj⟩
  use j
  rintro b (b_in : b ∈ B j)
  exact hj ⟨b, b_in, rfl⟩

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