inv_le_mabs

Mathlib.Algebra.Order.Group.Unbundled.Abs

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

English

The inverse is dominated by the modulus: a^{-1} ≤ |a|_m.

Русский

Обратное элементу ограничено модулем: a^{-1} ≤ |a|_м.

LaTeX

$$|a^{-1}|_m \le |a|_m$$

Lean4

@[to_additive]
theorem inv_le_mabs (a : α) : a⁻¹ ≤ |a|ₘ :=
  le_sup_right

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

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

Разделы

Аффилиация

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