instIsTopologicalRing — Mathlib

English

FiniteAdeleRing carries a natural topological ring structure as a restricted product of local completions.

Русский

FiniteAdeleRing имеет естественную топологическую структуру кольца через ограниченный по месту продукт локальных замыканий.

LaTeX

$$instance : IsTopologicalRing (IsDedekindDomain.FiniteAdeleRing R K)$$

Lean4

instance : IsTopologicalRing (FiniteAdeleRing R K) :=
  haveI : Fact (∀ v : HeightOneSpectrum R, IsOpen (v.adicCompletionIntegers K : Set (v.adicCompletion K))) :=
    ⟨fun _ ↦ Valued.isOpen_valuationSubring _⟩
  RestrictedProduct.isTopologicalRing (fun (v : HeightOneSpectrum R) ↦ v.adicCompletion K)

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