pow_eq_neg_pow_iff — Mathlib

English

Let b ≠ 0. Then a^n = − b^n iff a = −b and n is odd.

Русский

Пусть b ≠ 0. Тогда a^n = − b^n тогда и только тогда, когда a = −b и n нечётно.

LaTeX

$$$$ a^n = - b^n \iff a = - b \land \operatorname{Odd}(n), \quad \text{при } b \neq 0. $$$$

Lean4

theorem pow_eq_neg_pow_iff (hb : b ≠ 0) : a ^ n = -b ^ n ↔ a = -b ∧ Odd n :=
  match n.even_or_odd with
  | .inl he =>
    suffices a ^ n > -b ^ n by simpa [he, not_odd_iff_even.2 he] using this.ne'
    lt_of_lt_of_le (by simp [he.pow_pos hb]) (he.pow_nonneg _)
  | .inr ho => by simp only [ho, and_true, ← ho.neg_pow, (ho.strictMono_pow (R := R)).injective.eq_iff]

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