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

Lean4

theorem zpow_nonpos_iff (hn : Odd n) : a ^ n ≤ 0 ↔ a ≤ 0 :=
  by
  rw [le_iff_lt_or_eq, le_iff_lt_or_eq, hn.zpow_neg_iff, zpow_eq_zero_iff]
  rintro rfl
  exact Int.not_even_iff_odd.2 hn .zero

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