instCommRing — Mathlib

English

Let R be a Dedekind domain and K a field with an algebra structure R → K, and suppose K is the field of fractions of R. The Adele ring A(R, K) naturally carries the structure of a commutative ring.

Русский

Пусть R — кольцо Дедеконда, K — поле с определением алгебры R→K и K является полем дробей R. Адель-кольцо A(R, K) естественно образует коммутативное кольцо.

LaTeX

$$$\\mathrm{CommRing}(\\mathrm{AdeleRing}(R,K))$$$

Lean4

instance : CommRing (AdeleRing R K) :=
  Prod.instCommRing

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