Skip to content

feat(Combinatorics/SimpleGraph/Matching): edgeSet is injective and strictly monotonic on matchings, and more API#36451

Open
SnirBroshi wants to merge 4 commits intoleanprover-community:masterfrom
SnirBroshi:feature/simple-graph/matching/more-api
Open

feat(Combinatorics/SimpleGraph/Matching): edgeSet is injective and strictly monotonic on matchings, and more API#36451
SnirBroshi wants to merge 4 commits intoleanprover-community:masterfrom
SnirBroshi:feature/simple-graph/matching/more-api

Conversation

@SnirBroshi
Copy link
Copy Markdown
Collaborator


Open in Gitpod

…strictly monotonic on matchings, and more API
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 10, 2026

PR summary 18a09f9093

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsMatching.mem_coe_toEdge
+ IsMatching.toEdge_preimage
+ IsMatching.verts_eq_biUnion_edgeSet
+ _root_.SimpleGraph.injOn_edgeSet_isMatching
+ _root_.SimpleGraph.strictMonoOn_edgeSet_isMatching
+ _root_.SimpleGraph.subgraph_edgeSet_monotone

You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions bot added the t-combinatorics Combinatorics label Mar 10, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 21, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 21, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 27, 2026
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 1, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-combinatorics Combinatorics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant