cast_le_neg_one_of_neg

Mathlib.Algebra.Order.Ring.Cast

URI: https://scilib.ai/kg/mathlib#Int.cast_le_neg_one_of_neg

English

If a < 0 in Z, then a.cast ≤ −1 in R.

Русский

Если a < 0 в Z, то a.cast ≤ −1 в R.

LaTeX

$$a^{\mathsf{cast}} \le -1$$

Lean4

theorem cast_le_neg_one_of_neg (h : a < 0) : (a : R) ≤ -1 :=
  by
  rw [← Int.cast_one, ← Int.cast_neg, cast_le]
  exact Int.le_sub_one_of_lt h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru