Lifting exponent lemma

Stream: Is there code for X?

[Alex Zhao]

Lifting the exponent lemma: v_p(a^n-b^n)=v_p(a-b)+v_p(n) for prime p

[Kevin Buzzard]

This isn't in mathlib because it's not true, e.g. a=3, b=1, n=2, p=2.

[Kevin Buzzard]

In general I think it's best if you post Lean code. There are several ways of writing v_p in Lean and whether or not the fixed version is in mathlib might depend on which way you choose.

[David Wärn]

Alex just forgot to add the assumptions that p is odd, doesn't divide a, and does divide a-b. I don't think this is in mathlib

[Kevin Buzzard]

I definitely recall someone talking about this sort of thing recently. You need these kinds of lemmas all over the place when doing Witt vectors (in particular the theory of Teichmuller lifts) but I suspect that it would be easier to develop the theory for integers separately :-)

Oh, ok I remember the context now -- the question was whether we have that if a==b mod p^n then a^p==b^p mod p^(n+1) again under the kind of hypotheses David suggested. I guess this is the inductive step one needs.

[David Wärn]

It's a pretty popular lemma in olympiad circles. It's basically equivalent to the assertion that $(\Z / p^n \Z)^\times$ is cyclic for $p$ odd. There are simple proofs which should be straightforward to formalise, where you just factorise $(a^p - b^p) = (a-b) (a^{p-1} +\ldots)$. I think there's also a more high-brow argument where you say that the Taylor series for exp and log induce a group isomorphism between (some neighbourhood of 0, under addition) and (some neighbourhood of 1, under multiplication) in the p-adics. For even p the radius of convergence is smaller since $v_2(n!) = (1-o(1))n$