mk_map_of_archimedean — Mathlib

English

Let S and R be linearly ordered rings with S Archimedean, and f: S →o R an order-preserving ring homomorphism. If x ∈ S is nonzero, then mk(f(x)) = mk(f(1)).

Русский

Пусть S и R — линейно упорядоченные кольца, S — Архимедово, и f: S →o R — монотонный по порядку кольцевой гомоморфизм. Для любого x ∈ S с x ≠ 0 выполняется mk(f(x)) = mk(f(1)).

LaTeX

$$$\forall x \,(x \neq 0 \rightarrow \operatorname{mk}(f x) = \operatorname{mk}(f 1)).$$$

Lean4

/-- See `mk_map_of_archimedean'` for a version taking `M →+*o R`. -/
theorem mk_map_of_archimedean [Archimedean S] (f : S →+o R) {x : S} (h : x ≠ 0) : mk (f x) = mk (f 1) := by
  rw [← orderHom_mk, mk_eq_zero_of_archimedean h, orderHom_zero]

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