Commit 2024-07-28 18:21 812fe714

View on Github →

chore(Combinatorics): drop some DecidableEq assumptions (#15233)

Estimated changes

Modified Mathlib/Combinatorics/HalesJewett.lean

modified theorem Combinatorics.Subspace.exists_mono_in_high_dimension

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

modified theorem SimpleGraph.cliqueFree_map_iff

modified theorem SimpleGraph.isNClique_map_iff

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean

modified theorem SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty

Modified Mathlib/Data/Fintype/Shrink.lean