Skip to content

feat(Combinatorics/SimpleGraph/InducedCopy): add UnlabeledEmbedding, unlabeledEmbeddingCount and embeddingCount #38631

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
FordUniver wants to merge 25 commits into
base: master
Choose a base branch
from
Open

feat(Combinatorics/SimpleGraph/InducedCopy): add UnlabeledEmbedding, unlabeledEmbeddingCount and embeddingCount #38631

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
6bf406f
feat(Combinatorics/SimpleGraph/Copy): introduce `Sub` carrier subtype
FordUniver May 13, 2026
65fb74a
Renamed Sub to UnlabeledCopy per suggestion by mitchell-horner
FordUniver May 17, 2026
1334d9e
feat(Combinatorics/SimpleGraph/Subgraph): add `Embedding.ofIsInduced`…
FordUniver May 13, 2026
0e1b271
use |>.isIndContained
FordUniver May 14, 2026
2b608ef
chore: fix stale Sub reference in UnlabeledCopy docstring
FordUniver Jul 8, 2026
5699548
Merge branch 'master' into feat/copy-sub-abbrev
FordUniver Jul 9, 2026
53a94cc
feat(Combinatorics/SimpleGraph/Copy): re-add copyCount_eq_card_image_…
FordUniver Jul 12, 2026
3669ba6
refactor(Combinatorics/SimpleGraph/Copy): rename copy counts and unif…
FordUniver May 13, 2026
568138c
chore(Combinatorics.SimpleGraph.Copy): replace file-wide @[expose] wi…
FordUniver May 13, 2026
e7cb121
chore(Combinatorics/SimpleGraph/Copy): migrate copyCount/unlabeledCop…
FordUniver May 13, 2026
277da3a
merge feat/subgraph-ofIsInduced into chore/copy-nat-card as diff base…
FordUniver Jul 12, 2026
97c26fb
feat(Combinatorics/SimpleGraph/InducedCopy): split induced material i…
FordUniver May 13, 2026
c6d766d
refactor(Combinatorics/SimpleGraph/InducedCopy): hoist `Embedding.toS…
FordUniver May 18, 2026
3e317f2
style(Combinatorics/SimpleGraph/InducedCopy): use `Embedding G H` ins…
FordUniver May 18, 2026
dec7da1
restored simpler proof of copyCount_eq_zero
FordUniver Jul 17, 2026
9a02a88
un-deprecated copyCount_eq_card_image_copyToSubgraph and restored pro…
FordUniver Jul 17, 2026
bf51685
Merge branch 'master' into feat/copy-sub-abbrev
FordUniver Jul 17, 2026
314f1f8
Merge feat/copy-sub-abbrev into chore/copy-spelling
FordUniver Jul 17, 2026
40e1050
replace deprecated mem_setOf_eq with mem_ofPred_eq
FordUniver Jul 17, 2026
4a320e8
Merge updated feat/copy-sub-abbrev into chore/copy-spelling
FordUniver Jul 17, 2026
cb0352f
Merge updated chore/copy-spelling into chore/copy-expose
FordUniver Jul 17, 2026
1f67407
chore(Combinatorics/SimpleGraph/Copy): make UnlabeledCopy an exposed …
FordUniver Jul 17, 2026
dab7855
Merge updated chore/copy-expose into chore/copy-nat-card
FordUniver Jul 17, 2026
fe7962f
Merge updated chore/copy-nat-card into diffbase/ind-copy-count
FordUniver Jul 17, 2026
0ef8fad
Merge updated diffbase/ind-copy-count into feat/ind-copy-count
FordUniver Jul 17, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3672,6 +3672,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Hall
public import Mathlib.Combinatorics.SimpleGraph.Hamiltonian
public import Mathlib.Combinatorics.SimpleGraph.Hasse
public import Mathlib.Combinatorics.SimpleGraph.IncMatrix
public import Mathlib.Combinatorics.SimpleGraph.InducedCopy
public import Mathlib.Combinatorics.SimpleGraph.Init
public import Mathlib.Combinatorics.SimpleGraph.LapMatrix
public import Mathlib.Combinatorics.SimpleGraph.LineGraph
Expand Down
Loading
Loading