no goals
α : Type u_1
β : Type ?u.129705
γ : Type ?u.129708
ι : Type ?u.129711
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
a : α
n : ℕ
⊢ ‖a ^ Nat.zero‖₊ ≤ ‖a‖₊ ^ Nat.zero
simp only [Nat.zero_eq, pow_zero, nnnorm_one, le_rfl]