Commit 2025-12-01 22:59 0e9e4c01

View on Github →

feat(SimpleGraph/Walks/Operations): golf ext_support using darts_injective and map_{fst,snd}_darts (#32106)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Walks/Operations.lean

modified theorem SimpleGraph.Walk.ext_support

Modified Mathlib/Data/List/Zip.lean

added theorem List.rightInverse_unzip_zip