Local rings modulo prime powers

For a positive power of a prime, a residue is a unit exactly when its reduction modulo the prime is nonzero. Mathlib's instance in Mathlib.RingTheory.ZMod.LocalRing makes the prime-power ring local; in that local ring, equality in the residue field is equality after reduction modulo the prime. The statements include the prime two and exclude the exponent-zero trivial ring.

Main declarations

• ZMod.isUnit_prime_pow_iff_castHom_ne_zero: the unit criterion under reduction.
• ZMod.residue_eq_residue_iff_castHom_eq: equality in the residue field is equality after reduction modulo the prime.

@[simp]

theorem ZMod.isUnit_prime_pow_iff_castHom_ne_zero (p k : ℕ) [Fact (Nat.Prime p)] (hk : 0 < k) (x : ZMod (p ^ k)) : IsUnit x ↔ (castHom ⋯ (ZMod p)) x ≠ 0

A residue modulo a positive prime power is a unit exactly when its reduction modulo the prime is nonzero.

theorem ZMod.residue_eq_residue_iff_castHom_eq (p k : ℕ) [Fact (Nat.Prime p)] [IsLocalRing (ZMod (p ^ k))] (hk : 0 < k) (x y : ZMod (p ^ k)) : (IsLocalRing.residue (ZMod (p ^ k))) x = (IsLocalRing.residue (ZMod (p ^ k))) y ↔ (castHom ⋯ (ZMod p)) x = (castHom ⋯ (ZMod p)) y

For a positive prime power, two residues have the same image in the local-ring residue field exactly when their reductions modulo the prime are equal.