Theorems · Theorem · number theory

Int.two_pow_sub_pow

∀ {x y : ℤ} {n : ℕ},
  2 ∣ x - y →
    ¬2 ∣ x →
      Even n →
        emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 ↑n

Lifting the exponent lemma for p = 2

Defined in

Mathlib.NumberTheory.Multiplicity

Cited by

1 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound