Найдена ошибка в учебнике Dummit and Foote по абстрактной алгебре

Finding a bug in Dummit and Foote's Abstract Algebra

Бен Каллус, участник Recurse Center, формализует учебник Dummit and Foote по абстрактной алгебре в Rocq (ранее Coq) и обнаруживает, что первое упражнение на доказательство содержит ложное утверждение: инъективность функции не эквивалентна наличию левого обратного отображения в случае пустой области определения. Формальная проверка выявила контрпример, который легко пропустить при работе на бумаге. Ошибка уже занесена в список опечаток учебника.