Commit 2025-08-24 21:36 10b473a8

View on Github →

chore(Combinatorics): golf entire ofColex_inj, homOfEq_heq and mem_supp_of_adj_mem_supp. deprecate tail_cons_eq. (#28480)

Estimated changes

Modified Mathlib/Combinatorics/Colex.lean

modified theorem Finset.ofColex_inj

Modified Mathlib/Combinatorics/Quiver/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

modified theorem SimpleGraph.Walk.tail_cons

deleted theorem SimpleGraph.Walk.tail_cons_eq