nightly#128 adaptations for nightly-2025-11-27

Stream: nightly-testing

[Kim Morrison]

chore: adaptations for nightly-2025-11-27 nightly#128

Please review this PR. At the next toolchain release this diff will land in 'master'.

[Kevin Buzzard]

Did something go wrong here? The diff is +11000 and the PR changes 642 files including docs/references.bib. It's hard to imagine that changes to lean 4 core result in mathlib being forced to add a reference to a 1988 Compositio paper.

[Kevin Buzzard]

Indeed the proposed addition to references.bib in this PR is already present in mathlib master.

[Kim Morrison]

Closing, there's a new one coming now.

[Kevin Buzzard]

Just to remark that as far as I'm aware there have been no new adaptation PRs since the faulty one on Nov 27th discussed above.