mul_self_nonneg

Mathlib.Algebra.Order.Ring.Unbundled.Basic

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

English

Same as Sq Nonpos under simplifications.

Русский

То же самое, что Sq Nonpos после упрощения.

LaTeX

$$$r^2 \le 0 \iff r = 0$$$

Lean4

theorem mul_self_nonneg [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] (a : R) : 0 ≤ a * a := by
  simpa only [sq] using sq_nonneg a

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

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

Разделы

Аффилиация

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