cast_one_le_of_pos

Mathlib.Algebra.Order.Ring.Cast

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

English

If a > 0 in Z, then 1 ≤ a in R.

Русский

Если a > 0 в Z, то 1 ≤ a в R.

LaTeX

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

Lean4

theorem cast_one_le_of_pos (h : 0 < a) : (1 : R) ≤ a :=
  mod_cast Int.add_one_le_of_lt h

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

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

Разделы

Аффилиация

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