zpow_nonneg_iff — Mathlib

English

Let α be a linearly ordered field with IsStrictOrderedRing. For any a ∈ α and any integer n, if n is odd, then a^n ≥ 0 if and only if a ≥ 0.

Русский

Пусть α — упорядоченное поле с свойством IsStrictOrderedRing. Для любого a ∈ α и целого n, если n нечётно, то a^n ≥ 0 тогда и только если a ≥ 0.

LaTeX

$$$\forall a \in \alpha, \forall n \in \mathbb{Z}, \mathrm{Odd}(n) \Rightarrow (0 \le a^{n} \iff 0 \le a)$$$

Lean4

protected theorem zpow_nonneg_iff (hn : Odd n) : 0 ≤ a ^ n ↔ 0 ≤ a :=
  le_iff_le_iff_lt_iff_lt.2 hn.zpow_neg_iff

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