English
Given a subring R of K and a predicate that every x or its inverse lies in R, the constructed A := ofSubring R hR is a valuation subring of K.
Русский
Пусть R — подкольцо K и выполнено условие, что для каждого x либо x ∈ R, либо x^{-1} ∈ R. Тогда A := ofSubring R hR является оценочным подкольцом K.
LaTeX
$$$A = \mathrm{ofSubring}(R,hR) \;\text{is a valuation subring of }K$$$
Lean4
/-- A subring `R` of `K` such that for all `x : K` either `x ∈ R` or `x⁻¹ ∈ R` is
a valuation subring of `K`. -/
def ofSubring (R : Subring K) (hR : ∀ x : K, x ∈ R ∨ x⁻¹ ∈ R) : ValuationSubring K :=
{ R with mem_or_inv_mem' := hR }