intCast_mono — Mathlib

English

The cast map from integers to any ordered ring is monotone; this property is preserved under the congruence construction.

Русский

Отображение приведения целых чисел в упорядоченное кольцо монотонно и сохраняется под конструкцию конгруэнций.

LaTeX

$$$m \le n \Rightarrow (m : R) \le (n : R)$$$

Lean4

@[gcongr]
protected theorem intCast_mono {m n : ℤ} (hmn : m ≤ n) : (m : R) ≤ n :=
  cast_mono hmn

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