PR summary 05a5af1841

Import changes for modified files

No significant changes to the import graph

Declarations diff

No declarations were harmed in the making of this PR! 🐙

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

./scripts/reporting/technical-debt-metrics.sh pr_summary

Thanks for your PR and for cleaning up the .bib entry I added. I tried following the links in your PR description, and mostly don't see how they support your point though. Can you double-check, please? (They could be AI-hallucinated; I've seen this before. And they do look plausible, so you really need to check.)

Thanks for asking! I did check the links before publishing the PR, but I agree that I didn't communicate what the links were showing very well. Let me give it another try:

The first two links (https://fama.iff.csic.es/personas/margalef/margalef.html, https://produccioncientifica.ucm.es/investigadores/166066/tesis) are institutional pages that use the spelling of the author names that I propose, "Margalef Roig" and "Domínguez", respectively.

The next two links (https://books.google.com/books/about/Differential_Topology.html?id=gexAr04vRT4C, https://books.google.com/books/about/Topolog%C3%ADa_diferencial.html?id=0PRMy3ffm4QC) are Google books entries for the original Spanish version of the book and the English version from 1992 that you cite. They show that the title of the book is "Differential Topology" in the English version and "Topología diferencial" in the original Spanish, which justifies the change to the title field. The 5th page of the Spanish version, as shown on the page, also supports the author name spelling I'm proposing.

The fifth link (https://search.worldcat.org/title/Differential-topology/oclc/25713102), claims the publisher is "North-Holland, Amsterdam" and again repeats the author names that I suggest.

The final link (https://www.ams.org/tran/2010-362-08/S0002-9947-10-05073-7/) references this same book (see under references) and uses "North-Holland Publishing Co., Amsterdam" as the publisher.

In conclusion: I think the changes to the author names are well-evidenced. The same is true for the title change.

The evidence for the change to the publisher field is perhaps a bit less clear-cut. You could make the case that "North-Holland, Amsterdam" would be tidier, or even "Elsevier", since North-Holland had been acquired by Elsevier already in 1970.

I still think "North-Holland Publishing Co." is cleaner than "North-Holland" alone, though, as the latter is easy to misread as a toponym. Also, "North-Holland Publishing Co." is already used in Mathlib (see ref. MR0302656) and is referenced elsewhere (see the final link above, but also https://en.wikipedia.org/wiki/Elsevier and https://www.wikidata.org/wiki/Q19960298).

-awaiting-author