no goals
α : Type u_1
β : Type ?u.132724
γ : Type ?u.132727
ι : Type ?u.132730
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
a : α
n : ℕ
⊢ ‖a ^ Nat.zero‖ ≤ ‖a‖ ^ Nat.zero
simp only [Nat.zero_eq, pow_zero, norm_one, le_rfl]