sq_le_sq

Mathlib.Algebra.Order.Ring.Abs

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

English

For any a, b in an ordered ring, a^2 ≤ b^2 iff |a| ≤ |b|.

Русский

Для любых a, b в упорядоченном кольце a^2 ≤ b^2 эквивалентно |a| ≤ |b|.

LaTeX

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

Lean4

theorem sq_le_sq : a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b| := by simpa only [sq_abs] using sq_le_sq₀ (abs_nonneg a) (abs_nonneg b)

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

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

Разделы

Аффилиация

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