chore(number_theory/padics): fix lemma names and golf (#17798)
The `norm_p_pow` lemma was actually a lemma about `zpow`. This renames it add adds the missing lemma about pow.
This also uses a nicer algebra instance that agrees with the subring definition, although it probably doesn't matter anywhere.
