abs_pow_sub_pow_le — 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\\neq 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 abs_pow_sub_pow_le [IsOrderedRing α] : |a ^ n - b ^ n| ≤ |a - b| * n * max |a| |b| ^ (n - 1) :=
  by
  obtain _ | n := n; · simp
  rw [Nat.add_sub_cancel, pow_sub_pow_eq_sub_mul_geomSum, abs_mul, mul_assoc, Nat.cast_succ]
  gcongr
  · exact abs_nonneg _
  · exact abs_geomSum_le ..

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