nightly#116 adaptations for nightly-2025-11-14

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2025-11-14 nightly#116 Please review this PR. At the next toolchain release this diff will land in 'master'.

[Kevin Buzzard]

The only thing I see which surprises me is

-  npow_zero _ := rfl
-  npow_succ _ _ := rfl
+  npow_zero _ := by simp [Int.pow_zero]
+  npow_succ _ _ := by simp [Int.pow_succ]

in both Mathlib/Algebra/Group/Int/Defs.lean and Mathlib/Algebra/Ring/Int/Defs.lean. First, that it shows up at all, and secondly that it shows up twice (probably the ring one can just be deleted?). Was there some fundamental change in NPow on Int? Not that this bothers me. I'm fine with this being merged (perhaps after things are clarified a bit?)

[Robin Arnez]

Kevin Buzzard schrieb:

Was there some fundamental change in NPow on Int?

Previously, n^0 = 1 and a^(b+1) = a^b * a was defeq for Int. Now, this is traded for the defeq ((n : Nat) : Int) ^ m = ((n ^ m : Nat) : Int) which results in faster reduction times for things like (1 : Int) ^ 256 (which previously resulted in "maximum recursion depth reached").

[Kevin Buzzard]

Thanks. That answers my first question about the PR; I can't figure out the second one (why the proofs need to be given twice -- see my comments on the PR) but I don't think that should stop me merging it!