algebraMap_monotone — Mathlib

English

The algebra map from a commutative ring R to an ordered module A is monotone: a ≤ b implies algebraMap(a) ≤ algebraMap(b).

Русский

Карта алгебраического отображения от кольца R в упорядочиваемый модуль A монотонна: a ≤ b → algebraMap(a) ≤ algebraMap(b).

LaTeX

$$algebraMap Monotone$$

Lean4

theorem algebraMap_monotone : Monotone (algebraMap R A) := fun a b h =>
  by
  rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, ← sub_nonneg, ← sub_smul]
  trans (b - a) • (0 : A)
  · simp
  · exact smul_le_smul_of_nonneg_left zero_le_one (sub_nonneg.mpr h)

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