feat: add instances NeZero(n^0) for n : Nat and n : Int

This PR adds two missing `NeZero` instances for `n^0` where `n : Nat` and `n : Int`.

Author: fgdorais

src/Init/Data/Int/Pow.lean

@@ -50,6 +50,8 @@ protected theorem pow_ne_zero {n : Int} {m : Nat} : n ≠ 0 → n ^ m ≠ 0 := b
 
 instance {n : Int} {m : Nat} [NeZero n] : NeZero (n ^ m) := ⟨Int.pow_ne_zero (NeZero.ne _)⟩
 
+instance {n : Int} : NeZero (n^0) := ⟨Int.one_ne_zero⟩
+
 -- This can't be removed until the next update-stage0
 @[deprecated Nat.pow_pos (since := "2025-02-17")]
 abbrev _root_.Nat.pos_pow_of_pos := @Nat.pow_pos

src/Init/Data/Nat/Basic.lean

@@ -801,6 +801,8 @@ protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pow_pos (by decide)
 instance {n m : Nat} [NeZero n] : NeZero (n^m) :=
   ⟨Nat.ne_zero_iff_zero_lt.mpr (Nat.pow_pos (pos_of_neZero _))⟩
 
+instance {n : Nat} : NeZero (n^0) := ⟨Nat.one_ne_zero⟩
+
 protected theorem mul_pow (a b n : Nat) : (a * b) ^ n = a ^ n * b ^ n := by
   induction n with
   | zero => simp [Nat.pow_zero]