Commit 2024-08-23 02:52 08b234f1

View on Github →

chore(SimpleGraph): fix DecidableEq/Fintype assumptions (#16079) Found by a linter in #10235 Mostly repeats @grunweg's #15306 accidentally reverted by @semorrison's #15726

Estimated changes

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

modified theorem SimpleGraph.odd_card_iff_odd_components

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 theorem SimpleGraph.IsTuranMaximal.isEquipartition

modified theorem SimpleGraph.IsTuranMaximal.iso

modified theorem SimpleGraph.IsTuranMaximal.not_adj_iff_part_eq