one_lt_sq_iff_one_lt_abs

Mathlib.Algebra.Order.Ring.Abs

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

English

1 < a^2 iff 1 < |a|.

Русский

1 < a^2 эквивалентно 1 < |a|.

LaTeX

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

Lean4

@[simp]
theorem one_lt_sq_iff_one_lt_abs (a : α) : 1 < a ^ 2 ↔ 1 < |a| := by
  simpa only [one_pow, abs_one] using sq_lt_sq (a := 1) (b := a)

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

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

Разделы

Аффилиация

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