integer_univ — Mathlib

English

Let R be a Dedekind domain with field of fractions K, and S be the set of all height-one places of R in K. If S is the entire set of places, then every element of K is S-integral; equivalently, the S-integers coincide with K.

Русский

Пусть R — Дедекиндова область с полем дробей K, и S — множества всех мест высоты один для R в K. Если S — всe множество мест, то каждый элемент K является S-интегральным; то есть S-интегралы совпадают с K.

LaTeX

$$$\text{S-integers}(K,S)=K$$$

Lean4

/-- If `S` is the whole set of places of `K`, then the `S`-integers are the whole of `K`. -/
@[simp]
theorem integer_univ : (Set.univ : Set (HeightOneSpectrum R)).integer K = ⊤ :=
  by
  ext
  tauto

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