isInteger_or_isInteger — Mathlib

English

For every x ∈ K, either x is an integer (IsLocalization.IsInteger R x) or x^{-1} is an integer.

Русский

Для каждого x ∈ K либо x является целым, либо x^{-1} является целым.

LaTeX

$$$\\forall x:\\, K,\\; IsLocalization.IsInteger R x \\lor IsLocalization.IsInteger R x^{-1}$$$

Lean4

theorem isInteger_or_isInteger [h : ValuationRing R] (x : K) :
    IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹ :=
  (iff_isInteger_or_isInteger R K).mp h x

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