valuationSubring — Mathlib

English

The integers are contained in the valuation subring associated to v.

Русский

Целые числа содержатся в подкольце оценки, связанного с v.

LaTeX

$$Z \subseteq v.valuationSubring$$

Lean4

/-- The valuation subring associated to a valuation. -/
def valuationSubring : ValuationSubring K :=
  { v.integer with
    mem_or_inv_mem' := by
      intro x
      rcases val_le_one_or_val_inv_le_one v x with h | h
      exacts [Or.inl h, Or.inr h] }

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