abs_le_one_iff_mul_self_le_one

Mathlib.Algebra.Order.Ring.Abs

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

English

Let a be an element of a totally ordered ring. Then |a| ≤ 1 if and only if a^2 ≤ 1.

Русский

Пусть a — элемент строго упорядоченного кольца. Тогда |a| ≤ 1 тогда же, когда a^2 ≤ 1.

LaTeX

$$$|a| \\le 1 \\iff a^2 \\le 1$$$

Lean4

theorem abs_le_one_iff_mul_self_le_one : |a| ≤ 1 ↔ a * a ≤ 1 := by
  simpa only [abs_one, one_mul] using abs_le_iff_mul_self_le (a := a) (b := 1)

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

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

Разделы

Аффилиация

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