Rocq

Rocq formalization exposes edge-case flaw in Dummit and Foote's Abstract Algebra

While formalizing Dummit and Foote's algebra textbook in the Rocq proof assistant, a Recurse Center participant found that the book's first proof exercise—claiming a function is injective if and only if it has a left inverse—fails when the domain is empty and the codomain is not. In that case the empty function is vacuously injective but has no left inverse, since no function can map from a nonempty codomain to an empty domain. The author later confirmed the issue is already listed in the book's published errata.