English
If S is empty, the S-integers form the smallest R-subalgebra of K, which is precisely R itself via the natural embedding of R into K.
Русский
Если S пустое, S-интегралы образуют минимальную подалгебру R внутри K, то есть сами R через естественное вложение R в K.
LaTeX
$$$\text{S-integers}(K,\emptyset)=R$$$
Lean4
/-- If `S` is the empty set, then the `S`-integers are the minimal `R`-subalgebra of `K` (which is
just `R` itself, via `Algebra.botEquivOfInjective` and `IsFractionRing.injective`). -/
@[simp]
theorem integer_empty : (∅ : Set (HeightOneSpectrum R)).integer K = ⊥ :=
by
ext x
simp only [Set.integer, Set.mem_empty_iff_false, not_false_eq_true, true_implies]
refine ⟨HeightOneSpectrum.mem_integers_of_valuation_le_one K x, ?_⟩
rintro ⟨y, rfl⟩ v
exact v.valuation_le_one y
