Commit 2025-08-07 00:48 80a716ba

View on Github →

chore(Data/FunLike/Equiv): remove FunLike argument in subsingleton_dom (#27911) This PR removes an unneccessary hypothesis that I spotted in subsingleton_dom.

Estimated changes

modified theorem EquivLike.subsingleton_dom