Un error en el libro de álgebra abstracta de Dummit y Foote

Finding a bug in Dummit and Foote's Abstract Algebra

Durante su segunda semana en el Recurse Center, Ben Kallus intentó formalizar el libro de texto 'Abstract Algebra' de Dummit y Foote en Rocq. Se encontró con que el primer ejercicio de prueba era falso: la afirmación de que una función es inyectiva si y solo si tiene inversa izquierda falla en el caso de que el dominio sea vacío. El autor explica cómo el uso de un asistente de pruebas lo llevó a descubrir este caso límite, que probablemente no habría notado en papel.