English
Let K be a linearly ordered semifield and p a nonnegative rational. Then the inequality 1 < p, written in the ambient field K, holds if and only if 1 < p as a nonnegative rational number. In particular, the order around 1 is preserved by the natural embedding of nonnegative rationals into K.
Русский
Пусть K — упорядоченная полейная система с нормированной структурой, p ∈ ℚ≥0. Тогда неравенство 1 < p, взятое в поле K, эквивалентно 1 < p как неотрицательному рациональному числу. То есть порядок вокруг 1 сохраняется при вставке ℚ≥0 в K.
LaTeX
$$$1 < (p : K) \iff 1 < p$$$
Lean4
@[simp]
theorem one_lt_cast : 1 < (p : K) ↔ 1 < p := by norm_cast
