invOf_le_one

Mathlib.Algebra.Order.Invertible

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

← MathLib Explorer

English

If 1 ≤ a, then ⅟a ≤ 1.

Русский

Если 1 ≤ a, то ⅟a ≤ 1.

LaTeX

$$$ 1 \le a \implies \ ⅟a \le 1 $$$

Lean4

@[simp]
theorem invOf_le_one [Invertible a] (h : 1 ≤ a) : ⅟a ≤ 1 :=
  mul_invOf_self a ▸ le_mul_of_one_le_left (invOf_nonneg.2 <| zero_le_one.trans h) h

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

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

Разделы

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

Аффилиация

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