p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (f j) = f i
⊢ ↑p ^ i ∣ nthHom f r j - nthHom f r i
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
r : R
i j : ℕ
h : i ≤ j
⊢ ↑p ^ i ∣ nthHom f r j - nthHom f r i
specialize f_compat i j h
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (f j) = f i
⊢ ↑(nthHom f r j) - ↑(nthHom f r i) = 0
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (f j) = f i
⊢ ↑p ^ i ∣ nthHom f r j - nthHom f r i
rw [← Int.coe_nat_pow, ← ZMod.int_cast_zmod_eq_zero_iff_dvd, Int.cast_sub]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (f j) = f i
⊢ ↑↑(ZMod.val (↑(f j) r)) - ↑↑(ZMod.val (↑(f i) r)) = 0
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (f j) = f i
⊢ ↑(nthHom f r j) - ↑(nthHom f r i) = 0
dsimp [nthHom]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (f j) = f i
⊢ ↑↑(ZMod.val (↑(f j) r)) - ↑↑(ZMod.val (↑(ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (↑(f j) r))) = 0
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (f j) = f i
⊢ ↑↑(ZMod.val (↑(f j) r)) - ↑↑(ZMod.val (↑(f i) r)) = 0
rw [← f_compat, RingHom.comp_apply]
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (f j) = f i
⊢ ↑↑(ZMod.val (↑(f j) r)) - ↑↑(ZMod.val (↑(ZMod.castHom (_ : p ^ i ∣ p ^ j) (ZMod (p ^ i))) (↑(f j) r))) = 0
simp only [ZMod.cast_id, ZMod.castHom_apply, sub_self, ZMod.nat_cast_val, ZMod.int_cast_cast]