ofSubring — Mathlib

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 }

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