Commit 2025-02-15 11:19 3bc2081f

View on Github →

chore(SimpleGraph): fix Fintype vs Finite (#21892) Found by the linters in #10235

Estimated changes

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

added theorem SimpleGraph.ConnectedComponent.Represents.exists_inter_eq_singleton

modified theorem SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_mem

modified theorem SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_not_mem

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

modified theorem SimpleGraph.ncard_odd_components_mono

Modified Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean

modified theorem SimpleGraph.Subgraph.IsMatching.exists_of_universalVerts