Commit 2025-11-26 01:16 0ceb38e3
View on Github →chore: use generic map_X lemmas where possible (#31244)
While thinking about grind annotations for homomorphisms, it occurs to me that automation is more likely when we use the generic, rather than namespaced, lemmas where possible. This is some cleanup in that direction.