-
Notifications
You must be signed in to change notification settings - Fork 13
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
68 changed files
with
1,475 additions
and
2,035 deletions.
There are no files selected for viewing
This file was deleted.
Oops, something went wrong.
This file contains 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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,116 @@ | ||
| on: | ||
| push: | ||
| branches: | ||
| - master | ||
|
|
||
| # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages | ||
| permissions: | ||
| contents: read | ||
| pages: write | ||
| id-token: write | ||
|
|
||
| jobs: | ||
| style_lint: | ||
| name: Lint style | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Check for long lines | ||
| if: always() | ||
| run: | | ||
| ! (find LeanCamCombi -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://') | ||
| - name: Don't 'import Mathlib', use precise imports | ||
| if: always() | ||
| run: | | ||
| ! (find LeanCamCombi -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$') | ||
| build_project: | ||
| runs-on: ubuntu-latest | ||
| name: Build project | ||
| steps: | ||
| - name: Checkout project | ||
| uses: actions/checkout@v2 | ||
| with: | ||
| fetch-depth: 0 | ||
|
|
||
| - name: Print files to upstream | ||
| run: | | ||
| grep -r --exclude-dir=ExampleSheets --files-without-match 'import LeanCamCombi' LeanCamCombi | sort > 1.txt | ||
| grep -r --exclude-dir=ExampleSheets --files-with-match 'sorry' LeanCamCombi | sort > 2.txt | ||
| mkdir -p docs/_includes | ||
| comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/YaelDillies\/LeanCamCombi\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md | ||
| rm 1.txt 2.txt | ||
| - name: Count sorries | ||
| run: | | ||
| python scripts/count_sorry.py | ||
| - name: Install elan | ||
| run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0 | ||
|
|
||
| - name: Get cache | ||
| run: ~/.elan/bin/lake -Kenv=dev exe cache get || true | ||
|
|
||
| - name: Build project | ||
| run: ~/.elan/bin/lake -Kenv=dev build LeanCamCombi | ||
|
|
||
| - name: Cache mathlib docs | ||
| uses: actions/cache@v3 | ||
| with: | ||
| path: | | ||
| .lake/build/doc/Init | ||
| .lake/build/doc/Lake | ||
| .lake/build/doc/Lean | ||
| .lake/build/doc/Std | ||
| .lake/build/doc/Mathlib | ||
| .lake/build/doc/declarations | ||
| key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} | ||
| restore-keys: | | ||
| MathlibDoc- | ||
| - name: Build documentation | ||
| run: ~/.elan/bin/lake -Kenv=dev build LeanCamCombi:docs | ||
|
|
||
| # - name: Build blueprint and copy to `docs/blueprint` | ||
| # uses: xu-cheng/texlive-action@v2 | ||
| # with: | ||
| # scheme: full | ||
| # run: | | ||
| # apk update | ||
| # apk add --update make py3-pip git | ||
| # apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev | ||
| # git config --global --add safe.directory $GITHUB_WORKSPACE | ||
| # git config --global --add safe.directory `pwd` | ||
| # python3 -m pip install --upgrade pip requests wheel | ||
| # python3 -m pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/" | ||
| # pip install -r blueprint/requirements.txt | ||
| # python3 -m pip install invoke | ||
| # inv all | ||
|
|
||
| - name: Copy documentation to `docs/docs` | ||
| run: | | ||
| mv .lake/build/doc docs/docs | ||
| - name: Bundle dependencies | ||
| uses: ruby/setup-ruby@v1 | ||
| with: | ||
| working-directory: docs | ||
| ruby-version: "3.0" # Not needed with a .ruby-version file | ||
| bundler-cache: true # runs 'bundle install' and caches installed gems automatically | ||
|
|
||
| - name: Bundle website | ||
| working-directory: docs | ||
| run: JEKYLL_ENV=production bundle exec jekyll build | ||
|
|
||
| - name: Upload docs & blueprint artifact | ||
| uses: actions/upload-pages-artifact@v1 | ||
| with: | ||
| path: docs/_site | ||
|
|
||
| - name: Deploy to GitHub Pages | ||
| id: deployment | ||
| uses: actions/deploy-pages@v1 | ||
|
|
||
| - name: Make sure the cache works | ||
| run: | | ||
| mv docs/docs .lake/build/doc |
This file contains 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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,10 +1,11 @@ | ||
|
|
||
| *.olean | ||
| /_target | ||
| /.lake | ||
| /doc-gen | ||
| /build | ||
| /leanpkg.path | ||
| /lake-packages | ||
| /leanpkg.path | ||
|
|
||
| decls.pickle | ||
| decls.yaml | ||
|
|
||
This file contains 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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,8 +1,10 @@ | ||
| # This is run when starting a Gitpod workspace on this repository | ||
|
|
||
| image: leanprovercommunity/mathlib:gitpod | ||
|
|
||
| vscode: | ||
| extensions: | ||
| - jroesch.lean | ||
| - leanprover.lean4 # install the Lean 4 VS Code extension | ||
|
|
||
| tasks: | ||
| - command: . /home/gitpod/.profile && scripts/get_cache.sh | ||
| - command: . /home/gitpod/.profile && lake exe cache get # Download cache |
This file was deleted.
Oops, something went wrong.
This file contains 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
This file contains 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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,37 @@ | ||
| /- | ||
| Copyright (c) 2023 Yaël Dillies. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Yaël Dillies | ||
| -/ | ||
| import Mathlib.GroupTheory.SpecificGroups.Cyclic | ||
| import LeanCamCombi.Mathlib.Data.Finset.Pointwise | ||
| import LeanCamCombi.Kneser.Kneser | ||
|
|
||
| /-! | ||
| # The Cauchy-Davenport theorem as a corollary of Kneser's lemma | ||
| This file proves the Cauchy-Davenport theorem as a corollary of Kneser's lemma. | ||
| ## Main declarations | ||
| * `ZMod.min_le_card_add'`: The Cauchy-Davenport theorem. | ||
| ## Tags | ||
| additive combinatorics, number theory, sumset, cauchy-davenport | ||
| -/ | ||
|
|
||
| open Finset | ||
| open scoped Pointwise | ||
|
|
||
| /-- The **Cauchy-Davenport Theorem**. -/ | ||
| lemma ZMod.min_le_card_add' {p : ℕ} (hp : p.Prime) {s t : Finset (ZMod p)} (hs : s.Nonempty) | ||
| (ht : t.Nonempty) : min p (s.card + t.card - 1) ≤ (s + t).card := by | ||
| haveI : Fact p.Prime := ⟨hp⟩ | ||
| obtain h | h := eq_bot_or_eq_top (AddAction.stabilizer (ZMod p) (s + t)) | ||
| · refine' min_le_of_right_le _ | ||
| rw [← AddSubgroup.coe_eq_zero, ← coe_addStab (hs.add ht), coe_eq_zero] at h | ||
| simpa [*] using add_kneser s t | ||
| · rw [← AddSubgroup.coe_eq_univ, ← coe_addStab (hs.add ht), coe_eq_univ] at h | ||
| refine' card_addStab_le_card.trans' _ | ||
| simp [*, card_univ] |
Oops, something went wrong.