one_le_div'

Mathlib.Algebra.Order.Group.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#one_le_div'

← MathLib Explorer

English

In a group with order, for all a, if inst_1.lt a 1 then inst_1.lt (a^{-1}) a.

Русский

В группе с порядком, если a < 1, то a^{-1} < a.

LaTeX

$$$a < 1 \Rightarrow a^{-1} < a$$$

Lean4

@[to_additive (attr := simp) sub_nonneg]
theorem one_le_div' : 1 ≤ a / b ↔ b ≤ a := by
  rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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