p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(↑(toZModPow n) x) = ↑(RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n)) x
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(↑(toZModPow n) x) = ↑(toZModPow m) x
rw [← zmod_cast_comp_toZModPow _ _ h]
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(↑(toZModPow n) x) = ↑(RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n)) x
rfl