Commit 2026-03-06 15:35 9657368b

View on Github →

feat(SimpleGraph/Subgraph): small things about spanningCoe and a small golf (#35331)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

added def SimpleGraph.Subgraph.coeEmbeddingSpanningCoe

added theorem SimpleGraph.Subgraph.edgeSet_spanningCoe

modified theorem SimpleGraph.Subgraph.inclusion.injective