Commit 2024-05-01 23:24 2c1517a8

View on Github →

chore(SimpleGraph/Regularity): Don't use Classical (#12575) The classical decidability instances were found in theorem statements, making them harder to use.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean

modified theorem SzemerediRegularity.increment_isEquipartition

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean