Repository navigation
feat(ModelTheory): dense linear orders have quantifier elimination - #11
Open
iosephusferrum wants to merge 3336 commits into
Open
iosephusferrum wants to merge 3336 commits into
iosephusferrum wants to merge 3336 commits into
Conversation
This is to avoid conflicts with [prod_apply](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Pi.html#prod_apply) which will be used often as `Is*Apply` instances are added.
This renames Lean 3 style `coe_int` in lemma names about `Int.cast` to `intCast`. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
…y#45301) This module has a single declaration, which can be trivially moved to its singular import.
This is to avoid conflicts with [prod_apply](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Pi.html#prod_apply) which will be used often as `Is*Apply` instances are added.
This removes repeated words, such as "category category" and "will will", from comments and docstrings. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
… lemmas for rings with finite quotients (leanprover-community#45255) Several lemmas about the absolute norm of an ideal exists in two copies: one for a finite `ℤ`-module, and a primed version for a ring with finite quotients, the first one being a restatement of the second. In this PR, the primed versions are kept, under the unprimed names, and the duplicates are deprecated. Three finiteness results that had no primed version but were restatements of lemmas in the `Ring.HasFiniteQuotients` namespace are deprecated in favor of those lemmas, and their uses updated. Note that the lemmas now require `Ring.HasFiniteQuotients R` rather than `Module.Finite ℤ R`. Where only the latter is available, the missing instance can be supplied by `Ring.HasFiniteQuotients.of_module_finite`. The module docstring now advertises `Ring.HasFiniteQuotients.finite_cardQuot_le`, which is the result the finiteness statements rest on, rather than `finite_absNorm_le`, as suggested in leanprover-community#42790. Prepared with Claude Code 🤖
This removes a repeated "the" from comments and docstrings. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
…5354) This fixes code spans in docstrings with a missing or misplaced backtick. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
This fixes misspellings in comments and docstrings, such as `coerssion`, `namescape` and `nonarchemidean`. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
…r-community#45356) This PR moves the batteries-pr-testing status comment out of `test_lint` into a new `batteries_pr_comment` job, together with the `mathlib-nightly-testing` App token that posts it, to keep credentials out of the build and test jobs. - `batteries_pr_comment` `needs: [build, test_lint]`, runs on `ubuntu-latest` with `contents: read`, checks out only this workflow's own local actions, and reads every build/test/lint outcome from the two jobs' outputs. - It posts only when `test_lint` succeeded or failed. A run cancelled before `test_lint` starts records that job as `cancelled`, not `skipped`, so a looser condition would post a comment and reset the labels on every superseded run. - The token is limited to `pull-requests: write`, which is all the labels and the comment need. - The mathlib-ci checkout only provided the comment script, so it moves to the new job too, and `test_lint` no longer needs it.
…s of ideal classes (leanprover-community#45217) In a Dedekind domain, every ideal class contains an integral ideal coprime to a given nonzero ideal. :robot: This PR was extracted from the [SKW project](https://github.com/xroblot/SKW) by Claude.
…community#45321) This PR tightens the checks in the workflows triggered by `workflow_run`, so that they now also check the triggering run's event and repository. `export_crossrefs.yml`, `nightly_detect_failure.yml` and `update_dependencies_zulip.yml` now act only on runs for pushes to this repository. `export_telemetry.yaml` also follows the fork CI, whose runs come from other repositories, so it accepts runs for `push` and `pull_request_target` events only, the two events our CI workflows use. The concurrency groups of `export_crossrefs.yml` and `nightly_detect_failure.yml` now include the head repository. Runs that these workflows skip then never share a group with the real ones, so they can't cancel them. `export_crossrefs.yml` also checks that the built commit is on the master **branch** and not a merely a tag named `master`. It is also split into 3 jobs, like `update_dependencies.yml` in leanprover-community#44881: - `export` runs the Lean code with only `contents: read` and no cache access, and uploads `crossrefs.json` as an artifact. - `publish` gets the `crossref-exports` environment and the app token, and runs no code from the checkout. - `report_failure` posts the Zulip message when either job fails. `update_dependencies_zulip.yml` now passes the `parse_changes` output to its scripts through `env` instead of writing it into the script text. `monitor-success` also gets the same repository check as `monitor-failures`. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
This PR stops using the Actions cache in this repository, and adds a check to `actionlint.yml` that keeps it that way. Entries in the Actions cache saved by runs on the default branch potentially affect runs on every other ref that fall back to them. GitHub already stops runs of low-trust triggers such as `pull_request_target` from saving such entries, unless a workflow asks for `cache-mode: write`. But the two jobs that still restored from the cache open or push to pull requests, so it's simpler for them not to depend on it at all. - `rm_set_option.yml` now uses an artifact instead. The restore step takes it only from earlier runs of this workflow on master started by the schedule or by hand, since pull requests can also start runs of this workflow file and upload artifacts from them. - `lint_and_suggest_pr.yml` no longer caches pre-commit's hook environments, which only take a few seconds to set up anyways. - `rm_set_option.yml`, the autofix job of `lint_and_suggest_pr.yml`, and the `report` job of `olean_report.yaml`, which handles PR content, set `cache-mode: none`. GitHub then refuses them any cache access, even from actions that use the cache internally. - The new `no-actions-cache` job fails if anything under `.github/` uses `actions/cache`, turns on an action's `cache` input, uses `leanprover/lean-action` without `use-github-cache: false`, or asks for any `cache-mode` other than `read` or `none`. - `.github/actionlint.yml` now also ignores the unknown `cache-mode` key in `.yaml` workflows, and `docs/workflows.md` mentions the new check.
…nity#45349) According to the naming convention, `True` and `False` need to be decapitalized in theorem names. This PR ensures this rule is followed in mathlib.
…munity#45281) Add some lemmas about the trace and the norm in `QuadraticAlgebra R a b`: the norm of `r • z` is `r ^ 2 * norm z`, and four times the norm of `z` is `trace z ^ 2 - discr a b * z.im ^ 2`. Also add that the discriminant of integer parameters is `0` or `1` modulo `4`, and a characterisation of `IsIntegralClosure A R B` when `A` acts faithfully on `B`. These are used in a later PR to determine when `QuadraticAlgebra ℤ a b` is the integral closure of `ℤ` in `QuadraticAlgebra ℚ a b`. Prepared with Claude Code 🤖
…5358) This PR updates the Mathlib dependencies. It is not merged automatically: a maintainer should look at what the new dependency revisions bring in before sending it to bors.
…eanprover-community#41459) Add MulOpposite monoid equivalences for submonoids and subgroups, and remove the corresponding TODOs in `Subsemiring/MulOpposite.lean`. Co-authored-by: Ezequiel <ezequiel.es608@gmail.com>
…eanprover-community#42693) Adds `IsGδ.polishSpace`: a Gδ subset of a Polish space is Polish, which strengthens the existing IsOpen.polishSpace. The proof follows the outline in Anush Tserunyan's descriptive set theory notes, https://www.math.mcgill.ca/atserunyan/Teaching_notes/dst_lectures.pdf where it is attributed to A. Bernshteyn. The "usual" approach (as in Kechris's Classical Descriptive Set Theory) constructs a complete compatible metric (the "Alexandrov metric"). The approach taken here is snappier to formalize - the idea is to give a closed embeddding from the G\delta set into another Polish space, and appeal to the fact closed subsets of Polish spaces are Polish. [Note the Alexandrov metric is recoverable from the embedding via the induced complete metrics on the product topology.]
This PR: - ensures all files in `Mathlib/RingTheory` have one and only one H1 header, - better aligns some H2 headers with the style guide. For files missing a module header, new headers were authored by Claude Opus 5.
…l` tactic (leanprover-community#45178) This PR adds a `Real.exp` extension for `dyadic_interval`. Co-authored-by: raoxiaojia <raoxiaojia@gmail.com>
…community#45365) This fixes misspellings in comments and docstrings that are missing a letter, such as `assumtions`, `coefficents` and `isomophism`. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
…mmunity#45366) This fixes misspellings in comments and docstrings that have an extra letter, such as `auxilliary`, `crystrallographic` and `somethimes`. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
…mmunity#45367) This fixes misspellings in comments and docstrings that have a wrong letter, such as `commatative`, `seperate` and `superceded`. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
This PR removes some unused imports from the overlapping instances linter and unused instances in type linter. This reduces the longest pole.
…ectangles (leanprover-community#26479) In this PR, we prove versions of the Cauchy-Goursat theorem where the contours in question are rectangular and unbounded (ie, where the contours look like the $\bigsqcup$ symbol). I am not sure if I have formalised these in the best way, or if `Analysis.Complex.CauchyIntegral` is the best place for them (it might be prudent to reorganise the file into multiple files at some point), but I believe this is a useful result. Suggestions welcome. Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
…anprover-community#40448) We generalise the tower law for `Module.rank` to the situation of a module over an algebraic extension of domains. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
… Hausdorff measure (leanprover-community#41839) This PR proves some properties of preconnected subsets of an extended metric space in terms of their Hausdorff measure. - The extended diameter of a preconnected set is at most its one-dimensional Hausdorff measure - A preconnected set with finite `d`-dimensional Hausdorff measure for some `d < 1` is a subsingleton, so any set with finite such measure is totally disconnected - A preconnected set with finite one-dimensional Hausdorff measure is totally bounded. The main tool is that the distance from a fixed base point is `1`-Lipschitz (we define it by `x => (edist a x).toReal` and `ENNReal.toReal` is necessary because `ℝ≥0∞` is not an EMetric space and blocks me from using `LipschitzOnWith`, this is also the reason why I proved some weird lemmas like `isClopen_setOf_edist_ne_top` and `IsPreconnected.edist_ne_top`), so it does not increase Hausdorff measures, and the image of a preconnected set under it is an interval whose one-dimensional Hausdorff measure is its length. Comparing the two turns distances inside the set into lower bounds for its measure. Some of these lemmas probably should belong to a different space. Feel free to give me some suggestions on this. In the future, I would also like to use results in this PR to prove that a preconnected, compact subset with finite one-dimensional Hausdorff measure is path-connected, and this is included in TODO. Created with the help of Claude Code, carefully reviewed and golfed by myself. Co-authored-by: Yongxi Lin <aaronlin@andrew.cmu.edu>
… topological spaces (leanprover-community#41918) In this PR we prove that 1. `isTopologicalBasis_isOpen_ordConnected`: in a linearly ordered topological space, every point of an open set `U` has an open `Set.OrdConnected` neighbourhood contained in `U`. 2. `countable_setOf_isolated_subtype`: in a separable linearly ordered topological space, the points of a subset `s` that are isolated in the subspace `s` form a countable set. 3. A subset of a separable linearly ordered topological space is separable in the subspace topology. This is proved as an instance. The material was developed for showing the measurability of the pathwise variation of a continuous stochastic process in RemyDegenne/brownian-motion#494. Created with the help of Claude Code, carefully reviewed and golfed by myself. Co-authored-by: Yongxi Lin <aaronlin@andrew.cmu.edu>
…munity#42265) Golf the proof of `coeff_inv_aux` by rewriting with `lt_iff_le_not_ge` so that the simp lemma `Finsupp.single_le_iff` can fire in the subsequent simp call.
…mas (leanprover-community#38193) Following the PR leanprover-community#38489, this PR add deprecated tags to the original `ENNReal` lemmas and change the transitive children files to use the generalized lemmas rather than the deprecated lemmas. Related Zulip thread: [#Is there code for X? > Summing `ENat`s without topology](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Summing.20.60ENat.60s.20without.20topology/with/588756615)
…er-community#44933) `simp` lemmas for `(A + B).row` and similar expressions, and bundled forms of `row`/`col` as `Equiv`/`AddEquiv`/`LinearEquiv`. Also fixes lots of places that should use `row`/`col` but don't.
... and `OrderIso.prodUnique`, `OrderIso.uniqueProd`. These all follow the existing `Equiv` definitions.
…lemma (leanprover-community#45260) Used in the CGT repo.
…hTop` (leanprover-community#45402) This PR moves the material on `sSup` and `sInf` on `WithTop α` and `WithBot α` from `Order/ConditionallyCompleteLattice/Basic` and `Order/ConditionallyCompleteLattice/Indexed` to a new file `Order/ConditionallyCompleteLattice/WithTop`. This material was scattered over five places in the two files, although the rest of these files does not depend on it.
…-community#45503) Split from leanprover-community#44287 using ChatGPT 5.5.
…pe.map` (leanprover-community#45511) and tag the matching `Set.inclusion` lemma as `@[simp]`.
Golf the 9th longest proof in mathlib by over 100 lines! mainly from deduplicating (originally from mathlib3 and got no review comments leanprover-community/mathlib3#13850 Co-authored-by: Batixx <s59fpern@uni-bonn.de>
…over-community#45499) This PR adds certain idempotent elements that capture the equalizer of two algebra homomorphisms from an unramified extension of rings. Mostly written by hand, but I got some help with `equalizerIdempotent_mul_eq_iff`. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
….equivFinRank` (leanprover-community#44597) Deprecate `NumberField.mixedEmbedding.fundamentalCone.equivFinRank`, a copy of `NumberField.Units.equivFinRank`, and use the latter in `NormLeOne.lean`.
Support Batteries adaptations as ordinary Mathlib PRs from `mathlib4-adaptations`. - Allow full commit pins during PR tests. Bors still requires stable dependency references. - Reuse `lean-pr-testing-comments.sh` in a separate job with the `mathlib-adaptations-status` App. Preserve status comments, labels, and `awaiting-mathlib` notifications. - Skip reports for superseded Mathlib commits or outdated Batteries pins. Keep push builds and status reports for existing adaptations in `mathlib4-nightly-testing`, with their current App. This lets this PR merge before Batteries leanprover-community#2049. TODOs mark the temporary reporting job and documentation for removal after those adaptations move. Validation: CI's Actionlint passes for the shared workflow and all five callers. The restored job matches the existing reporting behavior. Live validation is pending. - [x] depends on: leanprover-community/mathlib-ci#95 Prepared with Codex.
…er-community#45390) This PR adds certain idempotent elements that exist when a group acts on an unramified extension of rings. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
…5044) - The `header` doesn't fire on import-only files any more, so need not be disabled there. - One comment is obsolete, as the linter has also been fixed. - Another option is superfluous; two more are easy to fix.
leanprover-community#45580) The map `G/N →* H/M` induced by `f : G →* H` is injective iff `M.comap f ≤ N`.
…#45606) Remove numerous `backward.isDefEq.respectTransparency false` flags and other tech debt in the modular forms library.
…nity#45622) Simplify the proof of prime avoidance Co-authored-by: Batixx <s59fpern@uni-bonn.de>
…able (leanprover-community#45597) This PR adds a `Countable (α ⧸ s)` instance (as `QuotientGroup` is not instance-reducible).
…ontinuous_toFun` (leanprover-community#45600) This is just a bit of code hygiene that arose during the creation of the linter for numeric projections.
…nprover-community#43233) This PR adds the Wiener–Ikehara Tauberian theorem (`WienerIkehara` / `tendsto_sum_div` and friends) in `Mathlib/NumberTheory/LSeries/WienerIkehara.lean`, the analytic engine behind the (weak) prime number theorem. This theorem gives an asymptotic for `∑ n ∈ .Icc 0 ⌊x⌋₊, f n` for nonnegative `f` provided that `LSeries f` admits a continuous extension to `{s | 1 ≤ s.re}` after removing a simple pole at `s=1`. Mathematically, an advantage of this theorem is that no bounds on `LSeries f` are required at all; continuity (after removing the pole) is the only hypothesis. The disadvantage is that the conclusion is purely qualitative: no rate of convergence can be extracted. This result gives the weak prime number theorem (in both von Mangoldt and Mobius forms) quite easily, as well as a version in arithmetic progressions, using existing Mathlib support for Riemann zeta and Dirichlet L-functions. This will be done in a separate PR. Co-authored-by: Terence Tao <tao@math.ucla.edu> Co-authored-by: Terence Tao <teorth@gmail.com>
…ver-community#43273) In this PR, we develop some API for the order of vanishing of rational functions on schemes. We also change the file structure of order of vanishing in algebraic geometry to more closely mirror that of the ring theoretic order of vanishing results. Co-authored-by: Raph-DG <raphaeldouglasgiles@gmail.com>
…nity#45615) - `Finset.Iic_one : Iic (1 : α) = {1}` for `IsBotOneClass α`, and its additive version `Finset.Iic_zero`, both `simp`.
…e issue (leanprover-community#44890) leanprover-community#34083, adding `Set.indicator_singleton`, made simp non-confluent: the following example fails on current master: ``` import Mathlib.MeasureTheory.Measure.Haar.OfBasis example : ({0} : Set ℝ).indicator 1 =ᵐ[MeasureTheory.volume] (0 : ℝ → ℝ) := by simp [-Set.indicator_singleton, Filter.EventuallyEq, MeasureTheory.ae_iff] ``` Add a simp lemma to resolve this issue. Co-authored-by: Leopold Mayer <leomayer@uw.edu> Co-authored-by: Leopold Mayer <leopoldmayer1998@gmail.com>
…eanprover-community#45091) While reviewing the graph API, I noticed that the proof of ``` Connected.induce_compl_singleton_of_degree_eq_one ``` can be shortened using ``` Preconnected.induce_of_degree_eq_one (s := {v}ᶜ) ``` The unique neighbor handles nonemptiness. This removes the duplicate proof and moves the lemma from `Acyclic` to `Connectivity.Connected`. No API changes required, and the lemma can be imported without `Acyclic`.
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
…leanprover-community#45616) The option type is (un)countable if and only the type is (un)countable. Before merging leanprover-community#39567 , @felixpernegger suggested proving the analogous result for countable and uncountable types. Here is the PR for such results. Co-authored-by: AlexBrodbelt <apbrodbelt@gmail.com>
…tifier-elimination-dlo
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
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.
6