ZMod (p ^ r) is a local ring

For a prime p and r ≠ 0, the reduction map ZMod (p ^ r) →+* ZMod p is a local ring homomorphism into a field, hence ZMod (p ^ r) is a local ring.

theorem ZMod.isLocalHom_castHom_pow {n r : ℕ} [NeZero n] (hr : r ≠ 0) : IsLocalHom (castHom ⋯ (ZMod n))

For r ≠ 0, the reduction ZMod (n ^ r) →+* ZMod n is a local ring homomorphism.

instance ZMod.instIsLocalRingHPowNatOfFactPrimeOfNeZero (p r : ℕ) [Fact (Nat.Prime p)] [NeZero r] : IsLocalRing (ZMod (p ^ r))

ZMod (p ^ r) is a local ring for p prime and r ≠ 0.