zpow_neg_two_nonneg

Mathlib.Algebra.Order.Field.Power

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

English

For any a, a^(-2) is nonnegative in a canonically ordered field.

Русский

Для любого a в канонически упорядоченном поле a^(-2) неотрицательно.

LaTeX

$$$0\\le a^{(-2:\\mathbb{Z})}$$$

Lean4

theorem zpow_neg_two_nonneg (a : α) : 0 ≤ a ^ (-2 : ℤ) :=
  even_neg_two.zpow_nonneg _

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

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

Разделы

Аффилиация

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