English
Let α be a linearly ordered field with IsStrictOrderedRing. For any a,b ∈ α and any n ∈ ℤ, if b ≠ 0, then a^n = -b^n holds iff a = -b and Odd n.
Русский
Пусть α — упорядоченное поле с IsStrictOrderedRing. Для любых a,b ∈ α и n ∈ ℤ, если b ≠ 0, то a^n = -b^n эквивалентно a = -b и n нечетно.
LaTeX
$$$\forall a,b \in \alpha, \forall n \in \mathbb{Z}, b \neq 0 \Rightarrow a^{n} = -b^{n} \iff a = -b \land \mathrm{Odd}(n)$$$
Lean4
theorem zpow_eq_neg_zpow_iff₀ (hb : b ≠ 0) : a ^ n = -b ^ n ↔ a = -b ∧ Odd n :=
match n with
| Int.ofNat m => by simp [pow_eq_neg_pow_iff, hb]
| Int.negSucc m =>
by
simp only [← neg_ofNat_succ, zpow_neg, ← inv_neg, pow_eq_neg_pow_iff hb, inv_inj, zpow_natCast]
simp [parity_simps]
