Multiplication by p embeds residues modulo p ^ n into residues modulo p ^ (n + 1). This additive map is well-defined even though upward casting is not a ring homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ZModdef mulPow (p n : ℕ) : ZMod (p ^ n) →+ ZMod (p ^ (n + 1))Surrounding namespaces, section variables, and local commands at this declaration.
namespace ZModtheorem mulPow_intCast (p n : ℕ) (a : ℤ) :
mulPow p n (a : ZMod (p ^ n)) = (p : ZMod (p ^ (n + 1))) * aSurrounding namespaces, section variables, and local commands at this declaration.
namespace ZModtheorem mulPow_injective {p : ℕ} (hp : p ≠ 0) (n : ℕ) :
Function.Injective (mulPow p n)The image of multiplication by p is the kernel of reduction modulo p.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ZModtheorem exists_mulPow_eq_of_castHom_eq_zero (p n : ℕ)
(z : ZMod (p ^ (n + 1)))
(hz : ZMod.castHom (pow_dvd_pow p (Nat.succ_le_succ (Nat.zero_le n)))
(ZMod (p ^ 1)) z = 0) :
∃ a : ZMod (p ^ n), mulPow p n a = zMultiplication by p respects multiplication by a coefficient reduced from the larger residue ring.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ZModtheorem mulPow_mul_castHom (p n : ℕ) (a : ZMod (p ^ (n + 1))) (b : ZMod (p ^ n)) :
mulPow p n (ZMod.castHom (pow_dvd_pow p (Nat.le_succ n)) (ZMod (p ^ n)) a * b) =
a * mulPow p n bReduction commutes with the additive maps given by multiplication by p.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ZModtheorem castHom_mulPow (p n : ℕ) (a : ZMod (p ^ (n + 1))) :
ZMod.castHom (pow_dvd_pow p (Nat.le_succ (n + 1))) (ZMod (p ^ (n + 1)))
(mulPow p (n + 1) a) =
mulPow p n (ZMod.castHom (pow_dvd_pow p (Nat.le_succ n)) (ZMod (p ^ n)) a)