zpow_pos_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 < a^{n} \iff 0 < a)$$$

Lean4

theorem zpow_pos_iff (hn : Odd n) : 0 < a ^ n ↔ 0 < a :=
  lt_iff_lt_of_le_iff_le hn.zpow_nonpos_iff

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