Commit 2024-08-01 19:38 dea069ea

View on Github →

chore(Turan): remove superfluous DecidableEq assumption (#15280) Found by the DecidableEq linter in #10235.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Turan.lean

modified theorem SimpleGraph.IsTuranMaximal.card_parts

modified theorem SimpleGraph.IsTuranMaximal.card_parts_le

modified theorem SimpleGraph.IsTuranMaximal.degree_eq_card_sub_part_card

modified def SimpleGraph.IsTuranMaximal.finpartition

modified theorem SimpleGraph.IsTuranMaximal.isEquipartition

modified theorem SimpleGraph.IsTuranMaximal.iso

modified theorem SimpleGraph.IsTuranMaximal.not_adj_iff_part_eq