From 7b29d976edfebf211141c83fc325ae8dd5e5414b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Thu, 13 Nov 2025 22:37:17 -0500 Subject: [PATCH] feat: add instances `NeZero(n^0)` for `n : Nat` and `n : Int` (#10739) This PR adds two missing `NeZero` instances for `n^0` where `n : Nat` and `n : Int`. --- > [!NOTE] > Add NeZero instances for n^0 when n : Nat and n : Int. > > Written by [Cursor Bugbot](https://cursor.com/dashboard?tab=bugbot) for commit 8305e65ba5d7037a6b1f5a631596822709f48c0a. This will update automatically on new commits. Configure [here](https://cursor.com/dashboard?tab=bugbot). Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> --- src/Init/Data/Int/Pow.lean | 2 ++ src/Init/Data/Nat/Basic.lean | 2 ++ 2 files changed, 4 insertions(+) diff --git a/src/Init/Data/Int/Pow.lean b/src/Init/Data/Int/Pow.lean index f7eff62ce4..e900aac527 100644 --- a/src/Init/Data/Int/Pow.lean +++ b/src/Init/Data/Int/Pow.lean @@ -62,6 +62,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⟩ + @[simp, norm_cast] protected theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by match n with diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index e25128a7a1..ea9f2853a1 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -817,6 +817,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]