sub_dvd_pow_sub_pow — Mathlib

English

For natural numbers x, y, n, we have x − y ∣ x^n − y^n.

Русский

Для натуральных x, y, n выполняется x − y делит x^n − y^n.

LaTeX

$$$$ x - y \mid x^{n} - y^{n} $$$$

Lean4

protected theorem sub_dvd_pow_sub_pow : x - y ∣ x ^ n - y ^ n :=
  by
  rcases le_or_gt y x with h | h
  · have : y ^ n ≤ x ^ n := Nat.pow_le_pow_left h _
    exact mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n
  · have : x ^ n ≤ y ^ n := Nat.pow_le_pow_left h.le _
    exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)

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