Sync upstream mathlib4 (2026-05-11, +30 commits)#5
Merged
Conversation
This PR proves that the torsion subgroup of a product is the product of the torsion subgroups. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
Removes an `erw` that is now handled by `simp`. Extracted from #38415 [](https://gitpod.io/from-referrer/) Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
…#38832) - rewrites `frobeniusNumber_pair` to use `Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le` instead of constructing the witnesses via the Chinese remainder argument - closes the final witness equality by applying `succ_inj` to the resulting additive decomposition Extracted from #38144 [](https://gitpod.io/from-referrer/)
…tySequence` (#38833) - rewrites `complEDS₂_mul_b` by evaluating the parity split directly with `simp_rw` and `split_ifs`, removing the separate `Int.negInduction` proof Extracted from #38144 [](https://gitpod.io/from-referrer/)
…ion (#38654) This PR adds * `simp` lemmas that convert ways of expressing the multiplicity of a prime ideal `p` in the factorization of an ideal `I` into `multiplicity p.asIdeal I` (see [#Is there code for X? > Results on elements of number fields and ideals @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Results.20on.20elements.20of.20number.20fields.20and.20ideals/near/574739650)), * API lemmas on multiplicities, expressed in terms of `multiplicity p.asIdeal I`. * We also refactor a proof in Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas by extracting a couple of lemmas that we can reuse in one of the new lemmas. These will be useful in proving the Northcott property of heights on number fields.
…her up (#39181) This just moves the code for the `positivity` extension for `NumberField.totalWeight` before the section on "Heights over the rational numbers", in anticipating of adding code before that section that will need the positivity extension.
This PR adds lemmas `ShortComplex.ShortExact.acyclic_X₁/₂/₃` which allow to deduce that certain homological complexes in a short exact sequence are acyclic.
`ConvexSpace` is convex geometry, not linear algebra
…ossible and typo fix (#38971)
* Changing the usage of `IsNormalClosureFG N` to `N.IsNormalClosureFG` as the use of the latter seems easier to read ("N is finitely generated under normal closure") and is in line with using dot notation for terms.
* Fix a typo in the main definition docstring regarding the usage of `map`: it should be `.map` instead of `_map`.
…tegory (#36216) Co-authored-by: Michael Lee <michael.a.rodrigues.lee@gmail.com>
We rewrite the proof so as to avoid working with unbundled relations, and golf it somewhat in the process.
`Stoch` is a positive category (see _A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics_, Fritz, 2020, Example 11.25). Add several `Deterministic` instances for `SFinKer` and `Stoch` associators, unitors, braiding, counit, and comul morphisms. - [x] depends on: #38211 - [x] depends on: #38212 - [x] depends on: #39042 - [x] depends on: #39043 - [x] depends on: #39051 - [x] depends on: #39052
… by `@[fun_prop]` (#38512) Since #30511, the `@[measurability]` attribute is equivalent to `@[fun_prop]` when applied to lemmas about measurability of functions. This PR replaces these attributes by `@[fun_prop]` and adds a warning for this use of `@[measurability]`. Note that `@[measurability]` is still used for lemmas about measurability of sets.
…` (#38835) - rewrites `normSq_le_normSq_of_re_le_of_im_le` to reduce to the squared-coordinate inequalities and finish with `nlinarith` Extracted from #38144 [](https://gitpod.io/from-referrer/)
- rewrites `map_boundedFormula` by avoiding the `iff_eq_eq` detour and using the restricted free-variable realization lemma directly - shortens `isElementary_of_exists` by replacing the `map_rel` `erw` with explicit `simp_rw` and `rw` Extracted from #38415 [](https://gitpod.io/from-referrer/)
Strengthen the lemma `Scheme.ι_image_homOfLE_le_ι_image` so we get an equality instead of an LE. Also add a variant of `Scheme.homOfLE_apply` that takes in its argument unbundled, which is useful in the proof.
Under mild conditions (`D` being a lower set is sufficient though not necessary), open and closed sets in the `ScottHausdorff D` topology correspond to `DirSupInaccOn D` and `DirSupClosedOn D` sets.
…in Cantor's theorem (#39147) #6114 and #35752 removed the defeq abuse in `Function.cantor_surjective`, then #35239 golfed it, reintroducing defeq abuse. This reverts the golf to avoid defeq abuse, and cleans up a bit.
…t exact squares (#39028) We obtain abstract result about derivability structures which will imply that for categories of homological complexes, certain localizer morphisms are derivability structures iff the corresponding localizer morphisms on homotopy categories are derivability structures.
Rename [Module.Free.Module.free_shrink](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/FreeModule/Basic.html#Module.Free.Module.free_shrink) to `Module.Free.shrink` and rename [Module.Finite.Module.finite_shrink](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Finiteness/Basic.html#Module.Finite.Module.finite_shrink) to `Module.Finite.shrink`.
This adds a few more API lemmas for `{Add|}Subgroup.{FiniteIndex|IsFiniteRelIndex}` and connects the index with `Ideal.absNorm`; we also add the fact that (relative) indices of nonzero ideals in a Dedekind domain that is finite and free over the integers are finite.
We also generalize `Algebra.norm_algebraMap` from base fields to commutative rings, assuming the algebra is free over the base ring, and add some more API (`Algebra.del_lsmul`, `Algebra.norm_natCast`).
Companion to the existing `lineMap_mem_openSegment`: for `t ∈ Icc 0 1`, `AffineMap.lineMap a b t ∈ [a -[𝕜] b]`. Replaces the open-coded pattern `segment_eq_image_lineMap ▸ mem_image_of_mem _` at the two existing call sites. Co-authored-by: Christoph Spiegel <christophspiegel.berlin@gmail.com>
… via `LinearEquiv.ofLinear` (#38814) This PR refactors `Submodule.quotientEquivOfIsCompl` to use `LinearEquiv.ofLinear` rather than `LinearEquiv.symm <| LinearEquiv.ofBijective`. The new definition makes both directions of the equivalence explicit: the forward idirection is `Submodule.liftQ` of the projection onto `q` along `p`, and the backward direction is `Submodule.mkQ` composed with the inclusion `q` in `E`.
Defines `H.equiv₀`, the additive equivalence between `H F 0` and `F.obj.obj (op T)` when the category has a terminal object `T`. Co-authored-by: Brian-Nugent <bnugent@uw.edu>
Adds lower bounds to Chebyshev.lean for the theta, psi, and prime counting functions. Relating to this, the lcm of the first n natural numbers is defined, with some basic API, and the psi function is shown to equal to the log of this lcm. A helper lemma on the prime factorization of a finset lcm is added to FinsetLemmas.lean. API for `primesLE` (the primes less than or equal to a natural number) is added to `PrimeCounting.lean`. The API for `primesBelow` (the primes strictly less than a natural number) has been moved from `SmoothNumbers.lean` to `PrimeCounting.lean` and the two API have been aligned. See also the discussion at https://leanprover.zulipchat.com/#narrow/channel/423402-PrimeNumberTheorem.2B/topic/A.20short.20proof.20of.20the.20Chebyshev.20lower.20bound Also made minor edits to `Primorial.lean` to link it to the new `primesLE`. A helper lemma that the log of a prime is always positive is added to `Analysis.SpecialFunctions.Log.Basic`. Co-authored-by: Terence Tao <tao@math.ucla.edu>
…n complexes (#39076) Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
…s invertible (#37216) We show that a finite stably free module `M` is free if it is invertible. - [x] depends on: #36951 Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
…ed` to `IsUnramifiedAt` (#39072) This PR adds an `iff` lemma relating `Unramified` to `IsUnramifiedAt`. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
…#39073) This PR adds a positivity lemma for the new `inertiaDeg'` (which will eventually replace `inertiaDeg`). An extra import is needed to synthesize finiteness on the residue fields. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
](https://gitpod.io/from-referrer/){kind=link}
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
18 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.686c76b39dab044f7548552a8cfa9d01633ae3aaAuto-merges to
masteronceCI (self-hosted)passes. Regenerateddaily until merged or until a conflict appears.