Commit 2025-03-18 12:02 67c43e5f

View on Github →

chore(SimpleGraph): deduplicate Hom.ofLE and Hom.mapSpanningSubgraphs (#23024) We keep the first.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Coloring.lean

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

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

added theorem SimpleGraph.Hom.ofLE_apply

Modified Mathlib/Combinatorics/SimpleGraph/Metric.lean

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.transfer_eq_map_ofLE

deleted theorem SimpleGraph.Walk.transfer_eq_map_of_le