feat(Combinatorics/Enumerative): Latin squares#36698
Open
ghseeli wants to merge 4024 commits into
Open
Conversation
…ma for disambiguation (leanprover-community#34413) Cherry picked from leanprover-community#34055. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…ation and variance (leanprover-community#33815) Make mathlib's style consistent by always putting spaces around the pipes. This is more readable when there are long arguments. This inconsistency was exposed by extending the `whitespace` linter to proof bodies in leanprover-community#30658.
…munity#34439) Discovered in leanprover-community#24343. Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
Define a predicate `HasGaussianLaw X P`, which states that under the measure `P`, the random variable `X` has a Gaussian distribution, i.e. `IsGaussian (P.map X)`.
…ity#34139) This PR adds an API lemma specializing `comap_iInf` to the case of finsets, which I've found helpful for working with primary decomposition. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
…nprover-community#34203) These were forgotten in leanprover-community#33873.
…community#34438) Cherry picked from leanprover-community#34055. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…olynomial.Degree.Defs` (leanprover-community#34449) `Defs` is the standard name for files mainly containing definitions.
…sIso_desc` and golf (leanprover-community#34237) We also fix the name of `Cofan.isColimit_iff_isIso_sigmaDesc` and turn the `iff` around.
…mmunity#34429) These lemmas work if the codomain is a `MulOneClass`, not necessarily a group.
…27701) ...and analogous results on `CanonicallyOrderedAdd`.
…ver-community#34457) ... and remove as many explicit proofs as possible.
…easure.join` (leanprover-community#34239) Add some small results which were apparently missing: * `join` and `bind` give probability measures if fed with probability measures * `join` and `bind` interchange with `sum`, `bind` interchanges with `smul` Co-authored-by: pfaffelh <p.p@stochastik.uni-freiburg.de> Co-authored-by: pfaffelh <pfaffelh@gmail.com>
…r-community#34358) This is renamed as `Fan.IsLimit.lift`.
…nprover-community#34353) The statement has a nice generalisation which doesn't use tuples, and allows easy expression of a few useful variants. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
…anprover-community#34468) When verify_version_tags.py is run from lean4's release_checklist.py, it runs in a shallow clone without tags. The local/remote consistency check would return a warning in this case, causing the script to exit with code 1 in single-tag mode (where warnings are treated as failures). This scenario is explicitly expected (as the existing comment noted), and the GitHub API check verifies the tag exists remotely. Treat this as a successful skip rather than a warning. Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
…finite sequences of paths (leanprover-community#28208) Add `Path.concatenate`, which folds the function `Path.trans` across a sequence of paths with compatible endpoints, corresponding to the concatenation of a finite sequence of paths. This is implemented with `Fin.dfoldl` from the Batteries library. Prove basic properties about `concatenate` (i.e., how it behaves with respect to `Path.refl`, `Path.subpath`, and homotopies).
…er-community#34286) This PR addresses all shellcheck warnings in `scripts/create-adaptation-pr.sh`: - Quote variables to prevent globbing/word splitting ([SC2086](https://www.shellcheck.net/wiki/SC2086)) - Use `$(...)` instead of legacy backticks ([SC2006](https://www.shellcheck.net/wiki/SC2006)) - Add `-r` flag to `read` commands ([SC2162](https://www.shellcheck.net/wiki/SC2162)) **Related PRs:** - leanprover/cslib#203 (cslib) - leanprover-community/batteries#1624 (batteries) 🤖 Prepared with Claude Code
…rover-community#34398) This PR fixes a bug in the `nightly_detect_failure.yml` workflow where duplicate messages were being posted to Zulip for the same nightly date. The deduplication logic compared the first 160 characters of the message, but the GitHub Actions run ID appears within those characters. Different workflow runs have different IDs, so the comparison always failed and duplicates were posted. Now we extract and compare the nightly date and bump branch explicitly using regex, which correctly identifies duplicate messages. **Update:** Also now fetches the last 20 messages and looks for the most recent one from the bot, ignoring human replies in between. This handles the case where someone replies to a bot message before the next workflow run. See https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Cslib.20bump.20branch.20reminders/near/569853848 for context. Suggested improvement by Chris Henson: https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Cslib.20bump.20branch.20reminders/near/569945200 🤖 Prepared with Claude Code
The current definition of `Quiver` allows morphisms to be in `Prop`. The docstring explicitly mentions that if you want to use Props as morphisms, you can do this with `Quiver.{0}`. But in fact there are only two occurrences of the string `Quiver.{0}` in mathlib, one in the docstring of `Quiver`, and one in the docstring of `Digraph` explaining why `Quiver.{0}` was not suitable for digraphs (because `Quiver` is a class); the definition of `Digraph` is precisely `Quiver.{0}` but as a structure. In contrast, there are many many occurrences of `Quiver.{v + 1}` in mathlib, all of which can be removed with this refactor.
It turns out that there is actually one `Quiver.{0}` in Mathlib: `Matrix.toQuiver` associates a Prop-valued quiver to a matrix with entries in a linearly ordered ring. There are two possible fixes here; I use `PLift` which was the easier one; another possibility is to make `Matrix.toDigraph` instead.
Define gaps of a finite set of pairwise disjoint closed intervals. Part of originally planned leanprover-community#29508
…`f v - f u` (leanprover-community#34462) Cherry picked from leanprover-community#34055. It is the first step of the construction of the vector measure associated to a bounded variation function: later, we will extend the finite additivity given by the current PR to countable additivity thanks to general extension theorems for vector measures. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…over-community#34052) Adds `Fintype.not_injective_of_card_lt`, the contrapositive of `card_le_of_injective`. This provides a direct pigeonhole-style statement that a function cannot be injective when the codomain is smaller than the domain. Moved from `Mathlib.Data.Fintype.Pigeonhole` to sit next to `card_le_of_injective` in `Mathlib.Data.Fintype.Card`.
…leanprover-community#34480) This PR fixes the daily CI workflow for leanchecker. The `check-leanchecker` job was configured to run only in `mathlib4-nightly-testing`, but the `notify-leanchecker` job runs in `mathlib4` and tries to query the job status from the current workflow run. Since the job was skipped in `mathlib4`, the notification produced broken Zulip messages with empty URLs (see https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/leanchecker.20failure/near/570212817). This PR: - Moves `check-leanchecker` to run in `mathlib4` (matching `check-nanoda` and `check-mathlib_test_executable`) - Enables both `master` and `nightly` branches for leanchecker (the TODO comment indicated this was waiting for leanchecker to land on master) 🤖 Prepared with Claude Code
…nity#30831) We define the quasi-compact precoverage on the category of schemes as the precoverage given by quasi-compact covers. From this, the fpqc precoverage is obtained in a follow-up PR as the intersection of this precoverage with the precoverage given by flat covers. From Proetale.
…prover-community#32316) In this PR we present some dimension shifting tools in `ModuleCat`.
Co-authored-by: Christopher J. R. Lloyd <cjl8zf@virginia.edu> Co-authored-by: George H. Seelinger <ghseeli@gmail.com>
…rd_succ' into lr_ls_m_coe
Co-authored-by: Christopher J. R. Lloyd <cjl8zf@virginia.edu> Co-authored-by: George H. Seelinger <ghseeli@gmail.com>
Co-authored-by: Christopher J. R. Lloyd <cjl8zf@virginia.edu> Co-authored-by: George H. Seelinger <ghseeli@gmail.com>
Co-authored-by: Iván Renison <85908989+IvanRenison@users.noreply.github.com>
Thanks for this! Co-authored-by: Iván Renison <85908989+IvanRenison@users.noreply.github.com>
…image_of_card_succ
Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
…rd_succ' into lr_ls_m_coe
As suggested by @dagurtomas.
Co-authored-by: Christopher J. R. Lloyd <cjl8zf@virginia.edu> Co-authored-by: George H. Seelinger <ghseeli@gmail.com>
ghseeli
temporarily deployed
to
cache-upload-forks
GitHub Actions
Inactive
Placed it lower in the file so it can use dependent lemmas in proof. Co-authored-by: Christopher J. R. Lloyd <cjl8zf@virginia.edu> Co-authored-by: George H. Seelinger <ghseeli@gmail.com>
Co-authored-by: Christopher J. R. Lloyd <cjl8zf@virginia.edu> Co-authored-by: George H. Seelinger <ghseeli@gmail.com>
ghseeli
temporarily deployed
to
cache-upload-forks
GitHub Actions
Inactive
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
Bot
removed
the
merge-conflict
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
20 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.
This PR defines Latin rectangles and Latin squares and proves an extension theorem using Hall's Marriage Theorem.
Main results
group_to_cayley_table: every finite groupGyields aLatinSquare G G.latin_rectangle_extends_one_row: a (non-square)LatinRectangleextends to aLatinRectanglewith one more row. This is an application of Hall's Marriage Theorem,
hallMatchingsOn.nonempty.latin_rectangle_extends_to_latin_square: aLatinRectangleextends to aLatinSquare.This is included in a new file
Combinatorics/Enumerative/LatinSquare.lean.