nonarchimedean — Mathlib

English

Given a SubmodulesRingBasis B, one obtains a RingSubgroupsBasis B by taking the additive subgroups B_i as the underlying subgroups.

Русский

Из SubmodulesRingBasis B получают RingSubgroupsBasis B, рассматривая B_i как подгруппы.

LaTeX

$$SubmodulesRingBasis B → RingSubgroupsBasis (fun i => (B i).toAddSubgroup)$$

Lean4

theorem nonarchimedean : @NonarchimedeanRing A _ hB.topology :=
  by
  letI := hB.topology
  constructor
  intro U hU
  obtain ⟨i, -, hi : (B i : Set A) ⊆ U⟩ := hB.hasBasis_nhds_zero.mem_iff.mp hU
  exact ⟨hB.openAddSubgroup i, hi⟩

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