no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ‖z ^ 0‖ = ‖z‖ ^ 0
simp
p : ℕ
inst✝ : Fact (Nat.Prime p)
z : ℤ_[p]
k : ℕ
⊢ ‖z‖ * ‖z ^ k‖ = ‖z‖ * ‖z‖ ^ k
p : ℕ
inst✝ : Fact (Nat.Prime p)
z : ℤ_[p]
k : ℕ
⊢ ‖z ^ (k + 1)‖ = ‖z‖ ^ (k + 1)
rw [pow_succ, pow_succ, norm_mul]
case e_a
p : ℕ
inst✝ : Fact (Nat.Prime p)
z : ℤ_[p]
k : ℕ
⊢ ‖z ^ k‖ = ‖z‖ ^ k
p : ℕ
inst✝ : Fact (Nat.Prime p)
z : ℤ_[p]
k : ℕ
⊢ ‖z‖ * ‖z ^ k‖ = ‖z‖ * ‖z‖ ^ k
congr
no goals
case e_a
p : ℕ
inst✝ : Fact (Nat.Prime p)
z : ℤ_[p]
k : ℕ
⊢ ‖z ^ k‖ = ‖z‖ ^ k
apply norm_pow