Maybe these should be in mathlib

theorem PadicInt.toZMod_surjective (p : ℕ) [Fact (Nat.Prime p)] : Function.Surjective ⇑toZMod

theorem PadicInt.toZModPow_surjective (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : Function.Surjective ⇑(toZModPow n)