benchmark leanprover/lean4#13895 adaptation branch#232
Merged
Conversation
Author
|
!bench |
|
Benchmark results for 19fb046 against 8a9ccb2 are in. There are significant results. @datokrat
Large changes (2✅, 1🟥)
Medium changes (7✅, 5🟥)
Small changes (31✅, 33🟥) Too many entries to display here. View the full report on radar instead. |
Author
|
!radar |
|
Benchmark results for e18d7e2 against 1cdfd83 are in. No significant results found. @datokrat Warning These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.
No significant changes detected. |
Author
|
!radar |
|
Benchmark results for 666fc21 against 1cdfd83 are in. No significant results found. @datokrat Warning These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.
No significant changes detected. |
… is complemented (leanprover-community#41033) On the road towards Fredholm operators
…nity#41008) ... over a noetherian ring. Also, over an arbitrary ring, a submodule codisjoint from a fg module is cofg. This is a prerequisite for Fredholm operators.
…prover-community#41025) Discovered while working on leanprover-community#36036.
…ver-community#38317) In this PR, I add some lemma about choose of prime pow. 1) For primes `p` and positive integer `n`, assume that for all `i ∈ Icc 1 (n - 1)`, `choose n i` congruent to `0` module `p`, then `n = p ^ multiplicity p n`. 2) For a prime power `n`, the greatest common divisor of `choose n 1, ⋯, choose n (n - 1)` is actually the minimal prime factor of `n`. 3) For a natural number `n` greater than `1`, assume that `n` is not a prime power, then the greatest common divisor of `choose n 1, ⋯, choose n (n - 1)` is `1`. Co-authored-by: WenrongZou <wenrongzou@outlook.com>
… under isomorphisms (leanprover-community#41036) This is only the translation of this statement in terms of some `ObjectProperty` in functor categories.
datokrat
force-pushed
the
lean-pr-testing-13895
branch
from
83622cf to
7017dc0
Compare
…y#37901) In this PR we define the notion of algebraic cycles on a scheme, and define the pushforward of an algebraic cycle by a quasicompact morhphism. This was originally defined in leanprover-community#26304, but after some refactoring it was decided that it would be best to split this definition into a separate PR. Co-authored-by: Raph-DG <raphaeldouglasgiles@gmail.com>
…r-community#40976) Generalize both interval-version Lebesgue differentiation theorems `LocallyIntegrable.ae_hasDerivAt_integral` and `IntervalIntegrable.ae_hasDerivAt_integral` from real-valued functions `f : ℝ → ℝ` to functions `f : ℝ → E` valued in a Banach space `E`. The existing proof already goes through the vector-valued averaging theorem `VitaliFamily.ae_tendsto_average`, so the only change is replacing scalar multiplication `*` by `•` in the slope computation. This is a prerequisite for leanprover-community#40973. AI usage disclosure: I used Claude Opus 4.8 to implement this and manually tested it with the other PR and my other separate project.
…ommunity#40986) Remove a duplicate lemma and generalize some lemmas to support two different codomains.
datokrat
force-pushed
the
lean-pr-testing-13895
branch
from
7017dc0 to
385ae40
Compare
…#40919) This can in future replace a similar lemma for `RingQuot`. The old copyright is because this was derived from `Mathlib/Algebra/Star/RingQuot.lean`.
Implement tactic for proving equality of polynomials. This tactic is part of a larger suite (see leanprover-community#30374). Also generalize the preprocessing step for `algebra` so that it always replaces `algebraMap R A r` with `r • 1` instead of only when `R` is `Nat` or `Int`. This was an oversight in `algebra` that broke `polynomial`. - [x] depends on: leanprover-community#31508
…anprover-community#38667) - `OrderHom`s are equivalent to `RelHom`s of `LE` (unlike `OrderEmbedding`/`OrderIso` they aren't defined using it) - Congruence equivs for `OrderEmbedding`/`OrderIso` when the two sides are order-isomorphic. This already exists for `OrderHom`.
…eanprover-community#41041) These probably became non-`noncomputable` with the new compiler.
…1044) This PR updates the Mathlib dependencies.
From flt-regular.
…a quotient preadditive category (leanprover-community#41067) Prove that, if `F : C ⥤ D` is an additive essentially surjective functor between preadditive categories and `C` has finite products, then `D` also has finite products. Use this to shorten the proof that the localization of an abelian category by a Serre class has finite products (in `CategoryTheory/Abelian/SerreClass/Localization`). Co-authored-by: morel <sophie.morel@ens-lyon.fr>
…eanprover-community#39625) Generalize `coeff_trunc_mul_trunc_eq_coeff_mul` (and its analogs for `truncFinset` and `trunc'`) to allow for different truncation levels for the two arguments. This matches the API for univariate power series, where we already have `PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc₂`. This is useful for defining partial derivatives of multivariate power series, see PR leanprover-community#39626. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
…er-community#40170) A few factorization lemmas, including: - `∀ n : ℕ`, `n ∣ radical n ^ n` - `∀ n k : ℕ`, `n ∣ k ^ n ↔ n.primeFactors ⊆ k.primeFactors` - `∀ n k : ℕ`, `radical n ∣ k ↔ n.primeFactors ⊆ k.primeFactors` - In any `UniqueFactorizationMonoid M`, `∀ a : M`, `∃ n, a ∣ radical a ^ n` [#Is there code for X? > A number divides a power of its square-free component](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/A.20number.20divides.20a.20power.20of.20its.20square-free.20component/with/599339469)
Bumps `actions/checkout` to v7.0.0 across all workflows.
v7 refuses to check out fork-PR code under `pull_request_target`/`workflow_run` unless `allow-unsafe-pr-checkout: true` is set.
Three steps intentionally check out fork-PR code, and we already defend against the malicious case (no persisted credentials; only trusted, base-built tooling runs against the checkout), so they get the opt-in:
```
┌────────────────────────────────────────────┬──────────────────────────────────┬─────────────────────────────────────────────────────────┐
│ File │ Step │ Checked-out ref │
├────────────────────────────────────────────┼──────────────────────────────────┼─────────────────────────────────────────────────────────┤
│ .github/workflows/add_label_from_diff.yaml │ "Checkout branch to label" (L50) │ ${{ github.event.pull_request.head.sha || github.sha }} │
├────────────────────────────────────────────┼──────────────────────────────────┼─────────────────────────────────────────────────────────┤
│ .github/workflows/PR_summary.yml │ "Checkout code" (L29) │ ${{ github.event.pull_request.head.sha }} │
├────────────────────────────────────────────┼──────────────────────────────────┼─────────────────────────────────────────────────────────┤
│ .github/workflows/decls-diff.yml │ "Checkout new commit" (L67) │ ${{ steps.meta.outputs.new-sha }} │
└────────────────────────────────────────────┴──────────────────────────────────┴─────────────────────────────────────────────────────────┘
```
This reverts commit 7f60f15. cf. [#PR reviews > CI refusing to check out fork pull request code @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/CI.20refusing.20to.20check.20out.20fork.20pull.20request.20code/near/606724422)
…unity#40808) This is essentially an adapted copy of the API we already have for the Bochner integral
Bumps `actions/checkout` to v7.0.0 across all workflows. v7 refuses to check out fork-PR code under `pull_request_target` / `workflow_run` unless `allow-unsafe-pr-checkout: true` is set. Five steps intentionally check out fork-PR code in those contexts. Each is already hardened, the fork code is either built inside the landrun sandbox or run with only `contents: read`, while trust-rooted tooling is loaded from the base-repo checkout. | File | Step | Checked-out ref | Trigger | |---|---|---|---| | `.github/actions/setup-build-env/action.yml` | Checkout PR branch | `inputs.pr_branch_ref` | build_fork (`pull_request_target`) | | `.github/workflows/build_template.yml` | `post_steps` checkout | `inputs.pr_branch_ref` | build_fork (`pull_request_target`) | | `.github/workflows/PR_summary.yml` | Checkout code | `github.event.pull_request.head.sha` | `pull_request_target` | | `.github/workflows/add_label_from_diff.yaml` | Checkout branch to label | `github.event.pull_request.head.sha \|\| github.sha` | `pull_request_target` | | `.github/workflows/decls-diff.yml` | Checkout new commit | `steps.meta.outputs.new-sha` | `workflow_run` | Reapplies leanprover-community#41055 (reverted in leanprover-community#41078) leanprover-community#41055 opted in the three workflow-file steps but missed the two on the fork-build path `setup-build-env`'s `Checkout PR branch` (used by the `build` and `test_lint` jobs) and `build_template.yml`'s `post_steps` checkout.
…ced by bilinear forms (leanprover-community#40489) Given a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`, the weak topology on `E` is the coarsest topology such that for all `y : F` every map `(B · y)` is continuous; equivalently, it is the topology on `E` induced by the map `(B · · : E → (F → 𝕜))`. This file defines a `Prop`-valued typeclass `LinearMap.IsWeak` expressing that an existing topology on `E` is the weak topology. Although this could be passed around explicitly as a hypothesis `Topology.IsInducing (B · ·)`, given the ubiquity of weak topologies in functional analysis, the numerous properties that can be deduced because the inducing map `B` is bilinear, the fact that several theorems (e.g., one version of the bipolar theorem) require this hypothesis, and we can instantiate this class for several extant types in Mathlib, we choose to make this a typeclass instead. Note that establishing `LinearMap.IsWeak` before proving theorems about a particular type can help prevent abuse of definitional equalities. This because spaces equipped with a weak topology are frequently type synonyms of some other type `E'`. For example, suppose `E'` is a type (potentially with some extant topology other than the weak topology) and `B' : E' →ₗ[𝕜] F →ₗ[𝕜] 𝕜` is a bilinear form. To consider the weak topology on `E'` induced by `B'`, in practice we must create a type synonym `E` with an instance `TopologicalSpace E := .induced (B' · ·) Pi.topologicalSpace`. It would then be tempting to create theorems such as: ```lean example (y : F) : Continuous (fun x : E ↦ B' x y) := sorry ``` However, this statement contains an abuse of the the definitional equality `E := E'` since `x : E`, but `B'` has domain `E'`. Morever, one might be tempted to say that `B'.IsWeak`, but this is impossible because the domain of `B'` is `E'`, which is equipped with the incorrect topology. Instead, what one should do is to first define a new bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜` by composing `B'` with the linear equivalence between `E` and `E'`, and then establish `B.IsWeak`. If then one proves theorems about `E` using only the `LinearMap.IsWeak` API, then one can have more confidence that the statements are type correct.
…er-community#39230) I wanted to understand why these two proofs in leanprover-community#38807 were long (and also play around more with the API in this corner of the library) so I walked through them with Claude Opus. prepared with Claude code
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…r-community#41087) This aligns the API with the `Scheme` case.
…ver-community#41058) Add `RingHom.IsIntegral.kerLift` which proves that the `kerLift` of an integral ring homomorphism is integral.
…prover-community#40212) Endow the direct sum `ι →₀ X` of `ι`-many copies of a metric space `X` with the L^p metric for any `1 ≤ p < ∞`. `p = ∞` is theoretically possible too but currently annoying due to defects in our tactics/`WithTop` API. I am leaving it as future work. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/What.20topology.20on.20Finsupp.3F/with/600119738)
…by faster tactic (leanprover-community#41106) Replace `cat_disch` with `intros; ext <;> simp` in `Triangle.shiftFunctorAdd'`. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/116290-rss/topic/Significant.20commits.20to.20mathlib4/near/606901493).
…schemes (leanprover-community#39122) This is a first step (of hopefully many) towards some basic birational geometry. This PR adds `Birational/Birational.lean`, which defines predicates `Birational`, `BirationalOver` and `IsRationalOver` for arbitrary schemes and provides basic API (e.g. that they are equivalence relations, and that affine space is rational). Some notes on the choice of definitions: There are multiple ways to define what it means for two schemes to be birational to each other. A common one is: "There exists a rational map with a rational inverse". However, this would require defining composition of rational maps, which is not always defined (In order to compose `f : X ⤏ Y` with `g : Y ⤏ Z`, you need at least `X` preirreducible, `Y` nonempty and `f` dominant). On the other hand, I can define "There exist dense subsets `U : Opens X` and `V : Opens Y` such that `U ≅ V` as schemes" for any two schemes `X` and `Y`, with no conditions. Hence I chose that as a definition. I'm also working on defining composition of rational maps (leanprover-community#39445), and once that's done, there should be a theorem connecting the two definitions. - [x] depends on: leanprover-community#39316 Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
…#41089) - actions/attest-build-provenance: v4.1.0 -> v4.1.1 - actions/setup-python: v6.2.0 -> v6.3.0 - softprops/action-gh-release: v3.0.0 -> v3.0.1 - actions/cache: v5.0.5 -> v6.1.0 (ESM migration + read-only cache handling) - zulip/github-actions-zulip/send-message: v2.0.1 -> v2.0.2 - leanprover-community/privilege-escalation-bridge: v1.2.0 -> v1.3.0 - leanprover-community/gh-problem-matcher-wrap: pin to the node24 build (clears the Node 20 deprecation warning) - kim-em/github-actions-ensure-sha-pinned-actions: pin to v5.0.0 instead of a feature branch - dcarbone/install-jq-action: v3.2.0 -> v4.0.1 (default jq -> 1.8.2) actions/checkout was already bumped to v7.0.0 on master (leanprover-community#41084).
leanprover-community#40933) This is more concise (and perhaps even more efficient) than converting an existing expression to Syntax and re-elaborating that. No need for this.
Adapt for the removal of batteries' `defLemma` linter (batteries#1863),
which followed lean4#13803 moving the linter into core and renaming it
`defProp`. Mathlib's `@[nolint defLemma]` attributes are now dangling
("linter 'defLemma' not found"), breaking the build on nightly-2026-06-27.
Drop the now-invalid `@[nolint defLemma]` from the 5 affected files.
Manifest keeps nightly-testing's batteries rev (cf0b862c), which already
includes leanprover-community#1863.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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.
No description provided.