div_nat_lt_self_of_pos_of_two_le

Mathlib.Algebra.Order.Field.Basic

URI: https://scilib.ai/kg/mathlib#div_nat_lt_self_of_pos_of_two_le

English

If a > 0 and 2 ≤ n, then a / n < a.

Русский

Если a > 0 и 2 ≤ n, то a/n < a.

LaTeX

$$$a>0 \Rightarrow (2 \le n) \Rightarrow \frac{a}{n} < a$$$

Lean4

theorem div_nat_lt_self_of_pos_of_two_le (ha : 0 < a) {n : ℕ} (hn : 2 ≤ n) : a / n < a :=
  div_lt_self ha (n.one_lt_cast.mpr hn)

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

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

Разделы

Аффилиация

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