Added back original file - #1
Closed
YuvalFilmus wants to merge 113 commits into
Closed
Conversation
…o vertices (leanprover-community#31880) Co-authored-by: sunyue <enthusiastical996@gmail.com>
…unity#32736) These will be renamed in the upcoming lean release; this PR makes the change ahead of time to reduce the difference in the bump.
…egular (leanprover-community#32785) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…leanprover-community#32790) This file was split in leanprover-community#32304, but only one of the new files was imported in the deprecated module.
…also a right inverse) (leanprover-community#32610) + Prove equivalent characterizations of Dedekind-finite monoids. + Show commutative monoids, finite monoids, and Artinian semirings are Dedekind-finite, and finite monoids/rings are Dedekind-finite.
`match_target t` does exactly the same as `guard_target =~ t`. `guard_target` is defined in core Lean, has more functionality and is used everywhere, whereas `match_target` only has one use. Spotted while looking for un(der)documented tactics. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
…in complex (leanprover-community#32750) This PR dualises leanprover-community#32461.
…er-community#31805) Some API is also introduced for the particular case of inner horns in `Δ[3]`. From https://github.com/joelriou/topcat-model-category Co-authored-by: Nick Ward gio256@protonmail.com
We opt to not dualize theorems on sets, and instead just dualize `sSup` and `iSup`.
…exes indexed by the integers (leanprover-community#32743) In this PR, we dualise leanprover-community#32003: we define the cochain complex indexed by the integers associated to a projective resolution of an object in an abelian category.
…ommunity#32778) I need to shuffle a little bit the imports to let Accumulate import partialSups. As Accumulate is only used in advanced parts of the library, this looks reasonable to me. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…on by a CLM as a CLM on D_K^n (leanprover-community#30239) A map `T : F →L[𝕜] F'` induces a map `postcompCLM T : 𝓓^{n}_{K}(E, F) →L[𝕜] 𝓓^{n}_{K}(E, F')` Co-Authored by: @ADedecker Co-authored-by: ADedecker <anatolededecker@gmail.com>
…#32202) A simplicial set `X` is finite (`SSet.Finite`) if it has finitely many nondegenerate simplices. Equivalently, `X` is finite dimensional and the type of `n`-simplices of `X` is finite for any `n`.
… with shifts (leanprover-community#32308) Let `F : C₁ ⥤ C₂ ⥤ D` be a bifunctor (which is additive in both variables). In this PR, we show that the induced bifunctor `F.map₂CochainComplex : CochainComplex C₁ ℤ ⥤ CochainComplex C₂ ℤ ⥤ CochainComplex D ℤ` commutes with shifts by `ℤ`. (This means that it commutes with shifts by each variable, and also that there is a commutativity up to a sign when we consider both commutation at the same time.)
…er-community#32588) Currently, all these lemmas are special cases of the `Finsupp` ones. After leanprover-community#25273 however, this will not be the case anymore.
…ver-community#30678) This `Module` instance allows me to not ungeneralise the `NoZeroSMulDivisors R ℍ[R,c₁,c₂,c₃]` in leanprover-community#30563.
…roups of Kan complexes (leanprover-community#32347) We introduce a structure `SSet.PtSimplex` which consists of morphisms `Δ[n] ⟶ X` which are constant to a certain `x : X _⦋0⦌` on the boundary. Homotopy groups of Kan complexes will be defined as a quotient of this. We introduce two structures `PtSimplex.RelStruct` and `PtSimplex.MulStruct` which will be important in the study of homotopy groups of Kan complexes. From https://github.com/joelriou/topcat-model-category
Creates a structure that contains the data of a non-decreasing sequence of finite sets whose union equals some countable set. This is used in the brownian motion project to transfer a theorem that holds over finite sets to a countable set (with monotone convergence). The design is modelled on CompactExhaustion (of course it can be seen as precisely a special case but I think taking that approach would be much more convoluted). I didn't want to give this its own file, but I couldn't put it in `Mathlib.Data.Set.Countable` without creating a `large-import` because I needed the fact that product of finite sets is finite, and couldn't find anywhere else sensible to put it that wouldn't create a `large-import`. Would be happy if someone has a better suggestion. Co-authored-by: David Ledvinka <dledvinka@Davids-Mac-mini.local> Co-authored-by: David Ledvinka <dledvinka.ledvinka@mail.utoronto.ca>
…h commute to shifts in two variables (leanprover-community#32317) We introduce the two variable counterpart `NatTrans.CommShift₂` of `NatTrans.CommShift`. We also define `Functor.CommShift₂` instances for the precomposition on each variable.
…community#32533) This shows that the product of roots (as a multiset) is injective.
…ifolds (leanprover-community#32759) A belongs to the interior / boundary of an open submanifold iff it belongs to the interior / boundary, when regarded as a point of the ambient manifold.
…er-community#32728) Given two cochain complexes `K` and `L`, We define a map from the cohomology of `HomComplex K L` to the type `SmallShiftedHom` (which identifies to a type of morphisms in the derived category).
…mmunity#32741) We define the notion of K-projective cochain complex in an abelian category, and show that bounded above complexes of projective objects are K-projective. This is the dual results to leanprover-community#31941: the main lemma is obtained by dualising the corresponding lemma for K-injective complexes. We also dualise the result from leanprover-community#31900: morphisms in the derived category from a K-projective cochain complex identify to homotopy classes of morphisms.
leanprover-community#32252) Proves the relationship between the Chebyshev psi and theta functions; psi is a sum of theta evaluated at powers of x. This upstreams a result from the PrimeNumberTheoremAnd project. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Typos found and fixed by Codex. Co-authored-by: Johan Commelin <johan@commelin.net>
…rover-community#31717) Uses the API for creating new level parameters introduced in leanprover-community#30797.
…ps` (leanprover-community#32562) This is the standard name for fun-like types.
This is a very preliminary development; most of the PR is really just lemmas about `HahnSeries.support`. This will be needed in the CGT repo, to define surreal Hahn series as the subfield of real, small Hahn series over their own order dual. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
…-community#32818) This PR continues the deprecation in Splits.lean as we move over to the new API in Factors.lean. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
…#32360) Calculated the degree and leading coefficients of Chebyshev T and U, as well as formulas for T(-x) and U(-x).
…over-community#32710) Also moved `ConditionallyCompleteLinearOrder.isCompact_Icc` and `ProperSpace ℝ` earlier to avoid large inputs.
…-community#32756) Analogous to `PullbackCone`, we add a `WidePullbackCone` with API to construct them and to show they are limiting.
…rover-community#32876) Similar with `MvPolynomial.support_monomial`, while for `MvPolynomial.C`.
…olynomial_mul_monomial` (leanprover-community#32788) This commit adds a variant `sPolynomial_mul_monomial'`, using `m.degree (monomial d c * p)` instead of `d + m.degree p`, which are different in the edge case that one of `c` and `p` is 0. A pair of variants about `leadingTerm` instead of `monomial` are also added.
…on of valuation subrings (leanprover-community#31919) This contribution was created as part of the Heidelberg Lean workshop "Formalising algebraic geometry" in November 2025. Co-authored-by: Daniel Funck @danielfunckmaths-commits
…ne of submodule and quotient (leanprover-community#32560) Let `V` be an `R`-module. Let `W` be a submodule of `V` with a basis `b` and `c` be a basis of the quotient module `V ⧸ W`. `basisSum b c` is a basis of `V` indexed by the sum type of the index types of `b` and `c` that extends `b`and lifts `c`. We apply this construction to a determinant equality: `LinearMap.det_eq_det_mul_det` shows that if a linear map `f : V →ₗ[R] V` stabilizes the submodule `W`, then the determinant of `f` is the product of the determinants of the linear endomorphisms of `W` and `V ⧸ W` induced by `f`. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Typos found and fixed by Codex.
From flt-regular Co-authored-by: Andrew Yang <the.erd.one@gmail.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
…ty#32254) Add congruence isomorphisms in both the ring and monoid arguments. Move `mapRangeRingHom` from `Algebra.MonoidAlgebra.Lift` to `Algebra.MonoidAlgebra.MapDomain` and make its proofs additivisable (by not using `lift`). Make `mapDomainRingHom` take a `MonoidHom` rather than `MonoidHomClass`.
…-community#32715) Add theorems about ordCompl[p] n, the prime-to-p part of n, when n is a power of p. There are similar existing theorems in Data/Nat/Factorization/PrimePow.lean emphasizing isPrimePow. Motivation of PR is for a follow up PR on Combinatorial Proof of Euler's Partition Identity
Extracted from leanprover-community#30658. Found by extending the commandStart linter to proof bodies.
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 is the follow-up PR of leanprover-community#32912 adding the deprecated module after the file was moved.