mk_map_of_archimedean' — Mathlib

English

Let S be Archimedean and f: S →+*o R an order-preserving ring homomorphism. For every x ≠ 0 in S, mk(f(x)) = 0.

Русский

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

LaTeX

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

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) = 0 := by
  simpa using mk_map_of_archimedean f.toOrderAddMonoidHom h

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