Commit 2025-03-19 16:30 1913ea88

View on Github →

refactor(SimpleGraph/Copy): redefine Copy as a structure (#23090) This is cleaner, and we weren't getting much out of it being an abbrev anyway. Zulip

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Copy.lean

added theorem SimpleGraph.Copy.coe_mk

deleted theorem SimpleGraph.Copy.coe_toHom_apply

added theorem SimpleGraph.Copy.ext

modified theorem SimpleGraph.Copy.injective

added theorem SimpleGraph.Copy.toHom_apply

added structure SimpleGraph.Copy