[Merged by Bors] - refactor: move SimpleGraph.Iso.card_edgeFinset_eq to untangle imports#11817
Closed
Parcly-Taxel wants to merge 2 commits intomasterfrom
Closed
[Merged by Bors] - refactor: move SimpleGraph.Iso.card_edgeFinset_eq to untangle imports#11817Parcly-Taxel wants to merge 2 commits intomasterfrom
SimpleGraph.Iso.card_edgeFinset_eq to untangle imports#11817Parcly-Taxel wants to merge 2 commits intomasterfrom
Conversation
The single and currently unused theorem `card_edgeFinset_map` in `Combinatorics.SimpleGraph.Maps` causes a dependency of that file on `Combinatorics.SimpleGraph.Finite`, which is problematic because the key concepts of `Maps` don't depend on graph finiteness at all. This commit moves the offending theorem to `Operations` in anticipation of #9317.
Finite and Map in SimpleGraphFinite and Maps in SimpleGraph
YaelDillies
reviewed
Apr 1, 2024
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
Finite and Maps in SimpleGraphSimpleGraph.Iso.card_edgeFinset_eq to untangle imports
Contributor
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Apr 1, 2024
…ts (#11817) The single and currently unused theorem `card_edgeFinset_eq` in `Combinatorics.SimpleGraph.Maps` causes a dependency of that file on `Combinatorics.SimpleGraph.Finite`, which is problematic because the key concepts of `Maps` don't depend on graph finiteness at all. This commit moves the offending theorem to `Operations` in anticipation of #9317.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
SimpleGraph.Iso.card_edgeFinset_eq to untangle importsSimpleGraph.Iso.card_edgeFinset_eq to untangle imports
xgenereux
pushed a commit
that referenced
this pull request
Apr 15, 2024
…ts (#11817) The single and currently unused theorem `card_edgeFinset_eq` in `Combinatorics.SimpleGraph.Maps` causes a dependency of that file on `Combinatorics.SimpleGraph.Finite`, which is problematic because the key concepts of `Maps` don't depend on graph finiteness at all. This commit moves the offending theorem to `Operations` in anticipation of #9317.
atarnoam
pushed a commit
that referenced
this pull request
Apr 16, 2024
…ts (#11817) The single and currently unused theorem `card_edgeFinset_eq` in `Combinatorics.SimpleGraph.Maps` causes a dependency of that file on `Combinatorics.SimpleGraph.Finite`, which is problematic because the key concepts of `Maps` don't depend on graph finiteness at all. This commit moves the offending theorem to `Operations` in anticipation of #9317.
uniwuni
pushed a commit
that referenced
this pull request
Apr 19, 2024
…ts (#11817) The single and currently unused theorem `card_edgeFinset_eq` in `Combinatorics.SimpleGraph.Maps` causes a dependency of that file on `Combinatorics.SimpleGraph.Finite`, which is problematic because the key concepts of `Maps` don't depend on graph finiteness at all. This commit moves the offending theorem to `Operations` in anticipation of #9317.
callesonne
pushed a commit
that referenced
this pull request
Apr 22, 2024
…ts (#11817) The single and currently unused theorem `card_edgeFinset_eq` in `Combinatorics.SimpleGraph.Maps` causes a dependency of that file on `Combinatorics.SimpleGraph.Finite`, which is problematic because the key concepts of `Maps` don't depend on graph finiteness at all. This commit moves the offending theorem to `Operations` in anticipation of #9317.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The single and currently unused theorem
card_edgeFinset_eqinCombinatorics.SimpleGraph.Mapscauses a dependency of that file onCombinatorics.SimpleGraph.Finite, which is problematic because the key concepts ofMapsdon't depend on graph finiteness at all. This commit moves the offending theorem toOperationsin anticipation of #9317.