pow_eq_pow_iff_of_ne_zero — Mathlib

English

For all a, b in a ring with order and n ≠ 0, a^n = b^n iff a = b or (a = -b and n is even).

Русский

Для любых a, b и n ≠ 0, a^n = b^n тогда и только тогда, когда a=b или a=-b и n чётно.

LaTeX

$$a^n = b^n \\iff a = b \\lor (a = -b \\land \\text{Even}(n))$$

Lean4

theorem pow_eq_pow_iff_of_ne_zero (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n :=
  match n.even_xor_odd with
  | .inl hne => by
    simp only [*, and_true, ← abs_eq_abs, ← pow_left_inj₀ (abs_nonneg a) (abs_nonneg b) hn, hne.1.pow_abs]
  | .inr hn => by simp [hn, (hn.1.strictMono_pow (R := R)).injective.eq_iff]

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