English
Let p, q be rational numbers and K a field equipped with a compatible linear order. Then the natural embedding of the rationals into K preserves minima: the image of min(p, q) in K equals the minimum of the images of p and q in K, i.e. (↑(min p q) : K) = min (p : K) (q : K).
Русский
Пусть p, q ∈ ℚ и K — поле с совместимым линейным порядком. Тогда естественное включение ℚ в K сохраняет минимум: образ min(p, q) в K равен min образов p и q в K, то есть (↑(min p q) : K) = min (p : K) (q : K).
LaTeX
$$$(\min(p,q))^K = \min(p^K,q^K)$$$
Lean4
@[simp, norm_cast]
theorem cast_min (p q : ℚ) : (↑(min p q) : K) = min (p : K) (q : K) :=
(@cast_mono K _).map_min
