mathlib

8acf2263 - feat(algebra/geom_sum): divisibility of sums and differences of powers (#17996)

feat(algebra/geom_sum): divisibility of sums and differences of powers (#17996) If `n : ℕ` and `x` and `y` belong to a `comm_ring`, then `x - y ∣ x ^ n - y ^ n`. If `n` is odd, then `x + y ∣ x ^ n + y ^ n`. These results follow from `geom_sum₂_mul`. There are additional theorems for when `x` and `y` are natural numbers. Co-authored-by: Niels Voss <nvosscode@gmail.com>