Multiplication by p^n identifies residues modulo p with the last kernel layer.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ZModdef mulPowPrime (p n : ℕ) : ZMod p →+ ZMod (p ^ (n + 1))Surrounding namespaces, section variables, and local commands at this declaration.
namespace ZModtheorem mulPowPrime_intCast (p n : ℕ) (a : ℤ) :
mulPowPrime p n (a : ZMod p) = (p ^ n : ZMod (p ^ (n + 1))) * aSurrounding namespaces, section variables, and local commands at this declaration.
namespace ZModtheorem mulPowPrime_injective {p : ℕ} (hp : p ≠ 0) (n : ℕ) :
Function.Injective (mulPowPrime p n)Every element killed by reduction modulo p^n is a multiple of p^n.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ZModtheorem exists_mulPowPrime_eq_of_castHom_eq_zero (p n : ℕ)
(z : ZMod (p ^ (n + 1)))
(hz : ZMod.castHom (pow_dvd_pow p (Nat.le_succ n)) (ZMod (p ^ n)) z = 0) :
∃ a : ZMod p, mulPowPrime p n a = zSurrounding namespaces, section variables, and local commands at this declaration.
namespace ZModtheorem castHom_mulPowPrime (p n : ℕ) (a : ZMod p) :
ZMod.castHom (pow_dvd_pow p (Nat.le_succ n)) (ZMod (p ^ n))
(mulPowPrime p n a) = 0Surrounding namespaces, section variables, and local commands at this declaration.
namespace ZModtheorem mulPowPrime_mul_castHom (p n : ℕ) (a : ZMod (p ^ (n + 1))) (b : ZMod p) :
mulPowPrime p n (ZMod.castHom (dvd_pow_self p (Nat.succ_ne_zero n)) (ZMod p) a * b) =
a * mulPowPrime p n b