Commit 2025-09-29 09:44 524bdd00

View on Github →

chore(Data/List/Sigma): remove redundant hypothesis from List.perm_dlookup (#30060) perm_nodupKeys can be used to eliminate a hypothesis from perm_dlookup

Estimated changes

modified theorem List.perm_dlookup
modified theorem List.perm_lookupAll