one_le_sq_iff_one_le_abs

Mathlib.Algebra.Order.Ring.Abs

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

English

1 ≤ a^2 iff 1 ≤ |a|.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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