nightly#117 adaptations for nightly-2025-11-15

Stream: nightly-testing

[github mathlib4 bot]

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

[Kevin Buzzard]

I forget if the policy is to merge or ignore for PRs which do nothing other than bumping the date (I've merged it).

[Kim Morrison]

I prefer to merge, as it at least records the fact "we got this working on YYYY-MM-DD", so if a mysterious problem arises the next day it is clear which nightly to start investigating.

[Kim Morrison]

(Although François regularly closes such PRs at Batteries; it doesn't matter too much.)