Sync upstream mathlib4 (2026-07-30, +20 commits) - #89
Merged
Merged
Conversation
Notation: - `K∞` : `NumberField.InfiniteAdeleRing K`; - `𝔸ᶠ[R, K]`: `IsDedekindDomain.FiniteAdeleRing R K`; - `𝔸[R, K]` : `NumberField.AdeleRing R K`; - specialisations `𝔸ᶠ[K]` and `𝔸[K]` to `R = RingOfIntegers K`.
…42212) Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
…es (#41978) Add the `Finite` analogue for `induction_subsingleton_or_nontrivial`.
We prove various lemmas about the `smallInductiveDimension` of a topological space, as well as interactions with the `HasSmallInductiveDimensionLT` and `HasSmallInductiveDimensionLE` typeclasses.
Inspired by #42205. I searched for ` _ _ _]` in vscode and manually went through all ~25 and see if they could be removed (and in some cases some minor style improvement). For ` _ _]` it is already over 100, so that work ought to be automatised Co-authored-by: Batixx <s59fpern@uni-bonn.de>
…ces (#42222) `inferInstance` works in place of `inferInstanceAs` in both places. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/583339-AI-authored-projects/topic/Comparator-related.20import.20subtleties/with/613349677)
…1654) The additive lemma states `(mk g).out = g + h`, so by the `to_additive` naming convention its name should end in `add`, not `mul`. Rename it to `QuotientAddGroup.mk_out_eq_add` (a copy-paste error inherited from mathlib3) and deprecate the old name.
This is just a general good practice these days. Two specific reasons are: - the module system makes thing faster, for example by reducing how much stuff has to be imported. - In the long run, we want to only support the module system, and not any non-module system uses of mathlib. #41950 signals this. That way, we can use no_expose, without needing to worry about uses without the module system where the definition will be exposed anyways. The migration is mostly mechanical, akin to what `modulize.lean` would do: make all imports `public`, and add `@[expose] public section` at the beginning of each file. (In a few cases of files without definitions, omit the expose attribute.) Inspired by #36236; re-done by hand. All files omitted there are actually fine to hand-convert.
…onway_99` (#42233) Kevin's Claude noticed that the `proof_wanted` for `conway_99` is misformalized. It asserts the existence of a simple graph `g` but then refers to the variable `G`. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
This PR deprecates `NumberTheory/RamificationInertia/Basic.lean` in favor of `RingTheory/RamificationInertia/Basic.lean`. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
…ify proofs (#42149)
This PR adds the lemma
```lean
lemma toAdd_unzero_eq_log {x : Mᵐ⁰} (hx : x ≠ 0) :
(unzero hx).toAdd = log x
```
and uses it to simplify some proofs involving `log`, `exp`, and rank-one discrete valuations.
Co-authored-by: fbarroero <fbarroero@gmail.com>
…is one (#37959) Co-authored-by: artie2000 <artem.khovanov@gmail.com>
This PR proves in `MeasureTheory.Measure.Support` that any measure which is compact-inner-regular on open sets has conull support. It also records the consequences for `[μ.InnerRegular]` on spaces with `[OpensMeasurableSpace X]` and for `[μ.Regular]`. It first proves compact subsets of `μ.supportᶜ` have measure zero, then applies `InnerRegularWRT IsCompact IsOpen`. The inner-regular and regular statements are corollaries. Created with the help of codex. Co-authored-by: Yongxi Lin <aaronlin@andrew.cmu.edu>
This PR implements a variation on the linter that was written by Claude in #41562. It suggest to use `have`/`let` instead of `haveI`/`letI` whenever the goal is a proposition. See also https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/surprising.20have.2FhaveI.20kernel.20phenomenon/with/609718493
This PR updates the Mathlib dependencies.
Addresses comments from #42114. In particular, we add docstrings for `isOpen_Ioo'` (and `isOpen_Iio'`, `isOpen_Ioi'`) and use dot notation. Co-authored-by: NoahW314 <noahwalker3.14@gmail.com>
Kevin's Claude noticed that the first two commented out `proof_wanted`s should say `LocallyLipschitzOn` (currently they are identical to the last two commented out `proof_wanted`s which say `ContinuousOn`). Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
… (#41614) Adds `Module.finrank_mul_finrank'`, a variant of the tower law `finrank R S * finrank S T = finrank R T` for a tower of domains `R → S → T`.
…ptions (#42267) This PR uses `implicit_reducible` to remove some backward options that currently block the use of `scripts/rm_set_option.py`.
See [this thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Performance.20cost.20of.20info.20tree.20traversal/with/610705175) for discussion. This prevents a confusing lack of messages for the `show` tactic introduced in #41761. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.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
17 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.
Automated daily sync from
leanprover-community/mathlib4@master.60af7185ecf32ed5cab100f9960f1d588b9a6cabAuto-merges to
masteronceCI (self-hosted)passes. Regenerateddaily until merged or until a conflict appears.
Note
Medium Risk
Large automated sync touching library structure, linters, and core Mathlib APIs; low individual change risk but broad compile/sorry surface if downstream code depends on deprecated paths or old
haveIpatterns.Overview
Daily merge of 20 commits from upstream mathlib4 (
60af7185…).Counterexamples are migrated to the modern module layout (
module,public import,@[expose] public section), with the root aggregator usingshake: keep-allanddeprecated_module: ignore.Proof style cleanup replaces
haveI/letIwithhave/letin Archive IMO/Wiedijk files and similar spots where only proof irrelevance matters. A newlinter.style.haveILetI(and high-priorityshowelaboration) suggestshave/letonPropgoals; tests live underMathlibTest/Linter/.Mathlib changes include:
WithZerolog/order lemmas viatoAdd_unzero_eq_log; measure support results for inner regular/regular measures;Module.finrank_mul_finrank'and related rank/finrank API;Nat.induction_subsingleton_or_nontrivialand a refactor of p-group nilpotence; small inductive dimension characterizations; adele notation𝔸[R,K],K∞,𝔸ᶠ[R,K]; deprecation ofNumberTheory.RamificationInertia.Basicin favor ofRingTheory.RamificationInertia.Basic; category/Over monoidal defeq option cleanup; and small fixes across algebra, topology, and tactics.lake-manifest.jsonbumps batteries to41bd267….Reviewed by Cursor Bugbot for commit a765b90. Bugbot is set up for automated code reviews on this repo. Configure here.