Commit 2022-12-06 09:40 b9b2114f
View on Github →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.