Commit 2025-09-17 16:12 4f719ec3

feat(NumberTheory/Padic): extend API for zmodRepr (#29405) Include lemmas for simplifying norms of p - 1 when lifted into Z_[p] and Q_[p] Provide specialized lemmas for Padic that rewrite norms in a similar way as IsUltrametricDist lemmas, without the import Describe how norms of zmodRepr are equal to 1 for units, which is specialized for naturals cast into Z_[p] Extract mapping lemmas from the ring-hom version of zmodRepr (toZMod) and provide them for zmodRepr as well Connect the ZMod.val injection + cast to PadicInt.toZMod, showing that they are inverse via val_toZMod_eq_zmodRepr. In preparation for p - 1 roots of unity of Z_[p] and Q_[p]