Skip to content

feat(Archive): primitivity of Langer and Zhou-6, covering structure #39686

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

Closed
RaggedR wants to merge 15 commits into from
Closed

feat(Archive): primitivity of Langer and Zhou-6, covering structure #39686

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
ccee857
feat(Combinatorics/SimpleGraph): group actions on simple graphs
RaggedR May 18, 2026
a2a5505
chore: add Action.lean to Mathlib.lean
RaggedR May 18, 2026
bca5030
feat(Combinatorics/SimpleGraph): coset graphs (Sabidussi construction)
RaggedR May 18, 2026
908c301
feat(Combinatorics/SimpleGraph): Sabidussi representation theorem
RaggedR May 18, 2026
f3269af
feat(Combinatorics/SimpleGraph): Lorimer's theorem and quotient graphs
RaggedR May 18, 2026
b4614a0
fix: drop unused GraphAction from connectionSet, add omit annotations
RaggedR May 18, 2026
1510488
doc: add docstring to sabidussiSymmetricGraph
RaggedR May 18, 2026
0ed8df1
feat(Archive): Langer graph, Tutte 12-cage, and structural equality v…
RaggedR May 21, 2026
a2a1522
doc: add visualization links for Langer graph and Tutte 12-cage
RaggedR May 21, 2026
b789e25
feat(Archive): Langer graph is a Sabidussi coset graph
RaggedR May 21, 2026
a84fa2f
feat(SimpleGraph/CosetGraph): coset projection and graph homomorphism
RaggedR May 22, 2026
817ece8
feat(Archive): primitivity of Langer and Zhou-6, covering structure
RaggedR May 22, 2026
0ecedde
[pre-commit.ci lite] apply automatic fixes
pre-commit-ci-lite[bot] May 22, 2026
8a829d4
fix: use concrete Fin 63/91 Atkinson instead of generic Fin n
RaggedR May 22, 2026
c76bfae
style: replace show with change in LangerGraph
RaggedR May 22, 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
2 changes: 2 additions & 0 deletions Archive.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,8 @@ import Archive.Imo.Imo2024Q5
import Archive.Imo.Imo2024Q6
import Archive.Imo.Imo2025Q3
import Archive.Kuratowski
import Archive.LangerGraph
import Archive.PrimitiveGraphs
import Archive.MinimalSheffer
import Archive.MiuLanguage.Basic
import Archive.MiuLanguage.DecisionNec
Expand Down
536 changes: 536 additions & 0 deletions Archive/LangerGraph.lean
View file
Open in desktop

Large diffs are not rendered by default.

Loading
Loading