Helping out: short tasks

Would you like to help out at a PR, differently from reviewing? Here are some ideas:

take a look at PRs with just some mathlib-infrastructure-related CI failure: unless it's an infrastructure PR, these are spurious/not the PRs fault. If the failure is spurious, commenting to this effect can be helpful.
take a look at PRs labelled help-wanted or please-adopt
If the author hasn't noticed, you can ask in a PR which just has a merge conflict, but would be reviewable otherwise. (Remember, that most contributors to mathlib are volunteers, contribute in their free time and often have other commitments — and that real-life events can happen!)
post a comment on a PR made from a fork, nicely asking them to re-submit it from a mathlib branch instead
check if any 'stale' PR by a new contributor benefits from support, such as help with failing CI or providing feedback on the code
check if any 'stale' delegated PR benefits from support, such as by fixing merge conflicts (but be sure to ask first; the PR author might simply be very busy)

This dashboard was last updated on: April 19, 2025 at 08:26 UTC

PRs with just failing CI, but only often-spurious jobs

There are currently no PRs with just an infrastructure-related CI failure. Congratulations!

PRs looking for help

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
6859	MohanadAhmed author:MohanadAhmed	TryLean4Bundle: Windows Bundle Creator	# `TryLean4Bundle`: Windows Bundle Creator A Windows batch script and a CI yml file that create an self extracting archive. The user should 1. just download the archive, 2. double click the archive to expand 3. double click the `RunLean.bat` script in the expanded archive. The script currently downloads 7 dependencies into CI then unpacks them in the appropriate locations and finally packs them back. To try a bundle created using these scripts but from a different repo see (https://github.com/MohanadAhmed/TryLean4Bundle/releases) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	CI WIP help-wanted	114/0	.github/workflows/mk_windows_bundle.yml,scripts/windowsBundle.bat	2	0	[]	nobody	262-759 8 months ago	598-30030 1 year ago	0-0 0 seconds
7300	ah1112 author:ah1112	feat: synthetic geometry	This is adding synthetic geometry using Avigad's axioms and formalizing Euclid Book I, through the Pythagorean theorem. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-euclidean-geometry awaiting-author help-wanted	2657/0	Mathlib.lean,Mathlib/Geometry/Synthetic/Avigad/Axioms.lean,Mathlib/Geometry/Synthetic/Avigad/EuclidBookI.lean,Mathlib/Geometry/Synthetic/Avigad/Tactics.lean	4	71	['ah1112', 'alreadydone', 'eric-wieser', 'github-actions', 'tb65536', 'urkud']	nobody	262-758 8 months ago	451-43821 1 year ago	0-0 0 seconds
9040	BoltonBailey author:BoltonBailey	feat: `to_snoc` an attribute for generating lemmas with snoc in them	This is an experimental PR for a new attribute which is basically `to_additive`, but instead of changing multiplication to addition, it changes `cons` to `snoc`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta please-adopt WIP help-wanted	1292/0	Mathlib/Tactic/ToSnoc.lean	1	0	[]	nobody	246-76700 8 months ago	246-76700 8 months ago	0-0 0 seconds
5919	MithicSpirit author:MithicSpirit	feat: implement orthogonality for AffineSubspace	Define `AffineSubspace.orthogonal` and `AffineSubspace.IsOrtho`, as well as develop an API emulating that of `Submodule.orthogonal` and `Submodule.IsOrtho`, respectively. Additionally, provide some relevant lemmas exclusive to affine subspaces, which are mostly to do with the relationship between orthogonality and `AffineSubspace.Parallel`. Closes #5539 --- Still WIP as I need to add more docstrings as well as notations for the new definitions. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis WIP help-wanted	330/0	Mathlib.lean,Mathlib/Analysis/InnerProductSpace/AffineSubspace.lean	2	4	['MithicSpirit', 'eric-wieser']	MithicSpirit assignee:MithicSpirit	246-76365 8 months ago	246-76365 8 months ago	0-0 0 seconds
21871	YaelDillies author:YaelDillies	feat: decomposition into independent atoms	Prove that any element in a compactly generated modular atomistic lattice (eg the lattice of submodules of a module) can be written as the supremum of independent atoms. From PersistentDecomp and Xena --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-order help-wanted	114/20	Mathlib/Data/Set/Insert.lean,Mathlib/Order/Atoms.lean,Mathlib/Order/CompactlyGenerated/Basic.lean	3	2	['github-actions']	nobody	62-45826 2 months ago	63-72128 2 months ago	0-15 15 seconds
13442	dignissimus author:dignissimus	feat: mabel tactic for multiplicative abelian groups	Mabel tactic for multiplicative abelian groups (#10361) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-meta modifies-tactic-syntax awaiting-author help-wanted	439/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/MAbel.lean,MathlibTest/mabel.lean	4	10	['BoltonBailey', 'dignissimus', 'github-actions', 'joneugster', 'kbuzzard']	joneugster assignee:joneugster	58-35360 1 month ago	63-16956 2 months ago	0-16 16 seconds
23186	grunweg author:grunweg	feat: split continuous linear maps	We define split linear maps and prove their basic properties. --- - [ ] depends on #23175 There are two sorries left. One is `ClosedComplemented.prod`; the other relates to the composition of split maps. Help with both is welcome. [This zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Composition.20of.20immersions.20is.20an.20immersion.3A.20infinite-dimensio/with/507300190) contains a proof of the non-trivial sorry. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis WIP help-wanted	240/0	Mathlib.lean,Mathlib/Analysis/NormedSpace/HahnBanach/Splits.lean	2	1	['github-actions']	nobody	8-57557 8 days ago	8-57557 8 days ago	0-0 0 seconds
22925	ggranberry author:ggranberry	feat(Mathlib/PlaceHolder/ToeplitzHausdorff): Toeplitz-Hausdorff	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-analysis awaiting-author WIP help-wanted	411/0	Mathlib/PlaceHolder/ToeplitzHausdorff.lean,Mathlib/PlaceHolder/ToeplitzHausdorff_v2.lean	2	10	['faenuccio', 'ggranberry', 'github-actions']	faenuccio assignee:faenuccio	1-41995 1 day ago	1-41995 1 day ago	4-24257 4 days
5863	eric-wieser author:eric-wieser	feat: add elaborators for concrete matrices	--- - [x] depends on: #5866 - [ ] depends on: #5897 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta blocked-by-other-PR help-wanted	257/7	Mathlib/Control/Monad/Cont.lean,Mathlib/Data/Matrix/Auto.lean,MathlibTest/matrix_auto.lean	3	6	['eric-wieser', 'github-actions', 'kim-em']	nobody	1-27911 1 day ago	1-28029 1 day ago	0-0 0 seconds
12934	grunweg author:grunweg	chore: replace more uses of > or ≥ by < or ≤	These were flagged by the linter in https://github.com/leanprover-community/mathlib4/pull/12879: it is easy to simple avoid > or ≥ in hypotheses or haves. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict awaiting-author help-wanted	41/42	Archive/Imo/Imo1962Q1.lean,Archive/Imo/Imo1988Q6.lean,Archive/Imo/Imo1994Q1.lean,Archive/Imo/Imo2005Q3.lean,Archive/Imo/Imo2006Q3.lean,Archive/Imo/Imo2008Q2.lean,Archive/Imo/Imo2008Q3.lean,Archive/Imo/Imo2019Q4.lean,Archive/Sensitivity.lean,Archive/Wiedijk100Theorems/CubingACube.lean,Mathlib/Tactic/Linarith/Datatypes.lean,test/cancel_denoms.lean,test/congr.lean,test/interval_cases.lean,test/observe.lean	15	11	['YaelDillies', 'adomani', 'github-actions', 'grunweg', 'jcommelin', 'urkud']	nobody	262-763 8 months ago	275-10360 9 months ago	1-73101 1 day
9642	eric-wieser author:eric-wieser	refactor(Analysis/Normed/{Group/Field}/Basic): Let `extends` generate the repeated fields	New-style structure shenanigans mean that instance constructors randomly complain about a missing field that can be found with `__ : MetricSpace _ := infer_instance`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) I will write a longer PR description for this once CI is happy	t-analysis merge-conflict awaiting-author WIP help-wanted	122/202	Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Complex/Basic.lean,Mathlib/Analysis/Matrix.lean,Mathlib/Analysis/Normed/Field/Basic.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Completion.lean,Mathlib/Analysis/Normed/Order/Basic.lean,Mathlib/Analysis/NormedSpace/ProdLp.lean,Mathlib/Analysis/NormedSpace/Star/Matrix.lean,Mathlib/Analysis/NormedSpace/Unitization.lean,Mathlib/Analysis/Quaternion.lean,Mathlib/Geometry/Manifold/Instances/Sphere.lean,Mathlib/InformationTheory/Hamming.lean,Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean,Mathlib/NumberTheory/Padics/PadicIntegers.lean,Mathlib/Topology/ContinuousFunction/Bounded.lean	17	11	['eric-wieser', 'leanprover-bot', 'urkud']	nobody	262-760 8 months ago	439-67062 1 year ago	0-0 0 seconds
6931	urkud author:urkud	refactor(Analysis/Normed): use `RingHomIsometric` for `.norm_cast`	--- I don't understand why linter fails. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis merge-conflict help-wanted	78/68	Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean,Mathlib/Analysis/Normed/Field/Basic.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/NormedSpace/Basic.lean,Mathlib/Analysis/NormedSpace/Exponential.lean,Mathlib/Analysis/NormedSpace/Spectrum.lean,Mathlib/Analysis/RCLike/Basic.lean,Mathlib/NumberTheory/NumberField/Embeddings.lean	8	0	[]	nobody	262-759 8 months ago	283-67863 9 months ago	0-0 0 seconds
6791	eric-wieser author:eric-wieser	refactor: Use flat structures for morphisms	This restores the symmetry we had in Lean3, where we had `MonoidHom.mk f one mul` not `MonoidHom.mk (OneHom.mk f one) mul`, and `f.toFun` wasn't notation for `f.toMulHom.toFun`. The nesting provided by the previous inheritance is useless to us in the face of `MonoidHomClass.toMonoidHom`, which completely eta-expands the structure anyway. We call the class `FunLikeFlatHack._` because this means the field is called `to_` which uses up less space in the goal view than any alternative. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-CI merge-conflict awaiting-author help-wanted	174/201	Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/Algebra/Hom.lean,Mathlib/Algebra/Category/GroupCat/ZModuleEquivalence.lean,Mathlib/Algebra/Category/GroupWithZeroCat.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf.lean,Mathlib/Algebra/Category/MonCat/Basic.lean,Mathlib/Algebra/Group/Ext.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Group/UniqueProds.lean,Mathlib/Algebra/Hom/Equiv/Basic.lean,Mathlib/Algebra/Hom/Group/Defs.lean,Mathlib/Algebra/Hom/GroupAction.lean,Mathlib/Algebra/Hom/NonUnitalAlg.lean,Mathlib/Algebra/Hom/Ring/Defs.lean,Mathlib/Algebra/Lie/Basic.lean,Mathlib/Algebra/Module/Equiv.lean,Mathlib/Algebra/Module/LinearMap.lean,Mathlib/Algebra/Order/Hom/Ring.lean,Mathlib/Algebra/Order/Interval.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean,Mathlib/Data/FunLike/Basic.lean,Mathlib/Data/Rat/Cast/CharZero.lean,Mathlib/Data/Real/EReal.lean,Mathlib/Data/Real/Sqrt.lean,Mathlib/GroupTheory/FreeAbelianGroup.lean,Mathlib/GroupTheory/MonoidLocalization.lean,Mathlib/LinearAlgebra/Quotient.lean,Mathlib/LinearAlgebra/TensorProduct.lean,Mathlib/RingTheory/RingInvo.lean,Mathlib/Topology/Algebra/Module/Basic.lean,Mathlib/Topology/MetricSpace/Dilation.lean	32	0	[]	nobody	262-759 8 months ago	578-55019 1 year ago	0-0 0 seconds
5934	eric-wieser author:eric-wieser	feat: port Data.Rat.MetaDefs	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This needs some eyes from people familiar with Qq	t-meta merge-conflict mathlib-port help-wanted	183/0	Mathlib.lean,Mathlib/Data/Rat/MetaDefs.lean,test/rat.lean	3	4	['eric-wieser', 'gebner']	nobody	262-758 8 months ago	431-74147 1 year ago	0-0 0 seconds
7903	urkud author:urkud	feat: define `UnboundedSpace`	--- The new instances generate some timeouts, and I don't understand why. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-topology merge-conflict help-wanted	111/59	Mathlib/Analysis/BoxIntegral/Basic.lean,Mathlib/Analysis/Normed/Module/Basic.lean,Mathlib/Topology/Bornology/Basic.lean,Mathlib/Topology/Bornology/Constructions.lean,Mathlib/Topology/MetricSpace/Bounded.lean,Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean	6	1	['github-actions']	nobody	254-75136 8 months ago	254-75136 8 months ago	0-0 0 seconds
9444	erdOne author:erdOne	feat: Various instances regarding `𝓞 K`.	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-number-theory merge-conflict help-wanted	27/0	Mathlib/NumberTheory/NumberField/Basic.lean,Mathlib/RingTheory/IntegralClosure.lean	2	9	['erdOne', 'leanprover-bot', 'mattrobball', 'riccardobrasca', 'xroblot']	nobody	246-76912 8 months ago	246-76912 8 months ago	0-0 0 seconds
10765	Vierkantor author:Vierkantor	feat(Tactic): `ring` modulo a given characteristic	This PR extends the `ring` tactic with a new config argument `char` which will try to reduce all constant terms modulo the given characteristic. This allows `ring` to prove e.g. `(x + y)^3 = x^3 + y^3` in characteristic 3. This is a simpler and faster way to do so than what we had before: `repeat { ring; reduce_mod_char }` becomes `ring (config := { char := 3 })`. The first step is to split off the required `CharP` definitions, since `Mathlib.Algebra.CharP.Basic` already requires the `ring` tactic. To perform the reduction modulo the given characteristic, I implemented `reduceCast` which reduces a raw integer, and wrapped it in `reduceResult` that takes a `NormNum.Result` for easy use. We need to pass through quite a few parameters into `reduceResult` so maybe it's worth defining a structure, or reusing `Cache` for this. Then it's basically a case of replacing every place where `ring` constructs a numeral with a call to `reduceResult`. Limitations: * `ring` doesn't attempt to detect the characteristic by itself, you need to pass it in explicitly. Trying to infer a `CharP` instance at each point sounds quite expensive. * Since the support for `%` in `NormNum` only exists for integers, I implemented the reduction only when a `Ring` instance is available. It is still sound in the semiring case, just not complete. * We could optimize exponentiation in the specific case where the characteristic `p` is a prime that divides the exponent `n`: `(x + y)^n = x^n + y^n`. I'll leave that to future work. --- - [x] depends on: #12907 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta merge-conflict awaiting-author help-wanted	275/108	Mathlib/RingTheory/MvPolynomial/Basic.lean,Mathlib/Tactic/Polyrith.lean,Mathlib/Tactic/Ring/Basic.lean,Mathlib/Tactic/Ring/RingNF.lean,test/ring_mod_char.lean	5	7	['Vierkantor', 'YaelDillies', 'github-actions', 'joneugster', 'leanprover-community-mathlib4-bot']	joneugster assignee:joneugster	219-69015 7 months ago	219-69015 7 months ago	28-28613 28 days
14739	urkud author:urkud	feat(Measure): add `gcongr` lemmas	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-measure-probability merge-conflict awaiting-author WIP help-wanted	12/8	Mathlib/MeasureTheory/Covering/Differentiation.lean,Mathlib/MeasureTheory/Function/SimpleFunc.lean,Mathlib/MeasureTheory/Integral/SetToL1.lean,Mathlib/MeasureTheory/Measure/MeasureSpace.lean,Mathlib/Probability/Kernel/Disintegration/Density.lean	5	3	['github-actions', 'kim-em', 'urkud']	nobody	153-85299 5 months ago	153-85299 5 months ago	0-66587 18 hours
18508	urkud author:urkud	chore(OperatorNorm/Completeness): drop a duplicate instance	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis merge-conflict help-wanted	5/22	Mathlib/Analysis/CStarAlgebra/Multiplier.lean,Mathlib/Analysis/InnerProductSpace/LinearPMap.lean,Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean,Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean,Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean,Mathlib/MeasureTheory/Integral/SetToL1.lean,Mathlib/Topology/Algebra/Module/StrongTopology.lean	7	15	['github-actions', 'j-loreaux', 'leanprover-bot', 'urkud']	nobody	120-41368 3 months ago	120-41369 3 months ago	0-46295 12 hours
11837	trivial1711 author:trivial1711	feat: completion of a uniform multiplicative group	Multiplicativize `Topology.Algebra.GroupCompletion`. That is, rewrite it in the multiplicative setting and recover the original results using `@[to_additive]`. - Because `@[to_additive]` doesn't work with `noncomputable section` (https://github.com/leanprover/lean4/pull/2610), some instances with `@[to_additive]` need to be explicitly marked with `noncomputable instance`. - One might be tempted to multiplicativize this definition from `Topology.Algebra.GroupCompletion`: ```lean instance [UniformSpace α] [Add α] : Add (Completion α) := ⟨Completion.map₂ (· + ·)⟩ ``` to this: ```lean @[to_additive] instance [UniformSpace α] [Mul α] : Mul (Completion α) := ⟨Completion.map₂ (· * ·)⟩ ``` However, as Eric Wieser pointed out, doing so would create a bad diamond with the definition ```lean instance [UniformSpace α] [TopologicalRing α] [UniformAddGroup α] [Ring α] : Mul (Completion α) := ⟨curry <\| (denseInducing_coe.prod denseInducing_coe).extend ((↑) ∘ uncurry (· * ·))⟩ ``` in `Topology.Algebra.UniformRing`. How should this diamond be resolved? Well, the definition of multiplication that uses `curry <\| (denseInducing_coe.prod denseInducing_coe).extend ((↑) ∘ uncurry (· * ·))` is the "correct" one. For example, it yields the correct result if `α` is `ℚ`, unlike the definition that uses `Completion.map₂ (· * ·)`. (This is because `Completion.map₂` yields junk values if used on a function which is not uniformly continuous. Note, however, that if multiplication on `α` is uniformly continuous, then `Completion.map₂ (· * ·)` and `curry <\| (denseInducing_coe.prod denseInducing_coe).extend ((↑) ∘ uncurry (· * ·))` are propositionally equal.) So, following Eric's suggestion, we remove the definition that uses `Completion.map₂ (· * ·)`, and generalize the other definition to any uniform space with a multiplication operation: ```lean @[to_additive] noncomputable instance [UniformSpace α] [Mul α] : Mul (Completion α) := ⟨curry <\| (denseInducing_coe.prod denseInducing_coe).extend ((↑) ∘ uncurry (· * ·))⟩ ``` This requires slightly modifying some of the proofs in `Topology.Algebra.GroupCompletion`. For example, suppose that `α` is a uniform group. Since we can no longer use `Completion.continuous_map₂`, it becomes more efficient to prove that the multiplication, inversion, and division operations on `Completion α` are uniformly continuous before we prove that `Completion α` is a group. - Previously, `Topology.Algebra.GroupCompletion` had an instance: ```lean instance [UniformSpace α] [Sub α] : Sub (Completion α) := ... ``` Naively multiplicativizing this would yield ```lean @[to_additive] instance [UniformSpace α] [Inv α] : Inv (Completion α) := ... ``` Unfortunately, this would conflict with `Topology.Algebra.UniformField`, which already instantiates `Inv (Completion α)` when `α` is a uniform field. Instead, we use two different `instance` declarations. (If `α` is an additive group, then this instantiates `Neg (Completion α)` twice, and the instances are syntactically equal.) ```lean @[to_additive] noncomputable instance [UniformSpace α] [Group α] : Inv (Completion α) := ... instance [UniformSpace α] [Neg α] : Neg (Completion α) := ... ``` This avoids the bad diamond (because a uniform field can never be a `Group`) while remaining backward compatible. Note that the `@[to_additive]` is necessary here, because it maintains the link between the additive setting and multiplicative setting. We use a similar method to instantiate `Div (Completion α)`. - Some definitions in this file involve a module structure on `α`. We leave these as is and do not attempt to multiplicativize them at all. - The instance of `DistribMulAction` must be multiplicativized to an instance of `MulDistribMulAction` manually. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Completion.20of.20a.20uniform.20multiplicative.20group --- # (Small) Issue Recall the following trick that this pull request uses to define inversion and negation on uniform spaces. The idea is that we define negation on the completion of any uniform space that has a negation operation, but we define inversion on only the completion of a uniform space that has the structure of a multiplicative group. We do this to avoid creating a bad diamond with the inversion operation on a uniform field. ```lean @[to_additive] noncomputable instance {α : Type} [UniformSpace α] [Group α] : Inv (Completion α) := ... instance {α : Type} [UniformSpace α] [Neg α] : Neg (Completion α) := ... ``` Now, suppose that we want to prove `coe_inv_of_group` (resp. `coe_neg`), which states that the coercion `α → Completion α` commutes with inversion (resp. negation). In the current version of this pull request, `coe_inv_of_group` (resp. `coe_neg`) only applies to uniform multiplicative (resp. additive) groups. However, we do not use the fact that multiplication (resp. addition) on `α` is uniformly continuous to prove it. We only use the fact that inversion (resp. negation) is continuous. So, what we really want is to have more general statements that look like this: ```lean theorem coe_inv_of_group {α : Type} [UniformSpace α] [Group α] [ContinuousInv α] : ... theorem coe_neg {α : Type} [UniformSpace α] [Neg α] [ContinuousNeg α] : ... ``` Note that `coe_inv_of_group` needs the assumption `[Group α]`, because otherwise inversion is not defined on `Completion α` at all. However, `coe_neg` does not need the analogous assumption `[AdditiveGroup α]`. The question is: If `coe_inv_of_group` and `coe_neg` are written in this more general form, how can we link them using `@[to_additive]`? Here is one option, but it obviously leaves something to be desired. ```lean @[to_additive coe_neg_do_not_use_this_use_the_more_general_version] theorem coe_inv_of_group {α : Type} [UniformSpace α] [Group α] [ContinuousInv α] : ... theorem coe_neg {α : Type} [UniformSpace α] [Neg α] [ContinuousNeg α] : ... ``` Co-authored-by: Eric Wieser --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra t-topology merge-conflict WIP help-wanted label:t-algebra$	342/217	Mathlib/Analysis/InnerProductSpace/Completion.lean,Mathlib/Analysis/Normed/Group/HomCompletion.lean,Mathlib/Analysis/Normed/Module/Completion.lean,Mathlib/Topology/Algebra/GroupCompletion.lean,Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean,Mathlib/Topology/Algebra/Nonarchimedean/Completion.lean,Mathlib/Topology/Algebra/UniformField.lean,Mathlib/Topology/Algebra/UniformMulAction.lean,Mathlib/Topology/Algebra/UniformRing.lean	9	14	['eric-wieser', 'github-actions', 'trivial1711']	nobody	78-42357 2 months ago	78-42357 2 months ago	101-64856 101 days
12824	BoltonBailey author:BoltonBailey	refactor: `ReflTransGen`	It would be nice to have that `ReflTransGen` is the composition of `ReflGen` with `TransGen`, currently experimenting with redefining it this way. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-logic merge-conflict WIP help-wanted	91/96	Mathlib/Logic/Relation.lean	1	4	['BoltonBailey', 'grunweg', 'vihdzp']	nobody	77-27010 2 months ago	79-40109 2 months ago	0-0 0 seconds
12673	grunweg author:grunweg	feat: add ContDiff.lipschitzOnWith	A C¹ function is Lipschitz on each convex compact set. From sphere-eversion. -------- Commits can be reviewed independently. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis merge-conflict awaiting-author help-wanted	30/11	Mathlib/Analysis/Calculus/ContDiff/RCLike.lean	1	6	['Ruben-VandeVelde', 'github-actions', 'grunweg', 'sgouezel']	nobody	1-61292 1 day ago	1-61292 1 day ago	1-7552 1 day

PRs with just a merge conflict

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
12936	mattrobball author:mattrobball	chore(Quiver.Opposite): make `Quiver.Hom.op/unop` `abbrev`'s	These are wrappers around the constructor and projection for `Opposite Quiver.Hom _ _`. The projection itself is reducible and with structure eta built in to defeq it seems like we might be making Lean work harder than is necessary. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict	39/34	Mathlib/Algebra/Homology/ShortComplex/Homology.lean,Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean,Mathlib/CategoryTheory/Idempotents/Basic.lean,Mathlib/CategoryTheory/Limits/HasLimits.lean,Mathlib/CategoryTheory/Limits/Opposites.lean,Mathlib/CategoryTheory/Opposites.lean,Mathlib/CategoryTheory/Sites/CoverLifting.lean,Mathlib/CategoryTheory/Subobject/Comma.lean,Mathlib/CategoryTheory/Triangulated/Opposite.lean,Mathlib/Combinatorics/Quiver/Basic.lean	10	9	['YaelDillies', 'kim-em', 'leanprover-bot', 'mattrobball']	nobody	262-763 8 months ago	329-53155 10 months ago	0-0 0 seconds
10721	urkud author:urkud	feat(Order/FunLike): define `PointwiseLE`	- introduce a mixin class `DFunLike.PointwiseLE`, use it to define `DFunLike.instPartialOrder`; - add a generic `DFunLike.orderEmbeddingCoe` - add `DFunLike.PointwiseLE` instances here and there. With this refactor and #13022, I'm going to generalize lemmas like `MeasureTheory.ae_mono` to `OuterMeasureClass`. --- - [x] depends on: #12983 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-logic t-order merge-conflict	123/50	Mathlib.lean,Mathlib/Algebra/Order/Hom/Ring.lean,Mathlib/Data/DFinsupp/Order.lean,Mathlib/Data/Finsupp/Order.lean,Mathlib/Data/FunLike/Basic.lean,Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean,Mathlib/GroupTheory/Congruence.lean,Mathlib/Order/FunLike.lean,Mathlib/Order/Heyting/Hom.lean,Mathlib/Order/Hom/Basic.lean,Mathlib/Order/Hom/Bounded.lean,Mathlib/Order/Hom/CompleteLattice.lean,Mathlib/Topology/Order/Hom/Basic.lean	13	48	['YaelDillies', 'dupuisf', 'leanprover-community-mathlib4-bot', 'urkud']	nobody	262-761 8 months ago	283-67863 9 months ago	64-12826 64 days
9339	FMLJohn author:FMLJohn	feat (RingTheory/GradedAlgebra/HomogeneousIdeal): given a finitely generated homogeneous ideal of a graded semiring, construct a finite spanning set for the ideal which only contains homogeneous elements	--- - [ ] depends on: #8187 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	402/4	Mathlib.lean,Mathlib/Algebra/DirectSum/Internal.lean,Mathlib/Algebra/GradedMonoid.lean,Mathlib/Algebra/Module/GradeZeroModule.lean,Mathlib/RingTheory/Finiteness.lean,Mathlib/RingTheory/GradedAlgebra/Basic.lean,Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean,Mathlib/RingTheory/GradedAlgebra/Noetherian.lean	8	11	['FMLJohn', 'github-actions', 'jjaassoonn', 'leanprover-community-mathlib4-bot']	nobody	262-760 8 months ago	295-75077 9 months ago	0-0 0 seconds
8788	FMLJohn author:FMLJohn	feat(Algebra/Module/GradeZeroModule): if `A` is a graded semiring and `M` is a graded `A`-module, then each grade of `M` is a module over the 0-th grade of `A`.	--- - [ ] depends on: #8187 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	237/4	Mathlib.lean,Mathlib/Algebra/DirectSum/Internal.lean,Mathlib/Algebra/GradedMonoid.lean,Mathlib/Algebra/Module/GradeZeroModule.lean,Mathlib/RingTheory/GradedAlgebra/Basic.lean,Mathlib/RingTheory/GradedAlgebra/Noetherian.lean	6	4	['FMLJohn', 'github-actions', 'leanprover-community-mathlib4-bot']	nobody	262-760 8 months ago	295-75062 9 months ago	0-0 0 seconds
6777	adomani author:adomani	chore(CovariantClass): replace eta-expanded (· ·), (· + ·), (· ≤ ·), (· < ·)	Replace `CovariantClass X X (· * ·) (· ≤ ·)` with -> `CovariantClass X X HMul.hMul LE.le` and similarly for `HAdd`, `LT`, `Contravariant`. This PR is inspired by [Issue #6646](https://github.com/leanprover-community/mathlib4/issues/6646) and, more specifically, [this comment](https://github.com/leanprover-community/mathlib4/issues/6646#issuecomment-1692792066). Note that https://github.com/leanprover/lean4/pull/2267 would make this unnecessary --- ```bash # First sed command: # the first captured pattern is `CovariantClass ` # the second captured pattern is `` # the third captured pattern is `+` or `` # the fourth captured pattern is `<` or `≤` # a match for `CovariantClass (· ·) (· ·)` becomes # `CovariantClass replaceop replaceop` # Second sed command: similar to the first, but looks for `(Function.swap (· ·))` sed -i ' s=$Co[ntra]variantClass \(..$ \2 \)(· $[+]$ ·) (· $[<≤]$ ·)=\1replaceop\3 replaceop\4=g s=$Co[ntra]variantClass \(..$ \2 \)($[Functio\.swap ]$(· $[+]$ ·)) (· $[<≤]$ ·)=\1(\3replaceop\4) replaceop\5=g s=replaceop+=HAdd.hAdd=g s=replaceop\=HMul.hMul=g s=replaceop<=LT.lt=g s=replaceop≤=LE.le=g s=$Co[ntra]variantClass N N$ (· \ ·) r=\1 HMul.hMul r=g s=$Co[ntra]variantClass N N (swap μ)$ (· ≤ ·)=\1 LE.le=g s=$Co[ntra]variantClass N N$ (swap (· \* ·)) r=\1 (swap HMul.hMul) r=g s=$CovariantClass (Filter α) (Filter α)$ (· / ·) (· ≤ ·)=\1 HDiv.hDiv LE.le=g s=$CovariantClass (Filter α) (Filter α)$ (swap (· / ·)) (· ≤ ·)=\1 (swap HDiv.hDiv) LE.le=g s=$Co[ntra]variantClass . (fun x y .> . \* .)$ (· ≤ ·)=\1 LE.le=g s=$Co[ntra]variantClass . (fun x y .> . \* .)$ (· < ·)=\1 LT.lt=g s=$Co[ntra]variantClass [^}]$ (· ≤ ·)=\1 LE.le=g s=$CovariantClass .* (Filter β)$ (· • ·) LE.le=\1 HSMul.hSMul LE.le=g ' $(git ls-files '*.lean') ``` [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict	703/678	Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean,Mathlib/Algebra/BigOperators/Basic.lean,Mathlib/Algebra/Bounds.lean,Mathlib/Algebra/CovariantAndContravariant.lean,Mathlib/Algebra/DirectSum/Internal.lean,Mathlib/Algebra/Group/UniqueProds.lean,Mathlib/Algebra/GroupPower/Order.lean,Mathlib/Algebra/MonoidAlgebra/Degree.lean,Mathlib/Algebra/Order/Archimedean.lean,Mathlib/Algebra/Order/Group/Abs.lean,Mathlib/Algebra/Order/Group/Defs.lean,Mathlib/Algebra/Order/Group/DenselyOrdered.lean,Mathlib/Algebra/Order/Group/MinMax.lean,Mathlib/Algebra/Order/Group/OrderIso.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Order/Interval.lean,Mathlib/Algebra/Order/Kleene.lean,Mathlib/Algebra/Order/LatticeGroup.lean,Mathlib/Algebra/Order/Module.lean,Mathlib/Algebra/Order/Monoid/Basic.lean,Mathlib/Algebra/Order/Monoid/Cancel/Defs.lean,Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean,Mathlib/Algebra/Order/Monoid/Defs.lean,Mathlib/Algebra/Order/Monoid/Lemmas.lean,Mathlib/Algebra/Order/Monoid/MinMax.lean,Mathlib/Algebra/Order/Monoid/NatCast.lean,Mathlib/Algebra/Order/Monoid/OrderDual.lean,Mathlib/Algebra/Order/Monoid/Prod.lean,Mathlib/Algebra/Order/Monoid/WithTop.lean,Mathlib/Algebra/Order/Monoid/WithZero/Basic.lean,Mathlib/Algebra/Order/Monoid/WithZero/Defs.lean,Mathlib/Algebra/Order/Nonneg/Ring.lean,Mathlib/Algebra/Order/Pointwise.lean,Mathlib/Algebra/Order/Positive/Ring.lean,Mathlib/Algebra/Order/Ring/Canonical.lean,Mathlib/Algebra/Order/Ring/Defs.lean,Mathlib/Algebra/Order/Ring/Lemmas.lean,Mathlib/Algebra/Order/Sub/Basic.lean,Mathlib/Algebra/Order/Sub/Canonical.lean,Mathlib/Algebra/Order/Sub/Defs.lean,Mathlib/Algebra/Order/WithZero.lean,Mathlib/Algebra/Parity.lean,Mathlib/Algebra/Star/Order.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Analysis/Normed/Order/Lattice.lean,Mathlib/Data/DFinsupp/Lex.lean,Mathlib/Data/DFinsupp/Order.lean,Mathlib/Data/Finset/Fold.lean,Mathlib/Data/Finsupp/Lex.lean,Mathlib/Data/Finsupp/Order.lean,Mathlib/Data/List/BigOperators/Basic.lean,Mathlib/Data/List/BigOperators/Lemmas.lean,Mathlib/Data/Multiset/Basic.lean,Mathlib/Data/Nat/Cast/Order.lean,Mathlib/Data/PNat/Basic.lean,Mathlib/Data/Real/ENNReal.lean,Mathlib/Data/Real/NNReal.lean,Mathlib/Data/Set/Semiring.lean,Mathlib/Data/Sign.lean,Mathlib/MeasureTheory/Function/LpOrder.lean,Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean,Mathlib/MeasureTheory/Measure/MeasureSpace.lean,Mathlib/MeasureTheory/Measure/VectorMeasure.lean,Mathlib/Order/ConditionallyCompleteLattice/Group.lean,Mathlib/Order/Filter/Basic.lean,Mathlib/Order/Filter/Pointwise.lean,Mathlib/Probability/Martingale/Basic.lean,Mathlib/Probability/Process/Stopping.lean,Mathlib/RingTheory/GradedAlgebra/Basic.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Game/Basic.lean,Mathlib/SetTheory/Game/PGame.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Basic.lean,Mathlib/SetTheory/Ordinal/NaturalOps.lean,Mathlib/Tactic/GCongr/Core.lean,Mathlib/Tactic/Positivity/Basic.lean,Mathlib/Topology/ContinuousFunction/Algebra.lean,lean-toolchain,test/Recall.lean,test/propose.lean	81	36	['adomani', 'alreadydone', 'digama0', 'eric-wieser', 'ericrbg', 'jcommelin', 'leanprover-bot', 'sgouezel']	nobody	262-759 8 months ago	283-67863 9 months ago	35-56459 35 days
6491	eric-wieser author:eric-wieser	chore(Mathlib/Algebra/Hom/GroupAction): add `SMulHomClass.comp_smul`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	24/10	Mathlib/Algebra/Hom/GroupAction.lean	1	0	[]	nobody	262-758 8 months ago	283-67863 9 months ago	83-76369 83 days
6993	jjaassoonn author:jjaassoonn	feat : lemmas about `AddMonoidAlgebra.{divOf, modOf}`	--- - [x] depends on: #7582 - [x] depends on: #8975 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	147/3	Mathlib/Algebra/MonoidAlgebra/Division.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/MvPolynomial/Basic.lean,Mathlib/Data/MvPolynomial/CommRing.lean,Mathlib/Data/MvPolynomial/Division.lean	5	42	['YaelDillies', 'alreadydone', 'digama0', 'eric-wieser', 'github-actions', 'jjaassoonn', 'leanprover-community-mathlib4-bot']	nobody	262-758 8 months ago	283-67863 9 months ago	102-21189 102 days
10629	madvorak author:madvorak	feat: List.cons_sublist_append_iff_right	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data merge-conflict	11/0	Mathlib/Data/List/Basic.lean	1	1	['eric-wieser']	nobody	247-80703 8 months ago	247-80703 8 months ago	53-73442 53 days
11632	mattrobball author:mattrobball	chore(Group/RingTheory.Congruence): make `Quotient`'s reducible	These are essentially wrappers and should not expose any data when made reducible. Their use in constructing typeclass instances makes reducible transparency desirable. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict	16/35	Mathlib/GroupTheory/Congruence/Basic.lean,Mathlib/RingTheory/Congruence/Basic.lean	2	14	['eric-wieser', 'fpvandoorn', 'github-actions', 'grunweg', 'kmill', 'leanprover-bot', 'mattrobball']	nobody	243-43727 8 months ago	273-65487 8 months ago	2-10495 2 days
13791	digama0 author:digama0	refactor: Primrec and Partrec	General cleanup of the `Primrec` and `Partrec` files, to better adjust to lean 4 things. The main user-visible change is that `Primrec₂` is no longer a `def` but an `abbrev`, because it was causing inference issues in lean 4. I also removed all the nonterminal `simp`s in `PartrecCode.lean`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	tech debt t-computability merge-conflict	585/778	Mathlib/Computability/Ackermann.lean,Mathlib/Computability/Halting.lean,Mathlib/Computability/Partrec.lean,Mathlib/Computability/PartrecCode.lean,Mathlib/Computability/Primrec.lean	5	2	['github-actions', 'grunweg']	nobody	243-43548 8 months ago	283-67863 9 months ago	1-84718 1 day
14023	mattrobball author:mattrobball	perf (RingTheory.OreLocalization): make data irreducible	We generally do not want to unfold operations passing through `Quotient` if we can avoid it for performance reasons. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict	43/32	Mathlib/GroupTheory/MonoidLocalization.lean,Mathlib/RingTheory/OreLocalization/Basic.lean,Mathlib/RingTheory/OreLocalization/Ring.lean	3	4	['github-actions', 'grunweg', 'leanprover-bot', 'mattrobball']	nobody	243-43521 8 months ago	293-78934 9 months ago	0-0 0 seconds
11964	adamtopaz author:adamtopaz	feat: The functor of points of a scheme	We construct the functor of points functor, and prove that it's full and faithful. --- - [ ] depends on: #11947 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebraic-geometry t-category-theory merge-conflict	210/0	Mathlib.lean,Mathlib/AlgebraicGeometry/FunctorOfPoints.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean	3	4	['github-actions', 'grunweg', 'leanprover-community-mathlib4-bot']	nobody	243-43407 8 months ago	283-67863 9 months ago	0-1223 20 minutes
12418	rosborn author:rosborn	style: replace preimage_val with ↓∩ notation	--- This is a rough draft of what the new `↓∩` notation would look like within mathlib. I believe this is an improvement in clarity and would like to have `↓∩` as a standard notation (along with `''`, `⁻¹'`, `↑`, etc...). As `↓∩` is specialized for `Set`s, I have only changed `preimage_val` when the left-hand side of `↓∩` is a `Set`. The introduction of the `↓∩` notation to Data.Set.Image is temporary as it isn't possible to import Data.Set.Subset directly. If we want `↓∩` unscoped, where would be the best place to define it? An option is Data.Set.Defs, but the notation cannot be defined without additional imports as the file does not import `notation3`. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict	56/61	Mathlib/Analysis/InnerProductSpace/Projection.lean,Mathlib/Data/Set/Function.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/Set/Subset.lean,Mathlib/MeasureTheory/Constructions/Polish.lean,Mathlib/MeasureTheory/MeasurableSpace/Basic.lean,Mathlib/MeasureTheory/Measure/Restrict.lean,Mathlib/Order/UpperLower/Basic.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/Clopen.lean,Mathlib/Topology/Connected/Basic.lean,Mathlib/Topology/Connected/PathConnected.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/ContinuousOn.lean,Mathlib/Topology/LocalAtTarget.lean,Mathlib/Topology/LocallyConstant/Basic.lean,Mathlib/Topology/Separation.lean,Mathlib/Topology/Sober.lean	18	3	['grunweg', 'rosborn']	nobody	243-43306 8 months ago	283-67863 9 months ago	29-14218 29 days
12751	Command-Master author:Command-Master	feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size	Remove `@[simp]` from `Nat.bit_false` and `Nat.bit_true`, as `bit0` and `bit1` are deprecated, and add some lemmas to `Bits`, `Bitwise` and `Size`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data new-contributor merge-conflict	66/7	Mathlib/Data/Nat/Bits.lean,Mathlib/Data/Nat/Bitwise.lean,Mathlib/Data/Nat/Multiplicity.lean,Mathlib/Data/Nat/Size.lean	4	26	['Command-Master', 'Rida-Hamadani', 'Ruben-VandeVelde', 'YaelDillies', 'github-actions', 'jcommelin']	nobody	242-64460 7 months ago	247-80702 8 months ago	54-52408 54 days
16464	Parcly-Taxel author:Parcly-Taxel	chore: deprecate `Nat.(case_)strong_induction_on`	…in favour of the now-renamed `Nat.(case)strongInductionOn` in core.	tech debt merge-conflict	54/56	Archive/Imo/Imo1981Q3.lean,Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean,Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean,Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean,Mathlib/Algebra/Polynomial/Derivative.lean,Mathlib/Algebra/Polynomial/Lifts.lean,Mathlib/Analysis/Analytic/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Hofer.lean,Mathlib/Analysis/SpecificLimits/Normed.lean,Mathlib/Combinatorics/Derangements/Finite.lean,Mathlib/Combinatorics/Enumerative/Catalan.lean,Mathlib/Combinatorics/Hall/Finite.lean,Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean,Mathlib/Computability/Primrec.lean,Mathlib/Data/Fintype/Basic.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/Data/Nat/Choose/Central.lean,Mathlib/Data/Nat/Defs.lean,Mathlib/Data/Nat/Digits.lean,Mathlib/Data/Nat/Log.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean,Mathlib/LinearAlgebra/Multilinear/Basic.lean,Mathlib/NumberTheory/BernoulliPolynomials.lean,Mathlib/NumberTheory/DiophantineApproximation.lean,Mathlib/NumberTheory/Pell.lean,Mathlib/NumberTheory/Primorial.lean,Mathlib/Order/Fin/Basic.lean,Mathlib/RingTheory/Adjoin/PowerBasis.lean,Mathlib/RingTheory/LittleWedderburn.lean,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean,Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean,Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean,Mathlib/RingTheory/Polynomial/Nilpotent.lean,Mathlib/RingTheory/PowerSeries/Basic.lean,Mathlib/RingTheory/QuotientNilpotent.lean,Mathlib/RingTheory/WittVector/Defs.lean,Mathlib/RingTheory/WittVector/Frobenius.lean,Mathlib/RingTheory/WittVector/StructurePolynomial.lean,Mathlib/SetTheory/Surreal/Dyadic.lean,Mathlib/Topology/Metrizable/Uniformity.lean	43	13	['Parcly-Taxel', 'b-mehta', 'github-actions', 'jcommelin']	nobody	210-53016 6 months ago	210-53016 6 months ago	8-1989 8 days
17127	FR-vdash-bot author:FR-vdash-bot	chore: remove global `Quotient.mk` `⟦·⟧` notation	--- Merge this PR when we are ready to migrate to `QuotLike` API (#16421). [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data merge-conflict	137/2	Counterexamples/Pseudoelement.lean,Mathlib/Algebra/Associated/Basic.lean,Mathlib/Algebra/BigOperators/Group/Finset.lean,Mathlib/Algebra/Group/Conj.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Order/CauSeq/Completion.lean,Mathlib/Algebra/Quandle.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean,Mathlib/CategoryTheory/Abelian/Pseudoelements.lean,Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean,Mathlib/CategoryTheory/Monoidal/Free/Basic.lean,Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean,Mathlib/CategoryTheory/Skeletal.lean,Mathlib/Data/Finset/Card.lean,Mathlib/Data/Fintype/List.lean,Mathlib/Data/Fintype/Quotient.lean,Mathlib/Data/Multiset/Basic.lean,Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean,Mathlib/Data/QPF/Univariate/Basic.lean,Mathlib/Data/Quot.lean,Mathlib/Data/Real/Basic.lean,Mathlib/Data/Set/Finite.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/GroupTheory/GroupAction/Basic.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/LinearAlgebra/Dual.lean,Mathlib/LinearAlgebra/Ray.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/ModelTheory/DirectLimit.lean,Mathlib/ModelTheory/Fraisse.lean,Mathlib/ModelTheory/Quotients.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean,Mathlib/NumberTheory/NumberField/Embeddings.lean,Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean,Mathlib/NumberTheory/Padics/PadicIntegers.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/Order/RelIso/Basic.lean,Mathlib/RepresentationTheory/Action/Concrete.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Cardinal/Ordinal.lean,Mathlib/SetTheory/Game/Basic.lean,Mathlib/SetTheory/Game/Birthday.lean,Mathlib/SetTheory/Game/Impartial.lean,Mathlib/SetTheory/Game/Ordinal.lean,Mathlib/SetTheory/Game/State.lean,Mathlib/SetTheory/Lists.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Basic.lean,Mathlib/SetTheory/Surreal/Basic.lean,Mathlib/SetTheory/Surreal/Dyadic.lean,Mathlib/SetTheory/Surreal/Multiplication.lean,Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/SetTheory/ZFC/Rank.lean,Mathlib/Topology/Connected/PathConnected.lean,Mathlib/Topology/Homotopy/HomotopyGroup.lean,Mathlib/Topology/Homotopy/Path.lean,Mathlib/Topology/Homotopy/Product.lean,Mathlib/Topology/MetricSpace/GromovHausdorff.lean,Mathlib/Topology/UniformSpace/Separation.lean,test/interactiveUnfold.lean	68	1	['github-actions']	nobody	201-15399 6 months ago	201-15399 6 months ago	4-72805 4 days
8029	alreadydone author:alreadydone	refactor: Homotopy between Functions not ContinuousMaps	This allows talking about homotopies without needing to supply proofs of continuity for the two ends. This for example simplifies the definition of H-spaces. Of course, if a homotopy exists between two functions, those two functions are automatically continuous because they are restrictions of the homotopy (which is continuous) to subspaces. `Homotopy.refl` still needs a continuous map as input, and `Homotopic` is only an equivalence relation when restricted to ContinuousMap. --- TODO: fix docstrings [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-topology RFC merge-conflict	246/250	Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean,Mathlib/Topology/Homotopy/Basic.lean,Mathlib/Topology/Homotopy/Contractible.lean,Mathlib/Topology/Homotopy/Equiv.lean,Mathlib/Topology/Homotopy/HSpaces.lean,Mathlib/Topology/Homotopy/HomotopyGroup.lean,Mathlib/Topology/Homotopy/Path.lean,Mathlib/Topology/Homotopy/Product.lean	8	3	['alreadydone', 'urkud']	nobody	191-44204 6 months ago	283-67863 9 months ago	9-20043 9 days
14598	Command-Master author:Command-Master	chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc.	Add the four typeclasses `IsTopAbsorbing`, `IsBotAbsorbing`, `NoTopSum`, `NoBotSum`, as additive equivalents for `MulZeroClass` and `NoZeroDivisors`. Add instances of these for `ENNReal`, `WithTop α`, `WithBot α`, `PUnit`, `EReal`, `PartENat`, `Measure`, `Interval` and `Filter`. Also split `Algebra/Order/AddGroupWithTop` to `Algebra/Order/Group/WithTop` and `Algebra/Order/Monoid/WithTop` --- Previous usages of lemmas with quantified names like `WithTop.add_top` have to be changed to just `add_top`. `add_lt_top` is `@[simp]`, in accordance with `ENNReal.add_lt_top` being `@[simp]`. This affects `WithTop.add_lt_top` which previously hadn't been `@[simp]`. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-order t-algebra merge-conflict label:t-algebra$	264/195	Archive/Wiedijk100Theorems/BallotProblem.lean,Mathlib.lean,Mathlib/Algebra/Order/Group/WithTop.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Interval/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean,Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/Algebra/Order/Monoid/WithTop.lean,Mathlib/Algebra/PUnitInstances/Order.lean,Mathlib/Algebra/Polynomial/Degree/Definitions.lean,Mathlib/Algebra/Polynomial/Monic.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Analysis/Analytic/Meromorphic.lean,Mathlib/Analysis/Normed/Lp/ProdLp.lean,Mathlib/Analysis/NormedSpace/ENorm.lean,Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean,Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean,Mathlib/Data/ENNReal/Operations.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/Nat/WithBot.lean,Mathlib/Data/Real/EReal.lean,Mathlib/LinearAlgebra/Lagrange.lean,Mathlib/MeasureTheory/Covering/Differentiation.lean,Mathlib/MeasureTheory/Decomposition/Lebesgue.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean,Mathlib/MeasureTheory/Function/Jacobian.lean,Mathlib/MeasureTheory/Function/L1Space.lean,Mathlib/MeasureTheory/Function/L2Space.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Function/LpSpace.lean,Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean,Mathlib/MeasureTheory/Function/UniformIntegrable.lean,Mathlib/MeasureTheory/Integral/Bochner.lean,Mathlib/MeasureTheory/Integral/MeanInequalities.lean,Mathlib/MeasureTheory/Integral/SetIntegral.lean,Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean,Mathlib/MeasureTheory/Measure/Hausdorff.lean,Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/MeasureTheory/Measure/MeasureSpace.lean,Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean,Mathlib/MeasureTheory/Measure/Regular.lean,Mathlib/MeasureTheory/Measure/Typeclasses.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/Order/Filter/Pointwise.lean,Mathlib/Probability/Kernel/Defs.lean,Mathlib/Probability/Martingale/Convergence.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/UniqueFactorizationDomain.lean,Mathlib/Topology/EMetricSpace/Defs.lean,Mathlib/Topology/MetricSpace/Bounded.lean,Mathlib/Topology/MetricSpace/HausdorffDistance.lean,Mathlib/Topology/MetricSpace/Lipschitz.lean	57	30	['Command-Master', 'YaelDillies', 'github-actions']	nobody	164-10865 5 months ago	164-10865 5 months ago	7-45599 7 days
12778	MichaelStollBayreuth author:MichaelStollBayreuth	perf: decouple algebraic and order hierarchies in type class search	Based on the experience gained with [#12680](https://github.com/leanprover-community/mathlib4/pull/12680), this attempts to decouple the algebraic and order hierarchies in type class search. * We lower the priorities of instances like `OrderedSemiring.toSemiring` (which are generated by the `extends` clause with default priority 1000) to 50. * Additionally, we make the default priority available via `open scoped AlgebraOrderInstances` and use that where appropriate. Motivation: Looking at instance synthesization traces, it appears that when (e.g.) presented with the goal to find a `Semiring` instance, the algorithm frequently goes down a rabbit hole trying and failing to find order instances. This seems to be caused by the presence of instances like `OrderedSemiring.toSemiring` with default priority, which are tried early in the search, but lead nowhere (after a fairly long time). These instances are created by declarations of the form ```lean class OrderedSemiring (α : Type u) extends Semiring α, OrderedAddCommMonoid α where ... ``` which automatically sets up (among other things) an instance `OrderedSemiring.toSemiring` with default piority. It appears that these instances cannot be removed completely (only locally in a module), so the next best solution is to make them low priority (which is possible also for downstream modules). To provide for situations where these instances are desired, we put a default priority version in the scope `AlgebraOrderInstances`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	slow-typeclass-synthesis t-order t-algebra merge-conflict label:t-algebra$	306/27	Mathlib/Algebra/Algebra/Subalgebra/Order.lean,Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean,Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean,Mathlib/Algebra/Module/Rat.lean,Mathlib/Algebra/Module/Submodule/Order.lean,Mathlib/Algebra/Order/AbsoluteValue.lean,Mathlib/Algebra/Order/Algebra.lean,Mathlib/Algebra/Order/Antidiag/Prod.lean,Mathlib/Algebra/Order/Archimedean/Basic.lean,Mathlib/Algebra/Order/BigOperators/Group/Finset.lean,Mathlib/Algebra/Order/BigOperators/Group/List.lean,Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean,Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean,Mathlib/Algebra/Order/BigOperators/Ring/List.lean,Mathlib/Algebra/Order/BigOperators/Ring/Multiset.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Chebyshev.lean,Mathlib/Algebra/Order/CompleteField.lean,Mathlib/Algebra/Order/Field/Basic.lean,Mathlib/Algebra/Order/Field/Defs.lean,Mathlib/Algebra/Order/Field/Pi.lean,Mathlib/Algebra/Order/Floor.lean,Mathlib/Algebra/Order/Floor/Div.lean,Mathlib/Algebra/Order/Group/Defs.lean,Mathlib/Algebra/Order/Group/Units.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Hom/Basic.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Order/Interval/Basic.lean,Mathlib/Algebra/Order/Interval/Set/Instances.lean,Mathlib/Algebra/Order/Invertible.lean,Mathlib/Algebra/Order/Kleene.lean,Mathlib/Algebra/Order/Module/Algebra.lean,Mathlib/Algebra/Order/Module/Defs.lean,Mathlib/Algebra/Order/Module/Pointwise.lean,Mathlib/Algebra/Order/Monoid/Basic.lean,Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean,Mathlib/Algebra/Order/Monoid/Defs.lean,Mathlib/Algebra/Order/Monoid/OrderDual.lean,Mathlib/Algebra/Order/Monoid/Prod.lean,Mathlib/Algebra/Order/Nonneg/Field.lean,Mathlib/Algebra/Order/Nonneg/Ring.lean,Mathlib/Algebra/Order/Pi.lean,Mathlib/Algebra/Order/Positive/Field.lean,Mathlib/Algebra/Order/Positive/Ring.lean,Mathlib/Algebra/Order/Rearrangement.lean,Mathlib/Algebra/Order/Ring/Basic.lean,Mathlib/Algebra/Order/Ring/Defs.lean,Mathlib/Algebra/Order/Ring/InjSurj.lean,Mathlib/Algebra/Order/Ring/Pow.lean,Mathlib/Algebra/Order/Sub/WithTop.lean,Mathlib/Algebra/Order/ToIntervalMod.lean,Mathlib/Algebra/Ring/BooleanRing.lean,Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/Analysis/BoundedVariation.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean,Mathlib/Analysis/Convex/Basic.lean,Mathlib/Analysis/Convex/Cone/Basic.lean,Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Analysis/Convex/Cone/Pointed.lean,Mathlib/Analysis/Convex/Cone/Proper.lean,Mathlib/Analysis/Convex/Exposed.lean,Mathlib/Analysis/Convex/Extrema.lean,Mathlib/Analysis/Convex/Function.lean,Mathlib/Analysis/Convex/Gauge.lean,Mathlib/Analysis/Convex/GaugeRescale.lean,Mathlib/Analysis/Convex/Hull.lean,Mathlib/Analysis/Convex/Join.lean,Mathlib/Analysis/Convex/Mul.lean,Mathlib/Analysis/Convex/Quasiconvex.lean,Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean,Mathlib/Analysis/Convex/Star.lean,Mathlib/Analysis/Convex/Strict.lean,Mathlib/Analysis/InnerProductSpace/Orientation.lean,Mathlib/Analysis/MeanInequalities.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Polynomials.lean,Mathlib/Analysis/SpecificLimits/FloorPow.lean,Mathlib/Analysis/SpecificLimits/Normed.lean,Mathlib/Combinatorics/Optimization/ValuedCSP.lean,Mathlib/Combinatorics/Pigeonhole.lean,Mathlib/Combinatorics/SetFamily/FourFunctions.lean,Mathlib/Data/DFinsupp/Lex.lean,Mathlib/Data/DFinsupp/Multiset.lean,Mathlib/Data/DFinsupp/Order.lean,Mathlib/Data/Finset/MulAntidiagonal.lean,Mathlib/Data/Finsupp/Lex.lean,Mathlib/Data/Finsupp/Multiset.lean,Mathlib/Data/Finsupp/Order.lean,Mathlib/Data/Int/Log.lean,Mathlib/Data/Multiset/Antidiagonal.lean,Mathlib/Data/Multiset/Basic.lean,Mathlib/Data/Multiset/Bind.lean,Mathlib/Data/Nat/Cast/Field.lean,Mathlib/Data/Nat/Cast/Order/Basic.lean,Mathlib/Data/Nat/Choose/Bounds.lean,Mathlib/Data/PNat/Factors.lean,Mathlib/Data/Rat/Denumerable.lean,Mathlib/Data/Set/Pointwise/Interval.lean	135	34	['MichaelStollBayreuth', 'YaelDillies', 'github-actions', 'leanprover-bot']	nobody	164-9768 5 months ago	164-9768 5 months ago	18-19513 18 days
18806	FR-vdash-bot author:FR-vdash-bot	refactor: deprecate `MulEquivClass`	--- - [x] depends on: #18809 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	84/72	Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/GroupWithZero/Hom.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Ring/Divisibility/Basic.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Ideal/Norm.lean,Mathlib/RingTheory/Localization/FractionRing.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean	15	6	['FR-vdash-bot', 'github-actions', 'leanprover-bot', 'mathlib4-dependent-issues-bot', 'vihdzp']	nobody	151-53446 5 months ago	151-53446 5 months ago	4-31794 4 days
17672	urkud author:urkud	refactor: turn `IsTorsionFree` into a typeclass	Rename `Monoid.IsTorsionFree` to `IsMulTorsionFree` and turn it into a typeclass. Generalize some lemmas from (linear) ordered groups to `IsMulTorsionFree`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	256/130	Mathlib.lean,Mathlib/Algebra/CharZero/Lemmas.lean,Mathlib/Algebra/Group/IsTorsionFree/Basic.lean,Mathlib/Algebra/Group/IsTorsionFree/Defs.lean,Mathlib/Algebra/Group/IsTorsionFree/Instances.lean,Mathlib/Algebra/Module/Defs.lean,Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean,Mathlib/Algebra/Order/Group/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean,Mathlib/Algebra/Order/Ring/Basic.lean,Mathlib/Algebra/Order/ToIntervalMod.lean,Mathlib/Combinatorics/Additive/CauchyDavenport.lean,Mathlib/Data/Nat/Prime/Pow.lean,Mathlib/FieldTheory/Finite/GaloisField.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean,Mathlib/GroupTheory/Order/Min.lean,Mathlib/GroupTheory/Torsion.lean,Mathlib/NumberTheory/ArithmeticFunction.lean,Mathlib/SetTheory/Surreal/Dyadic.lean,Mathlib/Topology/Instances/AddCircle.lean,Mathlib/Topology/Instances/ZMultiples.lean	21	12	['eric-wieser', 'github-actions', 'j-loreaux', 'leanprover-bot', 'urkud']	nobody	150-5523 4 months ago	150-42290 4 months ago	24-67723 24 days
19212	Julian author:Julian	feat(LinearAlgebra): add a variable_alias for VectorSpace	Taken directly from the variable_alias docs. Zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/why.20.5Bvariable_alias.5D.20attribute.20is.20not.20used.20in.20Mathlib.3F --- This is the first actual variable alias added to mathlib. I haven't reviewed variable_alias fully, but it seems like there's at least 3 ways they could be distributed in Mathlib: * alongside whatever subfolder they "belong to" (which is what I've tentatively done here) * In a file called `Aliases` somewhere near the thing they alias (which seems less discoverable to me) * In a single file, a la `Mathlib.TrainingWheels` (with some less playful name) which is meant to define a bunch of more "friendly" aliases all in one place. I kind of like the idea of the third thing as a future module but perhaps it can be synthesized if/when there are more aliases? For now as I say I've done the first one, but please let me know if someone prefers something else. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	25/0	Mathlib.lean,Mathlib/LinearAlgebra/VectorSpace.lean,scripts/noshake.json	3	10	['Julian', 'PieterCuijpers', 'github-actions', 'urkud']	nobody	143-74020 4 months ago	143-74020 4 months ago	7-68492 7 days
19337	zeramorphic author:zeramorphic	feat(Data/Finsupp): generalise `Finsupp` to any "zero" value	Remove the explicit dependence of `Finsupp` on `[Zero M]`, instead defining `Finsupp'` (better name pending) to be functions that are equal to a fixed value `z : M` cofinitely often. This PR is intended to do the initial work of replacing the definition of `Finsupp` with an instantiation of the more general definition, without adding any appropriate API. If accepted, the API development will follow in later PRs. Issues to consider: - Naming of `Finsupp'.` - Where should `Finsupp'` lemmas go? Do they need their own file/folder under `Data/`? Relevant Zulip threads: - https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Finsupp.20generalisations - https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Finsupp-like.20partial.20function Comments are welcome. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data merge-conflict	203/83	Archive/Wiedijk100Theorems/Partition.lean,Mathlib/Algebra/MvPolynomial/Basic.lean,Mathlib/Algebra/MvPolynomial/Rename.lean,Mathlib/Algebra/MvPolynomial/Variables.lean,Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Algebra/Polynomial/Laurent.lean,Mathlib/Data/Finsupp/BigOperators.lean,Mathlib/Data/Finsupp/Defs.lean,Mathlib/Data/Finsupp/Order.lean,Mathlib/Data/Nat/Choose/Multinomial.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean,Mathlib/RingTheory/PowerBasis.lean,scripts/nolints_prime_decls.txt	13	5	['github-actions', 'vihdzp', 'zeramorphic']	nobody	141-50097 4 months ago	141-50097 4 months ago	4-60621 4 days
18756	FR-vdash-bot author:FR-vdash-bot	refactor: deprecate `DistribMulActionSemiHomClass` `MulSemiringActionSemiHomClass`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	50/28	Mathlib/Algebra/Algebra/NonUnitalHom.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/GroupTheory/GroupAction/Hom.lean	3	4	['FR-vdash-bot', 'github-actions', 'leanprover-bot']	nobody	130-15766 4 months ago	130-15766 4 months ago	31-75259 31 days
18912	b-mehta author:b-mehta	feat(SpecialFunctions/Log): more continuity and limits for logb	Continuation from #18621. From the ExponentialRamsey project. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis merge-conflict	144/17	Mathlib/Analysis/SpecialFunctions/Log/Base.lean,Mathlib/Data/Set/Pointwise/Interval.lean,Mathlib/Topology/Algebra/Order/Field.lean	3	9	['b-mehta', 'dupuisf', 'github-actions', 'j-loreaux']	nobody	129-60280 4 months ago	129-60280 4 months ago	1-18352 1 day
19046	j-loreaux author:j-loreaux	feat: define class `SemigroupAction`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	34/25	Mathlib/Algebra/Category/ModuleCat/Presheaf.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean,Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/End.lean,Mathlib/Algebra/Group/Action/Prod.lean,Mathlib/Algebra/Group/Action/TypeTags.lean,Mathlib/Algebra/Polynomial/Laurent.lean,Mathlib/Analysis/Distribution/SchwartzSpace.lean,Mathlib/GroupTheory/CoprodI.lean,Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean,Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean	11	7	['alreadydone', 'github-actions', 'j-loreaux', 'leanprover-bot', 'urkud']	nobody	126-63650 4 months ago	126-63651 4 months ago	6-21105 6 days
18748	FR-vdash-bot author:FR-vdash-bot	refactor: deprecate `ContinuousLinearMapClass`	--- - [ ] depends on: #18689 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra t-topology merge-conflict label:t-algebra$	115/49	Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Operator/LinearIsometry.lean,Mathlib/Topology/Algebra/Module/Basic.lean,Mathlib/Topology/Algebra/Module/CharacterSpace.lean,Mathlib/Topology/Algebra/Module/FiniteDimension.lean,Mathlib/Topology/Algebra/Module/StrongTopology.lean,Mathlib/Topology/Algebra/Module/WeakDual.lean,Mathlib/Topology/Homeomorph.lean	10	5	['FR-vdash-bot', 'github-actions', 'leanprover-bot', 'mathlib4-dependent-issues-bot']	nobody	123-66179 4 months ago	123-66182 4 months ago	0-989 16 minutes
20527	trivial1711 author:trivial1711	refactor(Topology/UniformSpace/Completion): more descriptive names for `α → Completion α`	- We rename the various maps `α → Completion α` in order to make their names more consistent. - Let `α` be a uniform space. We rename the uniformly continuous function `α → Completion α` from `UniformSpace.Completion.coe'` to `UniformSpace.Completion.coe`. - Let `α` be a uniform additive group. We rename the additive group homomorphism `α →+ Completion α` from `UniformSpace.Completion.toCompl` to `UniformSpace.Completion.coeAddHom`. - Let `α` be a uniform ring. The ring homomorphism `α →+* Completion α` is called `UniformSpace.Completion.coeRingHom`; its name is unchanged. - Let `α` be a normed space over a field `𝕜`. We rename the linear isometry `α →ₗᵢ[𝕜] Completion α` from `UniformSpace.Completion.toComplₗᵢ` to `UniformSpace.Completion.coeₗᵢ`. - Let `α` be a normed space over a field `𝕜`. We rename the continuous linear map `α →L[𝕜] Completion α` from `UniformSpace.Completion.toComplL` to `UniformSpace.Completion.coeL`. - Let `α` be a normed additive group. We rename the norm preserving homomorphism `NormedAddGroupHom α (Completion α)` from `NormedAddCommGroup.toCompl` to `UniformSpace.Completion.coeNormedAddGroupHom`. - We analogously rename some other theorems. - We add some trivial theorems (all of which are proved by `rfl`) that state that the functions considered above are equal. We give all of them the `simp` and `norm_cast` attributes. - We add a new theorem `UniformSpace.Completion.coeAddHom_eq_coe` that states that `UniformSpace.Completion.coeAddHom` and `UniformSpace.Completion.coe` are equal as functions. - We similarly add a new theorem `UniformSpace.Completion.coeRingHom_eq_coe`. - We rename the theorem `UniformSpace.Completion.coe_toComplₗᵢ` to `UniformSpace.Completion.coeₗᵢ_eq_coe`. - We rename the theorem `UniformSpace.Completion.coe_toComplL` to `UniformSpace.Completion.coeL_eq_coe`. - We similarly add a new theorem `UniformSpace.Completion.coeNormedAddGroupHom_eq_coe`. - We change all occurrences of the string `((↑) : α → Completion α)` to `(coe : α → Completion α)` or just `coe`. - We put the statements of some theorems into simp normal form by using the plain function `coe` rather than the homomorphisms that carry more structure. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-topology merge-conflict	130/92	Mathlib/Analysis/Analytic/Uniqueness.lean,Mathlib/Analysis/Calculus/FDeriv/Analytic.lean,Mathlib/Analysis/Complex/AbsMax.lean,Mathlib/Analysis/Complex/Liouville.lean,Mathlib/Analysis/InnerProductSpace/Completion.lean,Mathlib/Analysis/Normed/Group/HomCompletion.lean,Mathlib/Analysis/Normed/Module/Completion.lean,Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean,Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean,Mathlib/Topology/Algebra/GroupCompletion.lean,Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean,Mathlib/Topology/Algebra/InfiniteSum/Nonarchimedean.lean,Mathlib/Topology/Algebra/Nonarchimedean/Completion.lean,Mathlib/Topology/Algebra/UniformRing.lean,Mathlib/Topology/Category/UniformSpace.lean,Mathlib/Topology/MetricSpace/Completion.lean,Mathlib/Topology/UniformSpace/Completion.lean	17	4	['eric-wieser', 'github-actions', 'trivial1711']	nobody	95-62972 3 months ago	95-62972 3 months ago	6-66637 6 days
18474	FR-vdash-bot author:FR-vdash-bot	perf: lower the priority of `WithOne.to` instances	--- From #7873. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data slow-typeclass-synthesis t-algebra merge-conflict label:t-algebra$	9/2	Mathlib/Algebra/Polynomial/BigOperators.lean,Mathlib/Data/Int/Cast/Defs.lean,Mathlib/Data/Nat/Cast/Defs.lean	3	7	['FR-vdash-bot', 'eric-wieser', 'github-actions', 'leanprover-bot']	nobody	93-50002 3 months ago	93-50002 3 months ago	76-67978 76 days
19091	Vierkantor author:Vierkantor	chore(Algebra/MonoidAlgebra): split Defs.lean further	This PR further splits the big file `MonoidAlgebra/Defs.lean` to focus on the ring structure on (`Add`)`MonoidAlgebra`. The following files have been split off: * `MonoidAlgebra/Lift.lean`: definition of `liftNC` * `MonoidAlgebra/MapDomain.lean`: definition of `mapDomain` * `MonoidAlgebra/Module.lean`: module structure (and some submodule results) * `MonoidAlgebra/Opposite.lean`: results on the `MulOpposite` ring structure I also changed one proof about scalar multiplication by natural numbers, so that it wouldn't need a full on module structure on `Finsupp`. This required adding a pair of lemmas on the definition of multiplying `Finsupp`s by natural numbers. --- - [ ] depends on: #19087 - [ ] depends on: #19205 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	883/560	Mathlib.lean,Mathlib/Algebra/MonoidAlgebra/Basic.lean,Mathlib/Algebra/MonoidAlgebra/Defs.lean,Mathlib/Algebra/MonoidAlgebra/Division.lean,Mathlib/Algebra/MonoidAlgebra/Lift.lean,Mathlib/Algebra/MonoidAlgebra/MapDomain.lean,Mathlib/Algebra/MonoidAlgebra/Module.lean,Mathlib/Algebra/MonoidAlgebra/Opposite.lean,Mathlib/Algebra/MonoidAlgebra/Support.lean,Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Data/Finsupp/Defs.lean,Mathlib/RingTheory/Polynomial/Opposites.lean	12	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	92-71519 3 months ago	92-71519 3 months ago	2-72196 2 days
20372	jvlmdr author:jvlmdr	feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L)	Introduce ContinuousLinearMap.bilinearCompLp and bilinearCompLpL. Generalize eLpNorm_le_eLpNorm_mul_eLpNorm theorems to include constant C in bound condition. --- Expect this may be useful for defining tempered distributions from functions in `L^p`. The definitions more or less follow `ContinuousLinearMap.compLp...`. Names are loosely analogous to `ContinuousLinearMap.bilinearComp` and `SchwartzMap.bilinLeftCLM`. Note: I preferred the spelling `hpqr : p⁻¹ + q⁻¹ = r⁻¹` with `f` in `L^p` and `g` in `L^q` to `hpqr : 1 / p = 1 / q + 1 / r`. It's easier to obtain from `ENNReal.IsConjExponent` too. A few questions: - [ ] I defined `bilinear{Left,Right}LpL` in addition to `bilinearCompLpL` because `LinearMap.mkContinuous₂` is marked as `noncomputable` and `LinearMap.mkContinuous` is not. Is this worth the extra definitions? (Note: This is not visible in the source due to `noncomputable section`.) - [ ] Should I use `C : ℝ` instead of `C : NNReal` for `eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm'`? - [ ] Is it going to be painful to have `[Fact (1 ≤ p)] [Fact (1 ≤ q)] [Fact (1 ≤ r)]`? I don't think there's a way to avoid it though. Maybe providing specialized versions for `p.IsConjExponent q` with `L^1`? Naming: - [ ] Is it satisfactory to add a `'` to the `eLpNorm_le_eLpNorm_mul_eLpNorm ` definitions in `CompareExp.lean` where `≤ ‖f x‖ * ‖g x‖` has been replaced with `≤ C * ‖f x‖ * ‖g x‖`? These could replace the existing theorems, although I don't want to break backwards compatibility. There are 5 instances: `eLpNorm_le_eLpNorm_top_mul_eLpNorm'`, `eLpNorm_le_eLpNorm_mul_eLpNorm_top'`, `eLpNorm'_le_eLpNorm'_mul_eLpNorm''`, `eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm'`, `eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm'` (I'm not sure why the existing theorem `eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm` has an internal `'`) - [ ] Is `bilinearLeftLpL` a suitable name? Other options: `bilinearCompLpLeftL`, `bilinearCompLeftLpL`, `bilinLeftLpL` (analogous to `SchwartzMap.bilinLeftCLM`) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-measure-probability merge-conflict	203/40	Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSpace.lean	2	1	['github-actions']	nobody	80-74259 2 months ago	80-74259 2 months ago	27-43617 27 days
21948	ChrisHughes24 author:ChrisHughes24	feat(ModelTheory): Formula.iSup and iInf	--- This was a slightly controversial addition discussed in #20175 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-logic merge-conflict	24/7	Mathlib/ModelTheory/Semantics.lean,Mathlib/ModelTheory/Syntax.lean	2	5	['YaelDillies', 'github-actions']	nobody	60-63719 2 months ago	60-63719 2 months ago	1-18127 1 day
18463	vihdzp author:vihdzp	feat(SetTheory/Ordinal/Notation/FundamentalSequence): define type of fundamental sequences	We define `Sequence α` as the type of sequences with length 0, 1, or `ω`, and give a basic API. A subsequent PR will introduce the notion of a (countable and computable) fundamental sequence and establish basic results. The goal of this is to generalize [`ONote.fundamentalSequence`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Ordinal/Notation.html#ONote.fundamentalSequence) to allow the construction of fundamental sequences for other ordinal notations. --- See [my ordinal notation repository](https://github.com/vihdzp/ordinal-notation/blob/a6fdd7fe7cb521e686ea271902e7e5496f1804d3/OrdinalNotation/Cantor.lean#L1218) for a demonstration of how this API looks in practice. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory t-order merge-conflict	174/1	Mathlib.lean,Mathlib/SetTheory/Ordinal/Notation/Cantor.lean,Mathlib/SetTheory/Ordinal/Notation/FundamentalSequence.lean	3	19	['YnirPaz', 'b-mehta', 'github-actions', 'vihdzp']	nobody	59-12001 2 months ago	59-12001 2 months ago	52-25108 52 days
21099	chrisflav author:chrisflav	chore(RingTheory/Generators): use unification hints for variables and relations	When working with generators and presentations, we rely on the `MvPolynomial` API, but since the type of variables is bundled in `Generators R S`, many lemmas don't apply with `rw` or `simp`, because they can't see through the definition of `vars` in constructions such as `Generators.comp` and `Generators.localizationAway`. A possible approach is to make all of these constructions `abbrev`s, but this causes `simp` to also unfold `val` which is not always desirable. More generally, it is then harder to predict how instance search and `simp` behave. This approach is tried in #21050, but causes many regressions. This approach is less invasive, as it uses `unif_hint` to unify the `vars` (and `rels`) fields of constructions with the correct type. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	231/91	Mathlib/Algebra/Module/Presentation/Differentials.lean,Mathlib/RingTheory/Generators.lean,Mathlib/RingTheory/Kaehler/JacobiZariski.lean,Mathlib/RingTheory/Presentation.lean,Mathlib/RingTheory/Smooth/StandardSmooth.lean	5	16	['chrisflav', 'erdOne', 'github-actions', 'leanprover-bot', 'mattrobball']	nobody	54-57237 1 month ago	54-57237 1 month ago	27-75210 27 days
4979	mhk119 author:mhk119	doc(Data/Nat/Bitblast): initial commit	Initial commit of Bitblast.lean where we prove equivalence of bitblast unsigned less than and bitblast addition. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict	202/4	Mathlib/Data/Bool/Basic.lean,Mathlib/Data/Nat/Bitwise.lean,Mathlib/Data/Nat/Pow.lean	3	49	['ChrisHughes24', 'digama0', 'goens', 'grunweg', 'j-loreaux', 'kim-em', 'mhk119']	nobody	48-53566 1 month ago	283-67863 9 months ago	7-68358 7 days
13964	pechersky author:pechersky	feat(Data/DigitExpansion): begin defining variant of reals without rationals	Based on a de Bruijn 1976 paper. This file is just the basic definition of a digit expansion. Will be followed up with furhter constructions. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data merge-conflict	518/0	Mathlib.lean,Mathlib/Data/DigitExpansion/Defs.lean,docs/references.bib	3	11	['eric-wieser', 'github-actions', 'kim-em', 'pechersky']	dupuisf assignee:dupuisf	46-60342 1 month ago	173-76850 5 months ago	129-57991 129 days
21339	vihdzp author:vihdzp	fix(Data/List/Lex): remove duplicate `List.LE` instance	Mathlib currently duplicates the Lean core instance for `≤` in lists in an incompatible way. We delete this duplicate instance. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Two.20.60List.2ELE.60.20instances.3F/near/497241115). --- This is a very quick and dirty fix. Core Lean provides all of the theorems we need to prove `≤` forms a linear order, but it provides them in terms of `Std` relation typeclasses which currently see no use in Mathlib. I've added the instances that were required to get the list theorems working. In the future, we really ought to unify the core and Mathlib relation typeclasses. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data merge-conflict	24/22	Mathlib/Data/List/Lex.lean,Mathlib/Data/String/Basic.lean,Mathlib/Topology/Category/Profinite/Nobeling.lean	3	1	['github-actions']	nobody	46-56129 1 month ago	46-56129 1 month ago	16-65973 16 days
21959	BGuillemet author:BGuillemet	feat(Topology/ContinuousMap): Stone-Weierstrass theorem for MvPolynomial	Add the subalgebra of multivariate polynomials and prove it separates points, on the same model as `ContinuousMap/Polynomial.lean`. Prove the Stone-Weierstrass theorem and some variations for multivariate polynomials. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-topology merge-conflict	285/1	Mathlib.lean,Mathlib/Topology/ContinuousMap/MvPolynomial.lean,Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean	3	1	['github-actions']	nobody	44-60280 1 month ago	44-60280 1 month ago	16-76141 16 days
22603	pechersky author:pechersky	chore(Topology): rename pi family from π to X	Only in files that mentioned such a family, via a script: ``` git grep -e "π : . → Type" --name-only \| rg Topology \| xargs -I{} sed -i -e 's/π/X/g' {} ``` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	tech debt t-topology merge-conflict	232/232	Mathlib/Topology/AlexandrovDiscrete.lean,Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean,Mathlib/Topology/Algebra/Module/Equiv.lean,Mathlib/Topology/Algebra/Order/LiminfLimsup.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/Bornology/Constructions.lean,Mathlib/Topology/Connected/Basic.lean,Mathlib/Topology/Connected/Clopen.lean,Mathlib/Topology/Connected/LocallyConnected.lean,Mathlib/Topology/Connected/TotallyDisconnected.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/ContinuousOn.lean,Mathlib/Topology/EMetricSpace/Diam.lean,Mathlib/Topology/EMetricSpace/Pi.lean,Mathlib/Topology/ExtremallyDisconnected.lean,Mathlib/Topology/Inseparable.lean,Mathlib/Topology/MetricSpace/Basic.lean,Mathlib/Topology/MetricSpace/Infsep.lean,Mathlib/Topology/MetricSpace/ProperSpace.lean,Mathlib/Topology/MetricSpace/Pseudo/Pi.lean,Mathlib/Topology/Metrizable/Basic.lean,Mathlib/Topology/Order/Basic.lean,Mathlib/Topology/Separation/Hausdorff.lean,Mathlib/Topology/UniformSpace/Ascoli.lean	24	1	['github-actions']	nobody	38-62011 1 month ago	38-62011 1 month ago	5-80034 5 days
22660	Ruben-VandeVelde author:Ruben-VandeVelde	chore: follow naming convention around Group.IsNilpotent	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	133/67	Mathlib/GroupTheory/Frattini.lean,Mathlib/GroupTheory/Nilpotent.lean,Mathlib/GroupTheory/SpecificGroups/ZGroup.lean	3	1	['github-actions']	nobody	32-82535 1 month ago	32-82535 1 month ago	10-48025 10 days
21856	vihdzp author:vihdzp	chore(SetTheory/Cardinal/Basic): generalize universes of `sum_le_iSup_lift`	We prove a more general version of the lemma which talks about families `ι → Cardinal.{v}` with `Small.{v} ι`, rather than just families `f : ι → Cardinal.{max u v}` with `ι : Type v`. We keep the old version, as it's seemingly more useful under common circumstances. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory merge-conflict	16/10	Mathlib/SetTheory/Cardinal/Basic.lean	1	6	['b-mehta', 'github-actions', 'vihdzp']	nobody	31-73769 1 month ago	31-73769 1 month ago	32-26420 32 days
21751	vihdzp author:vihdzp	refactor(SetTheory/Ordinal/Arithmetic): rework `Ordinal.pred` API	This PR does the following: - give a simpler definition of `Ordinal.pred` - replace `¬ ∃ a, o = succ a` and `∀ a, o ≠ succ a` by `IsSuccPrelimit o` throughout - improve theorem names --- There's a legitimate question of whether we even want `Ordinal.pred` (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ordinal.2Epred)) but this should be a good change in the meanwhile regardless. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory maintainer-merge merge-conflict	102/67	Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean	2	12	['YaelDillies', 'github-actions', 'vihdzp']	nobody	29-16418 29 days ago	29-16418 29 days ago	36-50134 36 days
22027	vihdzp author:vihdzp	chore(SetTheory/Ordinal/FixedPoint); review `Ordinal.nfp` API	This PR does the following: - add `iff` variants of various theorems, renaming some in the process - weaken some assumptions slightly - golf throughout --- - [x] depends on: #22017 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory merge-conflict	64/61	Mathlib/Logic/Equiv/List.lean,Mathlib/SetTheory/Ordinal/FixedPoint.lean	2	3	['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot']	nobody	13-40287 13 days ago	16-7247 16 days ago	43-68322 43 days
22966	alreadydone author:alreadydone	feat(RingTheory): rank of rational function field extension	+ `IsAlgebraic/IsIntegral R S` + `IsPushout R S R' S'` ⇒ `IsAlgebraic/IsIntegral R' S'` (for the "IsAlgebraic" version we currently need to assume `NoZeroDivisor R'` and `FaithfulSMul R R'` (i.e. `Injective (algebraMap R R')`) + `IsAlgebraic R S` + `IsFractionRing R R'` + `IsFractionRing S S'` ⇒ `IsPushout R S R' S'` (need to assume `FaithfulSMul R S` + `NonZeroDivisors S`) As consequences, we have `rank (f R) (f S) = rank R S` for `f = FractionRing (Polynomial ·)` or `FractionRing (MvPolynomial _ ·)` assuming `IsAlgebraic R S` + `IsDomain S` + `FaithfulSMul R S`. (For `f = Polynomial` or `MvPolynomial _`, `NoZeroDivisors R` is enough by #23095.) --- - [x] depends on: #23095 - [x] depends on: #23096 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	270/46	Mathlib/RingTheory/AdjoinRoot.lean,Mathlib/RingTheory/Algebraic/Basic.lean,Mathlib/RingTheory/Algebraic/Integral.lean,Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean,Mathlib/RingTheory/TensorProduct/Basic.lean	5	10	['Louddy', 'alreadydone', 'github-actions', 'leanprover-bot', 'mathlib4-dependent-issues-bot']	nobody	12-47703 12 days ago	12-47703 12 days ago	14-3730 14 days
13861	BoltonBailey author:BoltonBailey	feat(Data/Finsupp/Basic): `Finsupp.optionElim'`	Similar to how `Finsupp.cons` constructs a map `Fin (n + 1) →₀ M` from a map `Fin n →₀ M`, we define `Finsupp.optionElim'` to construct a map `Option α →₀ M` from a map `α →₀ M`, given an additional value for `none`. As a function, it behaves as `Option.elim'`, hence the name. We prove a variety of API lemmas, based on those for `Finsupp.cons`, to bring the definitions more in line with the contents of `Data/Finsupp/Fin`. We also do some light refactoring for succinctness, and put this any related preexisting lemmas in a new file to not trigger the linter. Needed by #12664 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data merge-conflict	204/62	Mathlib.lean,Mathlib/Algebra/Category/MonCat/Adjunctions.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Finsupp/Option.lean,Mathlib/Data/Finsupp/Single.lean,Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean	6	1	['github-actions']	nobody	12-38872 12 days ago	12-38872 12 days ago	12-6613 12 days
21858	vihdzp author:vihdzp	refactor(SetTheory/Ordinal/FixedPoint): redefine `Ordinal.deriv`	We previously defined the [ordinal derivative](https://en.wikipedia.org/wiki/Normal_function#Properties) of a function as the unique normal function satisfying `deriv f 0 = nfp f 0` and `deriv f (o + 1) = nfp f (deriv f o)` (where `nfp f a` is the next fixed point of `f` that's `≥ a`). The motivation here was to give a "nice" junk value on non-normal functions (the function is normal no matter what). However, in practice, this definition makes it unwieldy to prove things, by either requiring a tedious zero/successor/limit argument, or requiring one to rewrite `deriv f = enumOrd (fixedPoints f)`. We can instead define `deriv f = enumOrd (fixedPoints f)`. At the cost of giving "worse" junk values (which we have no legitimate uses of), we're able to much more easily prove all the expected properties in the standard case where `f` is a normal function. Finally, we do some drive-by API cleanup. --- - [ ] depends on: #21860 - [ ] depends on: #21970 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory merge-conflict	216/262	Mathlib/Logic/Equiv/List.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean,Mathlib/SetTheory/Ordinal/Enum.lean,Mathlib/SetTheory/Ordinal/FixedPoint.lean,Mathlib/SetTheory/Ordinal/Principal.lean,Mathlib/SetTheory/Ordinal/Veblen.lean	6	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	12-38334 12 days ago	12-38336 12 days ago	0-1601 26 minutes
22701	ctchou author:ctchou	feat(Combinatorics): the Katona circle method	This file formalizes the Katona circle method. From PlainCombi (LeanCamCombi): https://github.com/YaelDillies/LeanCamCombi/blob/master/LeanCamCombi/PlainCombi/KatonaCircle.lean Co-authored-by: Yaël Dillies	new-contributor t-combinatorics merge-conflict	121/0	Mathlib.lean,Mathlib/Combinatorics/KatonaCircle.lean	2	1	['github-actions']	nobody	12-36049 12 days ago	12-36049 12 days ago	30-8337 30 days
23411	PatrickMassot author:PatrickMassot	chore: remove finiteness from Order.Filter.Lift	Co-authored-by: Anatole Dedecker --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	longest-pole t-topology merge-conflict	48/21	Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean,Mathlib/Order/Filter/Basic.lean,Mathlib/Order/Filter/Finite.lean,Mathlib/Order/Filter/Lift.lean,Mathlib/Order/Filter/SmallSets.lean,Mathlib/Topology/Algebra/ContinuousMonoidHom.lean,Mathlib/Topology/Basic.lean	7	4	['Vierkantor', 'github-actions', 'kim-em', 'leanprover-community-bot-assistant']	nobody	10-82763 10 days ago	11-15932 11 days ago	10-21608 10 days
21573	lambda-fairy author:lambda-fairy	feat(Computability): regular languages are closed under reversal	This PR proves that regular languages are closed under reversal. It works by reversing the transitions in the NFA, and proving that the resulting automaton matches the reversed language. The argument proceeds by induction on the input word, ensuring that, at each character, the state sets for the forward and reverse automaton correspond to each other. I also clean up the existing NFA module, which includes making the `M` argument implicit by default. I can revert that if it's controversial. Thank you @Rob23oba for their help with the induction proof. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-computability merge-conflict	75/7	Mathlib/Computability/NFA.lean	1	8	['github-actions', 'lambda-fairy', 'madvorak', 'meithecatte', 'tristan-f-r']	nobody	10-32393 10 days ago	44-74644 1 month ago	24-86139 24 days
21488	imbrem author:imbrem	feat(CategoryTheory/Monoidal): premonoidal categories	Add support for premonoidal categories --- Still want to add support for: - Premonoidal braided/symmetric categories - The monoidal coherence theorem, which I've already ported in my `discretion` library - The `coherence` tactic, which should work fine for premonoidal categories too but wanted to get this in front of reviewers ASAP to make sure my general approach was alright [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-category-theory merge-conflict	900/361	Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean,Mathlib/CategoryTheory/Bicategory/End.lean,Mathlib/CategoryTheory/GradedObject/Monoidal.lean,Mathlib/CategoryTheory/Localization/Monoidal.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Center.lean,Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/CategoryTheory/Monoidal/End.lean,Mathlib/CategoryTheory/Monoidal/Free/Basic.lean,Mathlib/CategoryTheory/Monoidal/Functor.lean,Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/CategoryTheory/Monoidal/Opposite.lean,Mathlib/CategoryTheory/Monoidal/Transport.lean,Mathlib/Tactic/CategoryTheory/Monoidal/Datatypes.lean,Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean,Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean,Mathlib/Tactic/CategoryTheory/MonoidalComp.lean,MathlibTest/StringDiagram.lean	21	9	['YaelDillies', 'github-actions', 'grunweg', 'imbrem', 'kim-em', 'leanprover-community-bot-assistant']	nobody	9-68682 9 days ago	9-68683 9 days ago	58-20339 58 days
21525	sinhp author:sinhp	feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim)	This PR defines the basic preliminaries for defining locally cartesian closed categories (LCCCs). In particular, using the calculus of mates we define certain natural isomorphisms involving `Over.star` and `Over.pullback` which will be crucial in defining the right adjoint to the pullback functor in the development of LCCCs. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import t-category-theory merge-conflict	338/24	Mathlib/CategoryTheory/Comma/Over/Basic.lean,Mathlib/CategoryTheory/Comma/Over/Pullback.lean,Mathlib/CategoryTheory/Galois/Examples.lean	3	13	['b-mehta', 'github-actions', 'joelriou', 'leanprover-community-bot-assistant', 'sinhp']	nobody	9-68680 9 days ago	9-68682 9 days ago	43-83249 43 days
21673	erdOne author:erdOne	feat: `∑ z ∈ L, ‖z - x‖⁻ʳ` converges for lattices `L`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis merge-conflict	329/0	Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Disjoint.lean,Mathlib/Algebra/Module/ZLattice/Summable.lean,Mathlib/Order/Disjointed.lean	4	4	['github-actions', 'leanprover-community-bot-assistant', 'xroblot']	nobody	9-9678 9 days ago	9-9680 9 days ago	27-73279 27 days
23670	Vierkantor author:Vierkantor	feat(Tactic/Linter): one option for all Mathlib linters	This is intended to make downstream projects easier to maintain and keep up to Mathlib standards, by having one option `linter.mathlibStandard` control all the linters that we previously had to enable one by one in the lakefile. This is accomplished by introducing a new check `Mathlib.getLinterValue` that takes the `linter.mathlibStandard` option into account. If that option is set to true, it checks if this is one of the Mathlib standard linters, and enables the linter if so. I also considered a few ways of implementing this feature by setting options automatically. But I couldn't get any to work without modifying Lean itself: * an `initialize` command doesn't get access to the options in the current file (since it runs in IO rather than CoreM), * hooking the `runLinters` step of elaboration doesn't work because each linter restores the state (including options) after running. A drawback of the current approach is that a linter defined upstream of Mathlib cannot be enabled this way. There is no such linter currently, and we can fall back to the previous `lakefile` approach if that happens. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import t-linter merge-conflict	135/47	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/Attr.lean,Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean,Mathlib/Tactic/Linter/DocPrime.lean,Mathlib/Tactic/Linter/DocString.lean,Mathlib/Tactic/Linter/FlexibleLinter.lean,Mathlib/Tactic/Linter/GlobalAttributeIn.lean,Mathlib/Tactic/Linter/HashCommandLinter.lean,Mathlib/Tactic/Linter/Header.lean,Mathlib/Tactic/Linter/Lint.lean,Mathlib/Tactic/Linter/MinImports.lean,Mathlib/Tactic/Linter/Multigoal.lean,Mathlib/Tactic/Linter/OldObtain.lean,Mathlib/Tactic/Linter/PPRoundtrip.lean,Mathlib/Tactic/Linter/Style.lean,Mathlib/Tactic/Linter/UnusedTactic.lean,Mathlib/Tactic/Linter/UpstreamableDecl.lean,MathlibTest/MathlibStandardLints.lean,lakefile.lean,scripts/lint-style.lean	22	4	['Vierkantor', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant']	nobody	9-8956 9 days ago	9-8958 9 days ago	5-52291 5 days
16314	FR-vdash-bot author:FR-vdash-bot	chore(Data/Quot): deprecate `ind*'` APIs	--- - [x] depends on: #16264 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data merge-conflict	247/287	Counterexamples/CliffordAlgebraNotInjective.lean,Mathlib/Algebra/Colimit/Module.lean,Mathlib/Algebra/Lie/Quotient.lean,Mathlib/Algebra/Module/Torsion.lean,Mathlib/Algebra/RingQuot.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/CategoryTheory/ConnectedComponents.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/Computability/Reduce.lean,Mathlib/Computability/Tape.lean,Mathlib/Data/List/Cycle.lean,Mathlib/Data/Multiset/MapFold.lean,Mathlib/Data/Multiset/ZeroCons.lean,Mathlib/Data/Quot.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/FieldTheory/Fixed.lean,Mathlib/GroupTheory/Complement.lean,Mathlib/GroupTheory/Congruence/Basic.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/GroupTheory/Congruence/Hom.lean,Mathlib/GroupTheory/Coset/Basic.lean,Mathlib/GroupTheory/Coset/Defs.lean,Mathlib/GroupTheory/FreeAbelianGroup.lean,Mathlib/GroupTheory/GroupAction/Basic.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/GroupTheory/Index.lean,Mathlib/GroupTheory/MonoidLocalization/Basic.lean,Mathlib/GroupTheory/PGroup.lean,Mathlib/GroupTheory/Perm/Cycle/Concrete.lean,Mathlib/GroupTheory/PresentedGroup.lean,Mathlib/GroupTheory/QuotientGroup/Basic.lean,Mathlib/GroupTheory/QuotientGroup/Defs.lean,Mathlib/GroupTheory/SchurZassenhaus.lean,Mathlib/GroupTheory/Sylow.lean,Mathlib/LinearAlgebra/Alternating/DomCoprod.lean,Mathlib/LinearAlgebra/Projectivization/Basic.lean,Mathlib/LinearAlgebra/Quotient/Basic.lean,Mathlib/LinearAlgebra/Quotient/Defs.lean,Mathlib/MeasureTheory/Function/AEEqFun.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/NumberTheory/RamificationInertia/Basic.lean,Mathlib/Order/Antisymmetrization.lean,Mathlib/Order/Category/PartOrd.lean,Mathlib/Order/Filter/Germ/Basic.lean,Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean,Mathlib/RingTheory/AdicCompletion/Algebra.lean,Mathlib/RingTheory/AdicCompletion/Basic.lean,Mathlib/RingTheory/AdicCompletion/Functoriality.lean,Mathlib/RingTheory/AdjoinRoot.lean,Mathlib/RingTheory/Congruence/Basic.lean,Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean,Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean,Mathlib/RingTheory/Ideal/Cotangent.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/RingTheory/Ideal/Quotient/Basic.lean,Mathlib/RingTheory/Ideal/Quotient/Defs.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/Valuation/Quotient.lean,Mathlib/Topology/Algebra/Group/TopologicalAbelianization.lean,Mathlib/Topology/Algebra/InfiniteSum/Module.lean,Mathlib/Topology/Separation/Basic.lean	65	4	['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot']	nobody	4-7246 4 days ago	4-7248 4 days ago	55-52030 55 days
23211	Parcly-Taxel author:Parcly-Taxel	chore: automatically deprime common `induction'` uses	Replace `induction'` with `induction` for the following targets: ```python rep_dict = {("Nat", "~", 2): [("zero", 0), ("succ", 2)], ("Nat", "strong_induction_on", 1): [("h", 2)], ("Nat", "case_strong_induction_on", 2): [("hz", 0), ("hi", 2)], ("Nat", "le_induction", 2): [("base", 0), ("succ", 3)], ("List", "~", 2): [("nil", 0), ("cons", 3)], ("List", "reverseRecOn", 2): [("nil", 0), ("append_singleton", 3)], ("Multiset", "induction_on", 2): [("empty", 0), ("cons", 3)], ("Finset", "induction", 2): [("empty", 0), ("@insert", 4)], ("Finset", "induction_on", 2): [("empty", 0), ("@insert", 4)], ("MvPolynomial", "induction_on'", 2): [("monomial", 2), ("add", 4)], ("MvPolynomial", "induction_on", 3): [("C", 1), ("add", 4), ("mul_X", 3)]} ``` The script and the data file used can be found [here](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/The.20plan.20to.20remove.20induction'/near/508218834).	tech debt merge-conflict	2189/1565	Archive/Imo/Imo1977Q6.lean,Archive/Imo/Imo2006Q5.lean,Archive/Imo/Imo2013Q1.lean,Archive/Imo/Imo2013Q5.lean,Archive/Imo/Imo2019Q4.lean,Archive/Imo/Imo2024Q1.lean,Archive/MiuLanguage/DecisionSuf.lean,Archive/Sensitivity.lean,Archive/Wiedijk100Theorems/FriendshipGraphs.lean,Archive/Wiedijk100Theorems/Partition.lean,Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean,Mathlib/Algebra/Group/Conj.lean,Mathlib/Algebra/Group/ForwardDiff.lean,Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean,Mathlib/Algebra/Group/Pointwise/Set/Finite.lean,Mathlib/Algebra/Group/Pointwise/Set/ListOfFn.lean,Mathlib/Algebra/Lie/Solvable.lean,Mathlib/Algebra/Module/PID.lean,Mathlib/Algebra/Order/BigOperators/Group/List.lean,Mathlib/Algebra/Order/CauSeq/BigOperators.lean,Mathlib/Algebra/Order/Group/Multiset.lean,Mathlib/Algebra/Polynomial/BigOperators.lean,Mathlib/Algebra/Polynomial/Degree/Lemmas.lean,Mathlib/Algebra/Polynomial/Derivative.lean,Mathlib/Algebra/Polynomial/EraseLead.lean,Mathlib/Algebra/Polynomial/Eval/Defs.lean,Mathlib/Algebra/Polynomial/HasseDeriv.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Tropical/BigOperators.lean,Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean,Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/AlgebraicTopology/DoldKan/Projections.lean,Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean,Mathlib/Analysis/BoxIntegral/Partition/Additive.lean,Mathlib/Analysis/BoxIntegral/Partition/Split.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/Analysis/CStarAlgebra/Multiplier.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/Deriv/ZPow.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/Analysis/Calculus/SmoothSeries.lean,Mathlib/Analysis/Convex/Combination.lean,Mathlib/Analysis/Convex/Radon.lean,Mathlib/Analysis/InnerProductSpace/Projection.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Log/Base.lean,Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean,Mathlib/CategoryTheory/ComposableArrows.lean,Mathlib/CategoryTheory/Extensive.lean,Mathlib/CategoryTheory/Filtered/Basic.lean,Mathlib/CategoryTheory/Limits/VanKampen.lean,Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean,Mathlib/Computability/Ackermann.lean,Mathlib/Computability/DFA.lean,Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/Partrec.lean,Mathlib/Computability/PartrecCode.lean,Mathlib/Computability/PostTuringMachine.lean,Mathlib/Computability/Primrec.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Computability/TMConfig.lean,Mathlib/Computability/TMToPartrec.lean,Mathlib/Computability/Tape.lean,Mathlib/Control/LawfulFix.lean,Mathlib/Data/Complex/Exponential.lean,Mathlib/Data/Countable/Basic.lean,Mathlib/Data/DFinsupp/Defs.lean,Mathlib/Data/DFinsupp/WellFounded.lean,Mathlib/Data/Fin/Tuple/Basic.lean,Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean,Mathlib/Data/Finmap.lean,Mathlib/Data/Finset/Fold.lean,Mathlib/Data/Finset/Image.lean,Mathlib/Data/Finset/Lattice/Fold.lean,Mathlib/Data/Finset/Lattice/Lemmas.lean,Mathlib/Data/Finset/Lattice/Pi.lean,Mathlib/Data/Finset/Max.lean,Mathlib/Data/Finset/NAry.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Finset/Sym.lean,Mathlib/Data/Finsupp/BigOperators.lean,Mathlib/Data/Fintype/Basic.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/Data/Fintype/EquivFin.lean,Mathlib/Data/Fintype/Fin.lean	283	2	['github-actions', 'leanprover-community-bot-assistant']	nobody	4-5420 4 days ago	4-5422 4 days ago	10-65025 10 days
13795	FR-vdash-bot author:FR-vdash-bot	perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything	--- - [ ] depends on: #15192 - [ ] depends on: #15476 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	340/194	Mathlib/Algebra/Equiv/TransferInstance.lean,Mathlib/Algebra/Group/InjSurj.lean,Mathlib/Algebra/GroupWithZero/Action/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/End.lean,Mathlib/Algebra/GroupWithZero/InjSurj.lean,Mathlib/Algebra/Module/Defs.lean,Mathlib/Algebra/Module/RingHom.lean,Mathlib/Algebra/Ring/InjSurj.lean,scripts/noshake.json	9	35	['FR-vdash-bot', 'MichaelStollBayreuth', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mattrobball']	nobody	3-85961 3 days ago	3-85963 3 days ago	52-31623 52 days
15483	FR-vdash-bot author:FR-vdash-bot	chore(GroupTheory/Coset): reduce defeq abuse	--- - [x] depends on: #15482 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict label:t-algebra$	114/60	Mathlib/GroupTheory/Commensurable.lean,Mathlib/GroupTheory/Coset.lean,Mathlib/GroupTheory/QuotientGroup.lean,Mathlib/LinearAlgebra/Alternating/DomCoprod.lean,Mathlib/MeasureTheory/Measure/Haar/Quotient.lean,Mathlib/Topology/Algebra/Group/Compact.lean	6	14	['FR-vdash-bot', 'eric-wieser', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mattrobball', 'mergify', 'urkud']	nobody	3-38539 3 days ago	251-76869 8 months ago	4-79214 4 days
23621	FR-vdash-bot author:FR-vdash-bot	chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) - [x] depends on: #20676	t-order t-algebra merge-conflict label:t-algebra$	261/205	Archive/Imo/Imo1998Q2.lean,Counterexamples/LinearOrderWithPosMulPosEqZero.lean,Mathlib/Algebra/Order/Field/Canonical.lean,Mathlib/Algebra/Order/Field/Rat.lean,Mathlib/Algebra/Order/Floor/Ring.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Finset.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Order/Nonneg/Field.lean,Mathlib/Algebra/Order/Nonneg/Ring.lean,Mathlib/Algebra/Order/Ring/Nat.lean,Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean,Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean,Mathlib/Data/ENNReal/Basic.lean,Mathlib/Data/NNRat/Lemmas.lean,Mathlib/Data/NNReal/Defs.lean,Mathlib/Data/Rat/Cast/Order.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean,Mathlib/FieldTheory/RatFunc/AsPolynomial.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean,Mathlib/NumberTheory/EllipticDivisibilitySequence.lean,Mathlib/NumberTheory/FunctionField.lean,Mathlib/NumberTheory/Ostrowski.lean,Mathlib/RingTheory/Valuation/Archimedean.lean,Mathlib/RingTheory/Valuation/Basic.lean,Mathlib/RingTheory/Valuation/ExtendToLocalization.lean,Mathlib/RingTheory/Valuation/Integers.lean,Mathlib/RingTheory/Valuation/Integral.lean,Mathlib/RingTheory/Valuation/Minpoly.lean,Mathlib/RingTheory/Valuation/Quotient.lean,Mathlib/RingTheory/Valuation/RankOne.lean,Mathlib/RingTheory/Valuation/ValExtension.lean,Mathlib/RingTheory/Valuation/ValuationRing.lean,Mathlib/RingTheory/Valuation/ValuationSubring.lean,Mathlib/SetTheory/Cardinal/Order.lean,Mathlib/Topology/Algebra/Valued/LocallyCompact.lean,Mathlib/Topology/Algebra/Valued/NormedValued.lean,Mathlib/Topology/Algebra/Valued/ValuationTopology.lean,Mathlib/Topology/Algebra/Valued/ValuedField.lean,Mathlib/Topology/Algebra/Valued/WithVal.lean,Mathlib/Topology/Algebra/WithZeroTopology.lean,Mathlib/Topology/UnitInterval.lean,MathlibTest/instance_diamonds.lean,scripts/noshake.json	44	n/a	['FR-vdash-bot', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot']	nobody	2-31532 2 days ago	unknown	unknown
20567	grunweg author:grunweg	feat(Cache): two small features	- add an informational message to the get command (when run without arguments): when more than 80% of all cache files present were not used in the last command, tell the user about the `clean` command --- - [ ] depends on #20568 (for the first feature) - [ ] TODO: re-design this feature and the clean command: if there are N local copies of mathlib, cache should have a pointer to all of them - to avoid clearing all N-1 from inside the last local copy [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta merge-conflict	38/2	Cache/Main.lean	1	11	['Julian', 'arthurpaulino', 'fpvandoorn', 'github-actions', 'grunweg']	nobody	1-42642 1 day ago	1-42642 1 day ago	1-17369 1 day
22153	smmercuri author:smmercuri	feat: weak approximation theorems for infinite places of a number field	The number field $K$ is dense in $\prod_v (K, v)$ and in the infinite adele ring $\prod_v K_v$, where $v$ ranges over the infinite places, $(K, v)$ denotes $K$ equipped with the topology induced by $v$, and $K_v$ is the completion of $K$ at $v$. --- - [ ] depends on #22147 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import t-algebra t-analysis t-number-theory merge-conflict label:t-algebra$	576/2	Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Analysis/AbsoluteValue/Equivalence.lean,Mathlib/Analysis/Normed/Ring/WithAbs.lean,Mathlib/Data/Fin/Basic.lean,Mathlib/Data/Finset/Lattice/Fold.lean,Mathlib/Logic/Pairwise.lean,Mathlib/NumberTheory/NumberField/AdeleRing.lean,Mathlib/NumberTheory/NumberField/Embeddings.lean	8	1	['github-actions']	nobody	1-42462 1 day ago	1-42462 1 day ago	11-23591 11 days

PRs from a fork of mathlib

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
23772	SEU-Prime author:SEU-Prime	Create Amice.lean	i built amice equiv [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-number-theory WIP	283/0	Mathlib/NumberTheory/Padics/Amice.lean	1	2	['grunweg']	nobody	11-65987 11 days ago	11-65987 11 days ago	0-0 0 seconds
23937	unknown author:unknown	feat(Algebra): vanishing of induced hom between ext	unknown description	t-algebra t-category-theory blocked-by-other-PR WIP label:t-algebra$	-1/-1		-1	n/a	None	nobody	2-73715 2 days ago	unknown	unknown
23986	ShouxinZhang author:ShouxinZhang	feat(FieldTheory/RatFunc): add RatFunc.toFractionRingAlgEquiv	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	will-close-soon t-algebra label:t-algebra$	17/0	Mathlib/FieldTheory/RatFunc/Basic.lean	1	1	['joneugster']	nobody	1-38769 1 day ago	1-38769 1 day ago	0-0 0 seconds
3610	TimothyGu author:TimothyGu	feat: derive Infinite automatically for inductive types	Deals with recursive types, but not mutually recursive types or types with indices right now. See docstring for details. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta merge-conflict awaiting-author	517/0	Mathlib.lean,Mathlib/Tactic/DeriveInfinite.lean,test/DeriveInfinite.lean	3	11	['TimothyGu', 'digama0', 'eric-wieser', 'grunweg', 'kim-em', 'kmill']	kmill assignee:kmill	104-14399 3 months ago	104-14399 3 months ago	0-0 0 seconds

Stale new contributor PRs

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
15224	AnthonyBordg author:AnthonyBordg	feat(CategoryTheory/Sites): covering families and their associated Grothendieck topology	Define covering families on a category and their associated Grothendieck topology by using the API for `Coverage`. Give an explicit characterization of the covering sieves of the said topology. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-category-theory awaiting-author	112/0	Mathlib.lean,Mathlib/CategoryTheory/Sites/CoveringFamilies.lean	2	20	['AnthonyBordg', 'adamtopaz', 'dagurtomas', 'github-actions', 'joelriou']	nobody	256-62175 8 months ago	261-55840 8 months ago	1-48443 1 day
14563	awueth author:awueth	feat: if-then-else of exclusive or statement	--- If `¬(P ∧ Q)` then `ite (P ∨ Q) a 1 = (ite P a 1) * (ite Q a 1)` [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra awaiting-author label:t-algebra$	5/0	Mathlib/Algebra/Group/Basic.lean	1	3	['eric-wieser', 'github-actions', 'kim-em']	nobody	246-79551 8 months ago	246-79551 8 months ago	6-38745 6 days
11207	luigi-massacci author:luigi-massacci	feat(Topology/MetricSpace): Add new file with type of Katetov maps	add a type of Katetov maps (one point extensions of a metric) and related notation and FunLike coercions. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-topology WIP	138/0	Mathlib.lean,Mathlib/Topology/MetricSpace/Katetov.lean,docs/references.bib	3	16	['fpvandoorn', 'jcommelin', 'kim-em', 'luigi-massacci', 'urkud']	nobody	242-63928 7 months ago	344-66013 11 months ago	26-83567 26 days
11090	pangelinos author:pangelinos	feat: define spectral spaces and prove that a quasi-compact open of a spectral space is spectral	Define spectral spaces and prove that a quasi-compact open of a spectral space is spectral. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-topology please-adopt good first issue	69/0	Topology/Spectral/basic.lean	1	15	['YaelDillies', 'adomani', 'j-loreaux', 'jcommelin', 'kim-em', 'pangelinos']	nobody	242-63803 7 months ago	246-76729 8 months ago	16-44803 16 days
15121	Eloitor author:Eloitor	feat: iff theorems for IsSplitEpi and IsSplitMono in opposite category	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-category-theory awaiting-author	40/0	Mathlib/CategoryTheory/EpiMono.lean	1	3	['github-actions', 'joelriou', 'mattrobball']	nobody	229-39295 7 months ago	260-84954 8 months ago	7-3203 7 days
16773	arulandu author:arulandu	feat(Probability/Distributions): formalize Beta distribution	Formalize Beta distribution, using Gamma distribution as a reference. Added real-valued beta wrapper, in the manner of gamma. Thanks to @EtienneC30 for help with casting real <-> complex. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-measure-probability awaiting-author	286/1	Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Probability/Distributions/Beta.lean	3	48	['EtienneC30', 'arulandu', 'github-actions', 'vihdzp']	arulandu assignee:arulandu	210-85912 6 months ago	215-82630 7 months ago	1-21124 1 day
14237	js2357 author:js2357	feat: Define the localization of a fractional ideal at a prime ideal	Define the localization of a fractional ideal at a prime ideal, and prove some basic properties. --- This PR is part 3 out of 4 of a proof of `isDedekindDomain_iff_isDedekindDomainDvr`. Part 4 is available here: #14242 - [x] depends on: #14099 Part 1 - [x] depends on: #14216 Part 2 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra awaiting-author label:t-algebra$	230/0	Mathlib.lean,Mathlib/RingTheory/FractionalIdeal/LocalizedAtPrime.lean,Mathlib/RingTheory/Localization/Basic.lean	3	20	['Vierkantor', 'YaelDillies', 'github-actions', 'js2357', 'kbuzzard', 'leanprover-community-mathlib4-bot']	Vierkantor assignee:Vierkantor	206-64756 6 months ago	206-64874 6 months ago	26-39463 26 days
15651	TpmKranz author:TpmKranz	feat(Computability/NFA): operations for Thompson's construction	Lays the groundwork for a proof of equivalence of RE and NFA, w.r.t. described language. Actual connection to REs comes later, after the groundwork for the opposite direction has been laid. Third chunk of #12648 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-computability new-contributor awaiting-author	307/5	Mathlib/Computability/NFA.lean	1	13	['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions']	nobody	205-76365 6 months ago	206-63294 6 months ago	45-84611 45 days
14603	awueth author:awueth	feat: degree is invariant under graph isomorphism	--- Mathlib has the definition `SimpleGraph.Iso.mapNeighborSet` which is an equivalence between neighbor sets induced by an isomorphism. Would it be beneficial to add the same equivalence for `neighborFinset`? [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-combinatorics WIP	24/0	Mathlib/Combinatorics/SimpleGraph/Map/Finite.lean	1	11	['awueth', 'github-actions', 'jcommelin', 'kim-em', 'urkud']	nobody	178-58297 5 months ago	178-58297 5 months ago	31-44440 31 days
12799	jstoobysmith author:jstoobysmith	feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group	Add properties of the special unitary group, mirroring the properties of found in Algebra/Star/Unitary.lean. In particular, I add an instance of `specialUnitaryGroup` as a `Group`, `Star`, `InvolutiveStar`, and `StarMul`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra please-adopt awaiting-author label:t-algebra$	78/0	Mathlib/LinearAlgebra/UnitaryGroup.lean	1	7	['chrisflav', 'jcommelin']	nobody	170-63915 5 months ago	170-63915 5 months ago	9-22007 9 days
15809	archiebrowne author:archiebrowne	feat(RingTheory/MvPolynomial/Ideal): introduce new lemmas about MvPolynomial Ideals	Four new lemmas about MvPolynomialIdeals `sub_span_span_sub`, `span_eq_iff_basis_sub`, `mem_basis_mem_span`, `mem_span_exists_dvd_mem_basis`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra awaiting-author label:t-algebra$	38/0	Mathlib/RingTheory/MvPolynomial/Ideal.lean	1	6	['Ruben-VandeVelde', 'github-actions', 'riccardobrasca']	riccardobrasca assignee:riccardobrasca	151-61081 5 months ago	206-63001 6 months ago	41-7533 41 days
15649	TpmKranz author:TpmKranz	feat(Computability): introduce Generalised NFA as bridge to Regular Expression	Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid. Second chunk of #12648 --- - [x] depends on: #15647 [Data.FinEnum.Option unchanged since then] [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-computability new-contributor awaiting-author	298/0	Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib	5	5	['github-actions', 'mathlib4-dependent-issues-bot', 'trivial1711']	nobody	132-15677 4 months ago	132-15677 4 months ago	23-54870 23 days
20029	FrederickPu author:FrederickPu	Allow for Config attributes to be set directly	Allow for Config attributes to be set directly when using initialize_simp_projection as per issue #19895 Basically modified initialize_simp_projection so that the user has the option of specifying a tuple of config option values. Ex: ``` initialize_simp_projection MulEquiv (toFun → apply, invFun → symm_apply) (fullyApplied := false) ``` These config options are then converted into projections. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-meta WIP	34/4	Mathlib/Tactic/Simps/Basic.lean	1	10	['FrederickPu', 'YaelDillies', 'fpvandoorn', 'github-actions']	nobody	121-43139 4 months ago	121-78248 4 months ago	0-34081 9 hours
18461	hannahfechtner author:hannahfechtner	feat: left and right common multiples mixins	add mixins for left and right common multiples. These carry the data of what factors are used to create the common multiples --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra awaiting-author label:t-algebra$	78/0	Mathlib/Algebra/Group/Defs.lean	1	13	['github-actions', 'hannahfechtner', 'jcommelin', 'kbuzzard', 'kim-em', 'trivial1711']	nobody	88-82832 2 months ago	88-82832 2 months ago	69-35596 69 days
20797	vbeffara author:vbeffara	feat(Topology/Covering): CM version of eq_of_comp_eq	Add equivalents of the lemmas `IsCoveringMap.eq_of_comp_eq` and `IsCoveringMap.const_of_comp_CM` for the case of bundled `ContinuousMap` parameters. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-topology easy awaiting-author	9/1	Mathlib/Topology/Covering.lean	1	4	['github-actions', 'ocfnash', 'vbeffara']	nobody	88-69597 2 months ago	89-70550 2 months ago	2-77310 2 days
13685	niklasmohrin author:niklasmohrin	feat(Combinatorics): add definitions for network flows	Although we might not have any super-interesting results ready for mathlib yet, I feel that the definitions from this commit are already mature enough to include. These definitions are ported from last semester's work we did at https://github.com/niklasmohrin/lean-seminar-2023 and I have put some time in to refactor our code to `Int` and now to any parameter `R`. In the linked repository, there is some more stuff that I can send in. One obstacle without integer values is that it is not clear why a maximum flow would exist. I think the best way to tackle this would be to prove max-flow-min-cut theorem and implement the Ford-Fulkerson algorithm. It has been pointed out on Zulip that there is an [Isabelle formalization of the Edmonds Karp Algorithm](https://www.isa-afp.org/entries/EdmondsKarp_Maxflow.html). I feel that the definitions are pretty solid and it makes sense to include them, even if just for unifying definitions across downstream projects. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-combinatorics awaiting-author	244/0	Mathlib.lean,Mathlib/Combinatorics/Flow/Basic.lean,docs/references.bib	3	56	['Shreyas4991', 'YaelDillies', 'b-mehta', 'github-actions', 'madvorak', 'niklasmohrin']	nobody	67-4223 2 months ago	67-4223 2 months ago	86-21072 86 days
19582	yu-yama author:yu-yama	feat(GroupExtension/Abelian): define `OfMulDistribMulAction.equivH2`	Mainly defines: - `structure GroupExtension.OfMulDistribMulAction N G [MulDistribMulAction G N]`: group extensions of `G` by `N` where the multiplicative action of `G` on `N` is the conjugation - `structure GroupExtension.OfMulDistribMulActionWithSection N G [MulDistribMulAction G N]`: group extensions with specific choices of sections - `def GroupExtension.OfMulDistribMulAction.equivH2`: a bijection between the equivalence classes of group extensions and $H^2 (G, N)$ - [x] depends on: #20802 (split PR: contains changes to the `Defs` file) - [x] depends on: #20998 (split PR: mainly adds the `Basic` file) - [ ] depends on: #21837 (split PR: adds the first part of the `Abelian` file) --- Here is a relevant TODO in Mathlib: https://github.com/leanprover-community/mathlib4/blob/4e9fa40d7c480937e09cd6e47a591bd6f3b8be42/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean#L46-L48 I would appreciate your comments. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra blocked-by-other-PR label:t-algebra$	736/14	Mathlib.lean,Mathlib/GroupTheory/GroupExtension/Abelian.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,docs/references.bib	4	3	['erdOne', 'github-actions', 'mathlib4-dependent-issues-bot']	nobody	64-47538 2 months ago	64-51312 2 months ago	43-23183 43 days
20648	anthonyde author:anthonyde	feat: formalize regular expression -> εNFA	The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness. --- - [x] depends on: #20644 - [x] depends on: #20645 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-computability new-contributor	490/0	Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib	3	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	59-25373 2 months ago	59-25386 2 months ago	59-27181 59 days
13442	dignissimus author:dignissimus	feat: mabel tactic for multiplicative abelian groups	Mabel tactic for multiplicative abelian groups (#10361) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-meta modifies-tactic-syntax awaiting-author help-wanted	439/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/MAbel.lean,MathlibTest/mabel.lean	4	10	['BoltonBailey', 'dignissimus', 'github-actions', 'joneugster', 'kbuzzard']	joneugster assignee:joneugster	58-35360 1 month ago	63-16956 2 months ago	0-16 16 seconds
21501	sksgurdldi author:sksgurdldi	feat(List): add sum_zipWith_eq_finset_sum	### Description: This PR adds the lemma `List.sum_zipWith_eq_finset_sum` to `Mathlib.Algebra.BigOperators.Group.Finset.Basic`. #### Statement: The sum of the `zipWith` operation on two lists equals the sum of applying the operation to corresponding elements of the two lists, indexed over the minimum of their lengths. #### Formal Statement: ```lean lemma sum_zipWith_eq_finset_sum [Inhabited α] [Inhabited β] [AddCommMonoid γ] {op : α → β → γ} (l : List α) (m : List β) : (List.zipWith op l m).sum = ∑ x ∈ (Finset.range (Nat.min l.length m.length)), op (l[x]!) (m[x]!) ``` #### Remarks: - This lemma provides a useful equivalence between `List.zipWith` and summation over a `Finset.range` indexed by `Nat.min l.length m.length`. - It can be helpful in algebraic manipulations involving list-based summations. #### Dependencies: No additional dependencies. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra awaiting-author label:t-algebra$	43/0	Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean	1	1	['github-actions', 'j-loreaux']	nobody	58-34439 1 month ago	58-34439 1 month ago	13-33168 13 days
22302	CharredLee author:CharredLee	feat: add `CategoryTheory.Topos.Power`	This is a continuation of #21281 with the end goal of defining topoi in Mathlib. It introduces the notion of a power object in a category with a subobject classifier, which is a special case of an internal hom. The definition `HasPowerObjects C` contained in this PR is all that remains before `IsTopos C` can be defined. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-category-theory awaiting-author	312/0	Mathlib.lean,Mathlib/CategoryTheory/Topos/Power.lean	2	2	['github-actions', 'joelriou']	b-mehta assignee:b-mehta	52-35635 1 month ago	52-36762 1 month ago	0-1528 25 minutes
22314	shetzl author:shetzl	feat: add leftmost derivations for context-free grammars	Leftmost derivations are often easier to reason about than arbitrary derivations. This PR adds leftmost variants of Rewrites, Produces and Derives to the existing definition of context-free grammars and proves that a string of terminals can be derived iff it can be leftmost derived. Co-authored-by: Tobias Leichtfried --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-computability new-contributor	383/0	Mathlib.lean,Mathlib/Computability/LeftmostDerivation.lean	2	27	['github-actions', 'madvorak', 'shetzl']	nobody	51-62955 1 month ago	51-84224 1 month ago	51-84276 51 days
22390	YunkaiZhang233 author:YunkaiZhang233	feat(CategoryTheory): implemented proofs for factorisation categories being equivalent to iterated comma categories in two ways	Completed one of the tasks in TODOs, shown and implemented the details for `(X/C)/f ≌ Factorisation f ≌ f/(C/Y)`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-category-theory awaiting-author	112/1	Mathlib/CategoryTheory/Category/Factorisation.lean	1	9	['YunkaiZhang233', 'github-actions', 'joelriou']	nobody	46-76268 1 month ago	49-71740 1 month ago	0-6513 1 hour
8167	sebzim4500 author:sebzim4500	feat: Add new `grw` tactic for rewriting using inequalities.	feat: Add new `grw` tactic for rewriting using inequalities. Co-authored-by: @hrmacbeth, @digama0 --- - [x] depends on: #8796 ```lean example (x y z w : ℝ) (h₁ : x < z) (h₂ : w ≤ y + 4) (h₃ : Real.exp z < 5 * w) : Real.exp x < 5 * (y + 4) := by grw [h₁, ← h₂] exact h₃ ``` [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-meta modifies-tactic-syntax	552/2	Mathlib.lean,Mathlib/Data/Int/ModEq.lean,Mathlib/Tactic.lean,Mathlib/Tactic/GCongr/Core.lean,Mathlib/Tactic/GRW.lean,Mathlib/Tactic/GRW/Core.lean,Mathlib/Tactic/GRW/Lemmas.lean,MathlibTest/GRW.lean,scripts/noshake.json	9	53	['Vierkantor', 'digama0', 'eric-wieser', 'fpvandoorn', 'github-actions', 'hrmacbeth', 'kim-em', 'leanprover-community-mathlib4-bot', 'sebzim4500']	nobody	40-62139 1 month ago	41-49108 1 month ago	72-11359 72 days
22809	b-reinke author:b-reinke	feat: Category algebras and path algebras	This PR defines the category algebra of a linear category and path algebras of quivers. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor WIP	218/0	Mathlib/Algebra/Ring/Assoc.lean,Mathlib/CategoryTheory/Linear/CategoryAlgebra.lean,Mathlib/Combinatorics/Quiver/PathAlgebra.lean,Mathlib/Data/DFinsupp/BigOperators.lean	4	2	['b-reinke', 'github-actions']	nobody	38-79254 1 month ago	39-43493 1 month ago	0-0 0 seconds
22948	pelicanhere author:pelicanhere	feat(Algebra/DirectSum): morphism of directsum decomposition	Define morphism of directsum decomposition, which would be later used in defineing graded ring hom. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra label:t-algebra$	68/0	Mathlib/Algebra/DirectSum/Decomposition.lean	1	1	['github-actions']	nobody	34-69666 1 month ago	34-82310 1 month ago	34-82355 34 days
22196	xyzw12345 author:xyzw12345	feat: `lie_ring` tactic and `LieReduce` command	In this PR, we implement a new tactic that reduces expressions in a `LieRing` to a normal form and checks whether they are equal, and a command which reduces the expression and displays the normal form. The implementation of this tactic imitates the `ring` tactic, using the `Qq` package to implement a specific reduction algorithm, following the theory of Hall sets and Lyndon words. A reference for the algorithm can be found at, for example, [here](https://personal.math.ubc.ca/~cass/research/pdf/Free.pdf). This project is the result of a workshop at Peking University, and @siddhartha-gadgil has helped us a lot on understanding the concepts in metaprogramming. Edit: The changes are reverted to a point where only `AtomM` is used. Co-authored-by: @Thmoas-Guan <2300010733@stu.pku.edu.cn> @yhtq <2100012990@stu.pku.edu.cn> @Blackfeather007 <2100017455@stu.pku.edu.cn> --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-meta	821/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/LieAlgebra/Basic.lean,Mathlib/Tactic/LieAlgebra/LieRingNF.lean,Mathlib/Util/AtomM.lean,MathlibTest/lie_ring.lean,scripts/noshake.json	7	5	['github-actions', 'ocfnash', 'siddhartha-gadgil', 'xyzw12345']	nobody	34-63201 1 month ago	55-19585 1 month ago	55-19579 55 days
22159	shetzl author:shetzl	feat: add definition of pushdown automata	Add the definition of pushdown automata and their two acceptance conditions: acceptance based on empty stack and acceptance based on final state. Co-authored-by: Tobias Leichtfried --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-computability new-contributor awaiting-author	70/0	Mathlib.lean,Mathlib/Computability/PDA.lean	2	34	['YaelDillies', 'github-actions', 'madvorak', 'shetzl']	nobody	32-83182 1 month ago	32-83182 1 month ago	20-81771 20 days
20238	maemre author:maemre	feat(Computability/DFA): Closure of regular languages under some set operations	This shows that regular languages are closed under complement and intersection by constructing DFAs for them. --- Closure under all other operations will be proved when someone adds the proof for DFA<->regular expression equivalence, so they are not part of this PR. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-computability new-contributor awaiting-author	114/0	Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean	2	56	['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'urkud']	EtienneC30 assignee:EtienneC30	32-60488 1 month ago	32-60488 1 month ago	48-67492 48 days
18091	tukamilano author:tukamilano	feat: Hoeffding's lemma	Formalize Hoeffding's lemma using the property of cumulant. Co-authored-by: Yuma Mizuno [mizuno.y.aj@gmail.com](mailto:mizuno.y.aj@gmail.com) --- - [x] depends on: #20151	large-import new-contributor t-measure-probability awaiting-author	339/0	Mathlib.lean,Mathlib/Probability/Hoeffding.lean,Mathlib/Probability/Moments/Basic.lean,Mathlib/Probability/Moments/MGFAnalytic.lean,docs/references.bib	5	55	['RemyDegenne', 'YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'tukamilano', 'yuma-mizuno']	tukamilano assignee:tukamilano	29-74798 29 days ago	29-74806 29 days ago	1-58489 1 day
22069	Raph-DG author:Raph-DG	feat(LinearMap): Added lemmas relating kernels of linear maps to Submodule.map	Added the lemma ne_map_or_ne_kernel_inter_of_lt stating that if A < B as submodules, then for any linear map f, `ker f ⊓ A ≠ ker f ⊓ B ∨ Submodule.map f A ≠ Submodule.map f B`. We also prove the corollaries ker_inter_mono_of_map_eq and map_mono_of_ker_inter_eq. Co-authored-by: Raphael Douglas Giles (raphaeldouglasgiles@gmail.com) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra label:t-algebra$	28/0	Mathlib/LinearAlgebra/Span/Basic.lean	1	14	['Paul-Lez', 'Raph-DG', 'github-actions', 'j-loreaux']	nobody	24-62241 24 days ago	24-62258 24 days ago	58-47358 58 days
22884	tannerduve author:tannerduve	feat(Computability/TuringDegrees): define oracle computability and Turing degrees	### Description Define a model of oracle computability, introducing Turing reducibility (`≤ᵀ`), Turing equivalence (`≡ᵀ`), and Turing degrees as the quotient under Turing equivalence. - `RecursiveIn O f`: A function `f` is recursive in a set of oracles `O` if it can be computed using `O` via basic operations (zero, successor, pairing, composition, primitive recursion, and μ-recursion). - `TuringReducible`: The relation that `f` is recursive in `{g}`, i.e., `f ≤ᵀ g`. - `TuringEquivalent`: A relation defining Turing equivalence between partial functions. - `TuringDegree`: The set of equivalence classes under `TuringEquivalent`, forming a partially ordered structure. Additionally: - Prove that `TuringReducible` is a preorder (reflexive, transitive). - Show that `TuringEquivalent` is an equivalence relation. - Establish that partial recursive functions correspond to functions recursive in the empty oracle set. This formalization follows classical recursion theory (Odifreddi, Soare) and extends previous work by Carneiro. ### Breaking Changes None. ### Dependencies None.	t-computability new-contributor	221/0	Mathlib.lean,Mathlib/Computability/TuringDegrees.lean	2	8	['github-actions', 'tannerduve', 'tristan-f-r']	nobody	23-36384 23 days ago	37-52866 1 month ago	37-52912 37 days
22137	grunweg author:grunweg	feat: `IsEmbedding.sumElim_of_separatingNhds`	Characterise when the `Sum.elim` of two inducing maps resp. embeddings is an embedding, and deduce that the ranges of the two maps lying in separated neighbourhoods suffices. This will be used in my bordism theory project. ------------ - [x] depends on: #22827 (for breaking the import cycle) - [ ] depends on: #22969 - [ ] depends on: #22964 - [ ] depends on: #23371 (for the previous PR) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-topology awaiting-author blocked-by-other-PR	209/10	Mathlib/Data/Set/Image.lean,Mathlib/Data/Sum/Basic.lean,Mathlib/Order/Filter/Map.lean,Mathlib/Topology/Constructions/SumProd.lean	4	22	['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'plp127']	nobody	22-66169 22 days ago	22-66172 22 days ago	0-0 0 seconds
23349	BGuillemet author:BGuillemet	feat: add LocallyLipschitzOn.lipschitzOnWith_of_isCompact and two small lemmas about Lipschitz functions	Main feat (in Mathlib/Topology/EMetricSpace/Basic.lean): if a function `f` from an extended pseudometric space to a pseudometric space is locally Lipschitz on a compact subset `s`, then `f` is Lipschitz on `s`. The theorem is true only when the codomain of `f` is a pseudometric space, so it needs imports from Mathlib/Topology/MetricSpace. Other small feat (in Mathlib/Analysis/Calculus/ContDiff/RCLike.lean): a function that is continuously differentiable on an open subset is locally Lipschitz on this subset. --- - [ ] depends on: #22890 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import new-contributor t-topology blocked-by-other-PR	146/4	Mathlib/Analysis/Calculus/ContDiff/RCLike.lean,Mathlib/Topology/EMetricSpace/Basic.lean,Mathlib/Topology/EMetricSpace/Lipschitz.lean,Mathlib/Topology/UniformSpace/Compact.lean	4	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	22-52237 22 days ago	23-35255 23 days ago	0-0 0 seconds
22635	Kiolt author:Kiolt	feat: submonoid of pairs with quotient in a submonoid	This submonoid is part of the definition of toric ideals. From Toric --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	toric new-contributor t-algebra label:t-algebra$	36/0	Mathlib.lean,Mathlib/GroupTheory/MonoidLocalization/DivPairs.lean	2	10	['Paul-Lez', 'YaelDillies', 'erdOne', 'github-actions']	nobody	17-81322 17 days ago	17-81375 17 days ago	43-68307 43 days
22355	xyzw12345 author:xyzw12345	feat(Algebra/RingQuot): Some lemmas about `RingQuot.mkAlgHom` and `RingQuot.mkRingHom`	This PR provides a few basic lemmas about `RingQuot.mkRingHom` and `RingQuot.mkAlgHom`. These lemmas are about when are two elements mapped to the same one under these two maps, and they correspond to the lemma `Quot.eq`. PR #22279 depends on these lemmas. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra awaiting-author label:t-algebra$	16/0	Mathlib/Algebra/RingQuot.lean	1	13	['Paul-Lez', 'erdOne', 'eric-wieser', 'github-actions', 'ocfnash', 'xyzw12345']	nobody	17-10015 17 days ago	17-83738 17 days ago	32-33842 32 days
22279	xyzw12345 author:xyzw12345	feat(RingTheory/GradedAlgebra): homogeneous relation	In this PR, we defined the concept of a homogeneous relation and proved some properties about homogeneous relations. The main result of this PR is showing that taking `RingQuot` by a homogeneous relation can give a graded structure on the quotient ring. This result can be used to define graded structures on rings obtained using `RingQuot`, e.g. the Symmetric Algebra defined in #21539 can be verified to have such a structure. Co-authored-by: Zhixuan Dai @atstarrysky <22300180006@m.fudan.edu.cn> Yiming Fu @pelicanhere Zhenyan Fu @pumpkin678 Raphael Douglas Giles @Raph-DG Jiedong Jiang @jjdishere - [x] depends on: #22354 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra label:t-algebra$	455/0	Mathlib.lean,Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/DirectSum/Basic.lean,Mathlib/Algebra/DirectSum/Module.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/RingQuot.lean,Mathlib/RingTheory/GradedAlgebra/Basic.lean,Mathlib/RingTheory/GradedAlgebra/HomogeneousRelation.lean	8	6	['Paul-Lez', 'github-actions', 'mathlib4-dependent-issues-bot', 'ocfnash', 'xyzw12345']	nobody	17-9505 17 days ago	17-9508 17 days ago	18-41299 18 days
21985	FernandoChu author:FernandoChu	feat(CategoryTheory): the Grothendieck construction is prefibered	Adds a `isPreFibered` instance for the Grothendieck construction. Co-authored-by: Christian Merten --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-category-theory awaiting-author	55/0	Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean,Mathlib/CategoryTheory/Bicategory/Grothendieck.lean	2	14	['chrisflav', 'github-actions']	nobody	16-58625 16 days ago	16-58630 16 days ago	8-4256 8 days
22639	b-reinke author:b-reinke	feat(Mathlib/GroupTheory/FreeGroup): theory of (cyclically) reduced words	Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project. This PR defines in the new file `Mathlib/GroupTheory/FreeGroup/ReducedWords.lean` some extra lemmas for free groups, in particular about (cyclically) reduced words. ## Main declarations * `FreeGroup.Red.reduced`: the predicate for reduced words * `FreeGroup.Red.cyclicallyReduced`: the predicate for cyclically reduced words ## Main statements * `FreeGroup.infinite_order`: nontrivial elements of a free group have infinite order * `FreeGroup.zpow_left_injective`: taking n-th powers is an injective function on the free group Co-authored-by: Amir Livne Bar-on - [ ] depends on: #23366 - [ ] depends on: #23367 - [ ] depends on: #23368 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra blocked-by-other-PR label:t-algebra$	429/0	Mathlib.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/GroupTheory/FreeGroup/Reduce.lean,Mathlib/GroupTheory/FreeGroup/ReducedWords.lean	4	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	12-46443 12 days ago	22-77891 22 days ago	20-75471 20 days
20671	thefundamentaltheor3m author:thefundamentaltheor3m	feat(Analysis/Asymptotics/SpecificAsymptotics): Proving that 𝛔ₖ(n) = O(nᵏ⁺¹)	This PR proves a result about the $\sigma_k(n)$ arithmetic function, namely, that it is $O\left(n^{k+1}\right)$. Main theorem: `theorem sigma_asymptotic (k : ℕ) : (fun n ↦ (σ k n : ℝ)) =O[atTop] (fun n ↦ (n ^ (k + 1) : ℝ))` This result was proved as part of the sphere packing project. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import new-contributor t-number-theory awaiting-author	29/0	Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean	1	2	['b-mehta', 'github-actions']	b-mehta assignee:b-mehta	11-65698 11 days ago	21-60175 21 days ago	9-59130 9 days
21903	yhtq author:yhtq	feat: add from/toList between `FreeSemigroup` and `List` with relative theorems	Add from/toList between `FreeSemigroup` and `List` with relative theorems, as well as an incidental definition of lexicographic order on `FreeSemigroup`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import new-contributor t-algebra awaiting-CI label:t-algebra$	169/0	Mathlib/Algebra/Free.lean	1	11	['YaelDillies', 'github-actions']	nobody	11-12108 11 days ago	11-12108 11 days ago	51-9403 51 days
22657	Xmask19 author:Xmask19	feat: a graph is maximally acyclic iff it is a tree	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-combinatorics	86/0	Mathlib/Combinatorics/SimpleGraph/Acyclic.lean	1	6	['Rida-Hamadani', 'b-mehta', 'github-actions', 'grunweg']	b-mehta assignee:b-mehta	10-64165 10 days ago	10-64186 10 days ago	32-54866 32 days
22018	maddycrim author:maddycrim	feat(RingTheory/Localization/Pi): localization of a finite direct product where each semiring in product has maximal nilradical is a projection	For noncomputable def `surjectivePiNilradicalIsMaximal` : Let `M` be a submonoid of a direct product of commutative rings `R i`. If each `R i` has maximal nilradical then the direct product `∏ R i` surjects onto the localization of `∏ R i` at `M`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import new-contributor t-algebra label:t-algebra$	28/0	Mathlib/RingTheory/Localization/Pi.lean	1	24	['Paul-Lez', 'alreadydone', 'erdOne', 'github-actions', 'grunweg', 'jcommelin', 'maddycrim']	nobody	10-62011 10 days ago	12-57079 12 days ago	59-43907 59 days
23838	FordUniver author:FordUniver	feat(SimpleGraph): added completeGraph.adjDecidable	added completeGraph.adjDecidable --- Strangely `DecidableRel (completeGraph V).Adj` does not seem to be automatically inferred from `Top.adjDecidable` even though `⊤ : SimpleGraph V` is defined as `completeGraph V`. Am I missing something here or is it as simple as adding these two lines to mathlib?	new-contributor t-combinatorics	4/1	Mathlib/Combinatorics/SimpleGraph/Basic.lean	1	8	['FordUniver', 'YaelDillies', 'github-actions']	nobody	10-46476 10 days ago	10-57452 10 days ago	10-57506 10 days
21539	Raph-DG author:Raph-DG	feat(LinearAlgebra): Symmetric Algebra	Defined the universal property for the symmetric algebra of a module over a commutative ring, provided an explicit construction and proved that this satisfies the universal property. Also proved that the multivariate polynomial ring generated by a basis of a module satisfies the universal property of the symmetric algebra of that module. Co-authored-by: Zhixuan Dai <22300180006@m.fudan.edu.cn> Co-authored-by: Zhenyan Fu Co-authored-by: Yiming Fu Co-authored-by: Wang Jingting --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge new-contributor t-algebra label:t-algebra$	223/0	Mathlib.lean,Mathlib/Algebra/Symmetrized.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/MvPolynomial.lean	4	47	['ADedecker', 'Raph-DG', 'YaelDillies', 'eric-wieser', 'github-actions', 'xyzw12345']	nobody	10-28337 10 days ago	11-171 11 days ago	66-58166 66 days
23648	wwylele author:wwylele	feat(Topology/Order): add `Dense.exists_seq_strict{Mono/Anti}_tendsto`	Add `Dense.exists_seq_strict{Mono/Anti}_tendsto{'}` that restricts the sequence to a dense subset. This is useful for e.g. finding a monotone rational sequence approaching a real number. Co-authored-by: Jireh Loreaux --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-topology	62/0	Mathlib/Topology/Instances/Real/Lemmas.lean,Mathlib/Topology/Order/IsLUB.lean	2	10	['github-actions', 'j-loreaux', 'wwylele']	nobody	9-15699 9 days ago	13-48233 13 days ago	15-17795 15 days
22823	b-reinke author:b-reinke	feat(Algebra/Ring): associator of a non-associative ring	If `R` is a non-associative ring, then `(x * y) * z - x * (y * z)` is called the `associator` of ring elements `x y z : R`. The associator vanishes exactly when `R` is associative. We prove variants of this statement also for the `AddMonoidHom` bundled version of the associator, as well as the bundled version of `mulLeft₃` and `mulRight₃`, the multiplications `(x * y) * z` and `x * (y * z)`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import maintainer-merge new-contributor t-algebra label:t-algebra$	133/8	Mathlib.lean,Mathlib/Algebra/DirectSum/Ring.lean,Mathlib/Algebra/Ring/Associator.lean	3	46	['Paul-Lez', 'YaelDillies', 'b-reinke', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant']	nobody	8-74483 8 days ago	8-82020 8 days ago	32-56968 32 days
19796	peakpoint author:peakpoint	feat: Peano form of Taylor's theorem	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-analysis awaiting-author	329/19	Mathlib/Algebra/Polynomial/Module/Basic.lean,Mathlib/Analysis/Calculus/LHopital.lean,Mathlib/Analysis/Calculus/MeanValue.lean,Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Convex/Topology.lean,Mathlib/Analysis/Normed/Module/Convex.lean,Mathlib/Geometry/Manifold/Instances/Real.lean,Mathlib/Order/Interval/Set/Basic.lean,Mathlib/Topology/Algebra/Module/LocallyConvex.lean	9	13	['RemyDegenne', 'github-actions', 'peakpoint', 'sgouezel']	sgouezel assignee:sgouezel	8-72117 8 days ago	8-74988 8 days ago	33-36705 33 days
22790	mhk119 author:mhk119	feat: Extend `taylor_mean_remainder_lagrange` to `x < x_0`	The `taylor_mean_remainder_lagrange` theorem has the assumption that $x_0 < x$. In many applications, we need $x < x_0$ and one cannot use the current version to obtain this (see [zulip](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Taylor's.20theorem)). This PR introduces a set of theorems that push negations through Taylor expansions so that one can extend `taylor_mean_remainder_lagrange` to the case when $x < x_0$. These theorems should also be useful elsewhere since they are quite general.	new-contributor t-analysis awaiting-author	92/1	Mathlib/Analysis/Calculus/Deriv/Basic.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/Analysis/Calculus/Taylor.lean	3	10	['Paul-Lez', 'github-actions', 'grunweg']	nobody	8-71661 8 days ago	8-71661 8 days ago	30-77130 30 days
23718	syur2 author:syur2	feat(Algebra): hom localize equiv localize hom	Add the linear equiv of `S^{-1}(M =>[R] N)` equiv `(S^{-1} M) =>[S^{-1}R] (S^{-1} N)` for finitely presented module `M`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra label:t-algebra$	21/0	Mathlib/Algebra/Module/FinitePresentation.lean	1	1	['github-actions']	nobody	8-25399 8 days ago	13-4944 13 days ago	13-4942 13 days
22503	Kevew author:Kevew	chore(Nat): Nat factorization multiplicity	Ported lemmas from `Data/Nat/Multiplicity` to into a new file called `Data/Nat/Factorization/Multiplicity`, re-written in terms of `factorization`. Also, I'm new to this so is it fine to have a lemma copied over from another file? Like, I copied over @[simp] theorem Prime.factorization_self {p : ℕ} (hp : Prime p) : p.factorization p = 1 := by simp [hp] from Dat/Nat/Factorization/Basic. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import t-data new-contributor	269/15	Mathlib.lean,Mathlib/Data/Nat/Factorization/Basic.lean,Mathlib/Data/Nat/Factorization/Multiplicity.lean,Mathlib/Data/Nat/Multiplicity.lean	4	31	['Kevew', 'Paul-Lez', 'github-actions', 'grunweg']	Kevew assignee:Kevew	7-80983 7 days ago	36-28599 1 month ago	46-58948 46 days
23949	Louddy author:Louddy	feat: SkewPolynomial	# Univariate skew polynomials Skew polynomials are represented as `SkewMonoidAlgebra R (Multiplicative ℕ)`, where `R` is usually at least a Semiring. In this file, we define `SkewPolynomial` and provide basic instances. This is currently missing the definition of `coeff` and `single` as they require a more advance interface of `SkewMonoidAlgebra` which is still WIP (See TODOs in file). Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)> --- - [ ] depends on: #22078 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import new-contributor t-algebra blocked-by-other-PR label:t-algebra$	600/42	Mathlib.lean,Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean,Mathlib/Algebra/SkewPolynomial/Basic.lean,docs/references.bib	4	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	7-65115 7 days ago	7-65116 7 days ago	0-2389 39 minutes
23338	WilliamCoram author:WilliamCoram	feat: restricted power series form a ring	We define restricted powerseries over a normed ring R, and show they form a ring when R has the ultrametric property. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-number-theory	186/0	Mathlib.lean,Mathlib/RingTheory/PowerSeries/Restricted.lean	2	17	['Paul-Lez', 'WilliamCoram', 'github-actions', 'grunweg']	nobody	7-59022 7 days ago	23-68375 23 days ago	23-68499 23 days
22243	luigi-massacci author:luigi-massacci	feat(Topology/MetricSpace/Gluing): Inductive limits of separable spaces are separable	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-topology	23/0	Mathlib/Topology/MetricSpace/Gluing.lean	1	9	['Paul-Lez', 'github-actions', 'j-loreaux', 'luigi-massacci', 'mathlib-bors']	nobody	5-53085 5 days ago	11-59345 11 days ago	2-23272 2 days
22208	Thmoas-Guan author:Thmoas-Guan	feat(Algebra):filtered ring hom	In this PR, we define the filtered ring morphisms on rings and prove some basic properties of them. Co-authored by: Huanyu Zheng @Yu-Misaka Co-authored by: Yi Yuan @yuanyi-350 Co-authored by: Weichen Jiao @AlbertJ-314 --- - [ ] depends on: #20913 - [ ] depends on: #22632 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra blocked-by-other-PR label:t-algebra$	809/0	Mathlib.lean,Mathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean,Mathlib/RingTheory/FilteredAlgebra/FilteredHom.lean	3	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	3-83981 3 days ago	28-68823 28 days ago	0-267 4 minutes
11021	jstoobysmith author:jstoobysmith	feat(AlgebraicTopology) : add join of augmented SSets	This pull-request adds the definition of the join of augmented SSets defined as contravariant functors from `WithInitial SimplexCategory` to `Type u`. In addition it shows that the join of two standard augmented SSets is again an augmented SSets. From this the definition of the join of simplicial sets should follow easily. To aid the above theory, an api for `WithInitial SimplexCategory` has been created, with the notion of the `join` and `split` (forming a sort of inverse to join) of objects in this category are defined. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-category-theory merge-conflict WIP	2137/1	.gitignore,Mathlib.lean,Mathlib/AlgebraicTopology/Join.lean,Mathlib/AlgebraicTopology/SimplexCategory.lean,Mathlib/AlgebraicTopology/SimplexCategoryWithInitial.lean,Mathlib/AlgebraicTopology/SimplicialSet.lean	6	47	['github-actions', 'jcommelin']	nobody	262-761 8 months ago	317-82207 10 months ago	1-20125 1 day
12751	Command-Master author:Command-Master	feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size	Remove `@[simp]` from `Nat.bit_false` and `Nat.bit_true`, as `bit0` and `bit1` are deprecated, and add some lemmas to `Bits`, `Bitwise` and `Size`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data new-contributor merge-conflict	66/7	Mathlib/Data/Nat/Bits.lean,Mathlib/Data/Nat/Bitwise.lean,Mathlib/Data/Nat/Multiplicity.lean,Mathlib/Data/Nat/Size.lean	4	26	['Command-Master', 'Rida-Hamadani', 'Ruben-VandeVelde', 'YaelDillies', 'github-actions', 'jcommelin']	nobody	242-64460 7 months ago	247-80702 8 months ago	54-52408 54 days
9935	jstoobysmith author:jstoobysmith	feat(AlgebraicTopology): add constructors for horns	Added a function that given a simplicial set S and a set of n-1 simplexes satisfying certain conditions, creates a morphism in SSet from a n horn to a simplicial set S. Included also are a series of lemmas and definitions used in this construction. In particular I define a function that takes a m-simplex in a horn, and returns the smallest 'index' of face it factors through, and give a series of lemmas related to this. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra t-topology merge-conflict awaiting-author label:t-algebra$	462/2	Mathlib/AlgebraicTopology/SimplicialSet.lean	1	15	['YaelDillies', 'jcommelin', 'jstoobysmith', 'kim-em', 'linesthatinterlace']	nobody	242-64294 7 months ago	273-65619 8 months ago	14-58814 14 days
10006	jstoobysmith author:jstoobysmith	feat(AlgebraicTopology): homotopy in quasicategories	Defined a homotopy between two 1-simplicies in a quasicategories, and proved the property of being homotopic forms an equivalence relation. --- - [ ] depends on: #9935 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-category-theory merge-conflict awaiting-author blocked-by-other-PR	898/1	Mathlib.lean,Mathlib/AlgebraicTopology/Homotopy.lean,Mathlib/AlgebraicTopology/SimplexCategory.lean,Mathlib/AlgebraicTopology/SimplicialSet.lean	4	3	['joelriou', 'leanprover-community-mathlib4-bot']	nobody	207-3479 6 months ago	207-3479 6 months ago	0-0 0 seconds
14242	js2357 author:js2357	feat: Prove equivalence of `isDedekindDomain` and `isDedekindDomainDvr`	Prove that `isDedekindDomainDvr` is equivalent to both `isDedekindDomain` and `isDedekindDomainInv`. Specifically, prove `isDedekindDomainDvr A → isDedekindDomainInv A`, because `isDedekindDomain A → isDedekindDomainDvr A` and `IsDedekindDomain A ↔ IsDedekindDomainInv A` are already in Mathlib. - [x] depends on: #14099 - [x] depends on: #14216 - [ ] depends on: #14237 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra merge-conflict blocked-by-other-PR label:t-algebra$	269/1	Mathlib.lean,Mathlib/RingTheory/DedekindDomain/Dvr.lean,Mathlib/RingTheory/FractionalIdeal/LocalizedAtPrime.lean,Mathlib/RingTheory/Localization/Basic.lean	4	2	['github-actions', 'leanprover-community-mathlib4-bot']	nobody	206-50354 6 months ago	206-50354 6 months ago	0-0 0 seconds
16888	metinersin author:metinersin	feat(ModelTheory/Complexity): Define conjunctive and disjunctive normal forms	Define `FirstOrder.Language.BoundedFormula.IsDNF` and `FirstOrder.Language.BoundedFormula.IsCNF`. --- - [ ] depends on: #16887 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-logic merge-conflict blocked-by-other-PR	415/7	Mathlib/ModelTheory/Complexity.lean,Mathlib/ModelTheory/Equivalence.lean,Mathlib/ModelTheory/Syntax.lean	3	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	198-46332 6 months ago	198-46332 6 months ago	0-1045 17 minutes
16887	metinersin author:metinersin	feat(ModelTheory/Complexity): define conjunctive and disjunctive formulas	Defines `FirstOrder.Language.BoundedFormula.IsConjunctive` and `FirstOrder.Language.BoundedFormula.IsDisjunctive`. --- - [ ] depends on: #16885 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-logic merge-conflict blocked-by-other-PR	300/7	Mathlib/ModelTheory/Complexity.lean,Mathlib/ModelTheory/Equivalence.lean,Mathlib/ModelTheory/Syntax.lean	3	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	198-46332 6 months ago	198-46333 6 months ago	0-1299 21 minutes
16889	metinersin author:metinersin	feat(ModelTheory/Complexity): Normal forms	Defines `FirstOrder.Language.BoundedFormula.toDNF` and `FirstOrder.Language.BoundedFormula.toCNF` - given a quantifier-free formula, these construct a semantically equivalent formula in disjunctive normal form and conjunctive normal form, respectively. --- - [ ] depends on: #16888 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-logic merge-conflict blocked-by-other-PR	525/7	Mathlib/ModelTheory/Complexity.lean,Mathlib/ModelTheory/Equivalence.lean,Mathlib/ModelTheory/Syntax.lean	3	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	198-46331 6 months ago	198-46331 6 months ago	0-613 10 minutes
10190	jstoobysmith author:jstoobysmith	feat(AlgebraicTopology): add Augmented Simplex Category	- Added the definition of the category FinLinOrd of finite linear ordered sets. - Added the definition of the augmented simplex category `AugmentedSimplexCategory`, and showed it is the Skeleton of FinLinOrd. - Showed that the category of augmented simplicial objects defined as a comma category is equivalent to the category of functors from `AugmentedSimplexCategory^\op` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra t-topology t-category-theory merge-conflict WIP label:t-algebra$	720/0	Mathlib.lean,Mathlib/AlgebraicTopology/AugmentedSimplexCategory.lean,Mathlib/AlgebraicTopology/SimplicialObject.lean,Mathlib/Order/Category/FinLinOrd.lean	4	5	['TwoFX', 'YaelDillies', 'joelriou', 'jstoobysmith']	nobody	191-56530 6 months ago	191-56530 6 months ago	7-63215 7 days
12750	Command-Master author:Command-Master	feat: define Gray code	--- Define binary reflected gray code, both as a permutation of `Nat` and as a permutation of `BitVec n`, and prove some theorems about them. Additionally, remove `@[simp]` from `Nat.bit_false` and `Nat.bit_true`, as `bit0` and `bit1` are deprecated, and add some lemmas to `Bits`, `Bitwise` and `Size`. - [ ] depends on: #12751 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data new-contributor merge-conflict awaiting-author blocked-by-other-PR	226/0	Mathlib.lean,Mathlib/Data/Nat/Bits.lean,Mathlib/Data/Nat/Bitwise.lean,Mathlib/Data/Nat/GrayCode.lean,Mathlib/Data/Nat/Size.lean	5	5	['Rida-Hamadani', 'alreadydone', 'github-actions', 'grunweg', 'leanprover-community-mathlib4-bot']	nobody	180-68989 5 months ago	180-68989 5 months ago	6-8380 6 days
15654	TpmKranz author:TpmKranz	feat(Computability): language-preserving maps between NFA and RE	Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs Last chunk of #12648 --- - [ ] depends on: #15651 - [ ] depends on: #15649 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-computability new-contributor merge-conflict blocked-by-other-PR	985/2	Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib	7	2	['github-actions', 'leanprover-community-mathlib4-bot']	nobody	172-81091 5 months ago	172-81091 5 months ago	0-179 2 minutes
9605	davikrehalt author:davikrehalt	feat(Data/Finset & List): Add Lemmas for Sorting and Filtering	This PR includes several useful lemmas to the Data/Finset and Data/List modules in Lean's mathlib: 1. `toFinset_filter` (List): Shows that filtering commutes with toFinset. 2. `toFinset_is_singleton_implies_replicate` (List): Shows a list with a singleton toFinset is a List.replicate. 3. `filter_sort_commute` (Finset): Sorting and filtering can be interchanged in Finsets. 4. `Sorted.filter` (List): A sorted list stays sorted after filtering. 5. `Sorted.append_largest` (List): Appending the largest element keeps a list sorted. 6. `sort_monotone_map` (Finset): Relates sorting of a Finset after mapping to sorting of a list. 7. `sort_insert_largest` (Finset): Sorting a Finset with an inserted largest element. 8. `sort_range` (Finset): Sorting a range in a Finset equals the corresponding range list. 9. ~~`filter_eval_true` (List): Filtering a list with a predicate always true keeps the list unchanged.~~ 10. ~~`filter_eval_false` (List): Filtering with an always-false predicate gives an empty list.~~ 11. ~~`pairwise_concat` (List): Iff condition for Pairwise relation in concatenated lists (similar to pairwise_join).~~ 12. `list_map_toFinset` (Finset): toFinset commutes with map under injection --- - [x] depends on: #15952 This is my first PR to mathlib, so I'm not too familiar with etiquette's and more specifically there are two proofs in the PR which uses aesop, and I am not sure if it's frowned upon. I kept the aesop in there for now as I couldn't construct very short proofs otherwise. The sort_range function proof was suggested in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Computing.20Finset.20sort.20of.20Finset.20range/near/410346731 by Ruben Van de Velde. Thanks for your time for improving this PR.	t-data new-contributor merge-conflict please-adopt awaiting-author	71/0	Mathlib/Data/Finset/Basic.lean,Mathlib/Data/Finset/Image.lean,Mathlib/Data/Finset/Sort.lean,Mathlib/Data/List/Sort.lean	4	30	['YaelDillies', 'davikrehalt', 'eric-wieser', 'github-actions', 'jcommelin', 'leanprover-community-mathlib4-bot', 'urkud', 'vihdzp']	YaelDillies assignee:YaelDillies	170-40299 5 months ago	197-9090 6 months ago	12-48560 12 days
14598	Command-Master author:Command-Master	chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc.	Add the four typeclasses `IsTopAbsorbing`, `IsBotAbsorbing`, `NoTopSum`, `NoBotSum`, as additive equivalents for `MulZeroClass` and `NoZeroDivisors`. Add instances of these for `ENNReal`, `WithTop α`, `WithBot α`, `PUnit`, `EReal`, `PartENat`, `Measure`, `Interval` and `Filter`. Also split `Algebra/Order/AddGroupWithTop` to `Algebra/Order/Group/WithTop` and `Algebra/Order/Monoid/WithTop` --- Previous usages of lemmas with quantified names like `WithTop.add_top` have to be changed to just `add_top`. `add_lt_top` is `@[simp]`, in accordance with `ENNReal.add_lt_top` being `@[simp]`. This affects `WithTop.add_lt_top` which previously hadn't been `@[simp]`. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-order t-algebra merge-conflict label:t-algebra$	264/195	Archive/Wiedijk100Theorems/BallotProblem.lean,Mathlib.lean,Mathlib/Algebra/Order/Group/WithTop.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Interval/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean,Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/Algebra/Order/Monoid/WithTop.lean,Mathlib/Algebra/PUnitInstances/Order.lean,Mathlib/Algebra/Polynomial/Degree/Definitions.lean,Mathlib/Algebra/Polynomial/Monic.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Analysis/Analytic/Meromorphic.lean,Mathlib/Analysis/Normed/Lp/ProdLp.lean,Mathlib/Analysis/NormedSpace/ENorm.lean,Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean,Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean,Mathlib/Data/ENNReal/Operations.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/Nat/WithBot.lean,Mathlib/Data/Real/EReal.lean,Mathlib/LinearAlgebra/Lagrange.lean,Mathlib/MeasureTheory/Covering/Differentiation.lean,Mathlib/MeasureTheory/Decomposition/Lebesgue.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean,Mathlib/MeasureTheory/Function/Jacobian.lean,Mathlib/MeasureTheory/Function/L1Space.lean,Mathlib/MeasureTheory/Function/L2Space.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Function/LpSpace.lean,Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean,Mathlib/MeasureTheory/Function/UniformIntegrable.lean,Mathlib/MeasureTheory/Integral/Bochner.lean,Mathlib/MeasureTheory/Integral/MeanInequalities.lean,Mathlib/MeasureTheory/Integral/SetIntegral.lean,Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean,Mathlib/MeasureTheory/Measure/Hausdorff.lean,Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/MeasureTheory/Measure/MeasureSpace.lean,Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean,Mathlib/MeasureTheory/Measure/Regular.lean,Mathlib/MeasureTheory/Measure/Typeclasses.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/Order/Filter/Pointwise.lean,Mathlib/Probability/Kernel/Defs.lean,Mathlib/Probability/Martingale/Convergence.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/UniqueFactorizationDomain.lean,Mathlib/Topology/EMetricSpace/Defs.lean,Mathlib/Topology/MetricSpace/Bounded.lean,Mathlib/Topology/MetricSpace/HausdorffDistance.lean,Mathlib/Topology/MetricSpace/Lipschitz.lean	57	30	['Command-Master', 'YaelDillies', 'github-actions']	nobody	164-10865 5 months ago	164-10865 5 months ago	7-45599 7 days
16885	metinersin author:metinersin	feat(ModelTheory/Complexity): define literals	Defines `FirstOrder.Language.BoundedFormula.IsLiteral` and `FirstOrder.Language.BoundedFormula.simpleNot` - an auxiliary operation that takes the negation of a formula and does some simplification. --- - [x] depends on: #16800 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-logic merge-conflict awaiting-author	148/5	Mathlib/ModelTheory/Complexity.lean,Mathlib/ModelTheory/Equivalence.lean,Mathlib/ModelTheory/Semantics.lean,Mathlib/ModelTheory/Syntax.lean	4	20	['YaelDillies', 'awainverse', 'github-actions', 'mathlib4-dependent-issues-bot', 'metinersin']	nobody	161-53386 5 months ago	161-53386 5 months ago	0-19926 5 hours
13248	hcWang942 author:hcWang942	feat: basic concepts of auction theory	## Description Formalise some core concepts and results in auction theory: this includes definitions for first-price and second-price auctions, as well as several fundamental results and helping lemmas. This is the very first PR of the project formalizing core concepts and results in auction theory. Our group is working on more contributions on the formalization of game theory prefix. Co-authored-by: Ma Jiajun ## Reference Roughgarden, Tim. *Twenty Lectures on Algorithmic Game Theory*. Cambridge University Press, 2020. [Link](https://www.cambridge.org/core/books/twenty-lectures-on-algorithmic-game-theory/A9D9427C8F43E7DAEF8C702755B6D72B) --- - [x] Will depend on #14163 once that PR is merged. The Fintype lemmas introduced by this PR have been added in that PR and will be removed from here once that PR gets merged ## Current plan for formalization of Game Theory The current plan for the formalizing of Game Theory include: #### 1. Auction Theory. 🎉 _(200+ lines, this PR)_ - Essential definitions of Sealed-bid auction, First-price auction and Second-price auction. - First-price auction has no dominant strategy. - Second-price auction has dominant strategy. (Second-price auction is DSIC) #### 2. Mechanism design & Myerson's Lemma. 🎉 (400+ lines, pending for modification to Mathlib Standard) - Mechanism design An allocation rule is implementable if there exists - Dominant Strategy Incentive Compatible (DSIC) payment rule - An allocation rule is monotone if for every bidder’s gain is nondecreasing w.r.t. her/his bid - Myerson's Lemma Implementable ⇔ Monotone In the above case, the DSIC payment rule is unique. #### 3. von Neumann‘s Minimax Theorem. 🎉 (800+ lines, pending for modification to Mathlib Standard) - Equilibrium in zero sum game - Formalization strategy: via Loomis’s theorem. #### 4. Nash Equilibrium. 🎉 (pending for modification to Mathlib Standard) #### 5. Brouwer fixed-point theorem. (Work in Progress) #### 6. More Mechanism design. (Planning)	new-contributor t-logic merge-conflict awaiting-author	204/0	Mathlib.lean,Mathlib/GameTheory/Auction/Basic.lean,docs/references.bib	3	148	['Shreyas4991', 'YaelDillies', 'eric-wieser', 'faenuccio', 'github-actions', 'grunweg', 'hcWang942', 'tb65536', 'urkud', 'vihdzp']	hcWang942 assignee:hcWang942	157-5818 5 months ago	unknown	unknown
16116	jjdishere author:jjdishere	feat(Field): add theorems in Stacks Project Chapter 09FA Fields	Add theorems in Stacks Project Chapter 09FA Fields that are not in mathlib. Co-authored-by: --- - [x] depends on: #16105 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra merge-conflict WIP label:t-algebra$	6/2	Mathlib/Algebra/Field/Defs.lean,Mathlib/Algebra/Field/Subfield.lean	2	6	['github-actions', 'mathlib4-dependent-issues-bot', 'mergify']	nobody	155-53812 5 months ago	157-36220 5 months ago	0-0 0 seconds
16743	agjftucker author:agjftucker	feat(Analysis/Calculus/Implicit): define HasStrictDerivAt.implicitFunOfBivariate	In [this](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Implicit.20function.20theorem.20in.20familiar.20form) Zulip thread @Komyyy proved the "familiar" implicit function theorem. Then I wrote a proposal for a Mathlib PR. (Updated) it went: 1. `noncomputable def implicitFunOfBivariate {f : X × Y → Z} {p₀ : X × Y} {fx : X →L[𝕜] Z} {fy : Y ≃L[𝕜] Z} (hf₀ : HasStrictFDerivAt f (fx.coprod fy) p₀) : X → Y := ...` 2. `noncomputable def implicitFunOfBivariate' {f : X → Y → Z} {x₀ : X} {y₀ : Y} {fx : X →L[𝕜] Z} {fy : Y ≃L[𝕜] Z} (hfx : ContDiffAt 𝕜 1 (f · y₀) x₀) (hfy : ContDiffAt 𝕜 1 (f x₀ ·) y₀) (hfx₀ : fderiv 𝕜 (f · y₀) x₀ = fx) (hfy₀ : fderiv 𝕜 (f x₀ ·) y₀ = fy) : X → Y := ...` 3. `theorem image_eq_iff_implicitFunOfBivariate {f : X × Y → Z} {p₀ : X × Y} {fx : X →L[𝕜] Z} {fy : Y ≃L[𝕜] Z} (hf₀ : HasStrictFDerivAt f (fx.coprod fy) p₀) : ∀ᶠ p in 𝓝 p₀, f p = f p₀ ↔ hf₀.implicitFunOfBivariate p.1 = p.2 := ...` 4. `theorem implicitFunOfBivariate_hasStrictFDerivAt {f : X × Y → Z} {x₀ : X} {y₀ : Y} {fx : X →L[𝕜] Z} {fy : Y ≃L[𝕜] Z} (hf₀ : HasStrictFDerivAt f (fx.coprod fy) (x₀, y₀)) : HasStrictFDerivAt hf₀.implicitFunOfBivariate (-fy.symm ∘L fx) x₀ := ...` 5. something on the second derivative (or higher). Although my proposal elicited no response, I am making this micro-PR to address points 1, 3 and 4 since some limited enthusiasm had been shown earlier in that thread (admittedly for another proposal made by another person). I am testing the waters; if this PR gets anywhere I may continue to work on points 2 and 5. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-analysis merge-conflict awaiting-author	132/8	Mathlib/Analysis/Calculus/Implicit.lean,Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean,Mathlib/LinearAlgebra/Span.lean,Mathlib/Order/Filter/Prod.lean	4	4	['github-actions', 'sgouezel']	sgouezel assignee:sgouezel	144-82860 4 months ago	144-82860 4 months ago	63-71154 63 days
18646	jxjwan author:jxjwan	feat(RingTheory): isotypic components	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra merge-conflict label:t-algebra$	308/0	Mathlib/Order/CompactlyGenerated/Basic.lean,Mathlib/RingTheory/Isotypic.lean,Mathlib/RingTheory/SimpleModule.lean	3	1	['github-actions']	nobody	144-75390 4 months ago	144-75390 4 months ago	20-16585 20 days
19299	javierlcontreras author:javierlcontreras	feat(Algebra/CategoryTheory): Add CommAlgebraCat	--- - [x] depends on: #19065 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra merge-conflict WIP label:t-algebra$	26/1	Mathlib/Algebra/Algebra/Defs.lean,Mathlib/Algebra/Category/AlgebraCat/Basic.lean	2	4	['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot']	nobody	144-61395 4 months ago	144-77567 4 months ago	0-2116 35 minutes
19526	metakunt author:metakunt	feat:closure properties of numbers that are introspective to polynomials	Prove Part 1 of Claim 1.(i) of Theorem 6.1 in https://www3.nd.edu/~andyp/notes/AKS.pdf. ---- Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Aks.20primality.20Theorem.206.2E1.20Claim.20.28i.29.20proven	new-contributor t-number-theory merge-conflict awaiting-author	57/0	Mathlib.lean,Mathlib/NumberTheory/AKSPrimality.lean	2	10	['Ruben-VandeVelde', 'github-actions', 'jcommelin', 'kim-em', 'metakunt']	nobody	138-76723 4 months ago	138-76723 4 months ago	0-16072 4 hours
16344	robertmaxton42 author:robertmaxton42	feat(LinearAlgebra/FreeProduct): add induction principle, further simp opts for lift	Add an induction principle for proving properties about a `FreeProduct`. Replaces a number of `simp` and `aesop` calls in `lift` with `simp_rw` scripts to reduce compilation time (thanks Kevin!). - [ ] depends on: #15686 --- In a couple of places, I have used `simp↓` attributes when the linter tells me that a `simp` lemma is not in simp-normal form, instead of changing the LHS as the linter recommends. I claim that this is a legitimate use to tag important foundational lemmas that should be kept in a convenient human-readable form, but also contain nontrivial components that `simp` cannot already handle completely. Please tell me your thoughts. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra merge-conflict blocked-by-other-PR label:t-algebra$	240/17	Mathlib/LinearAlgebra/FreeProduct/Basic.lean	1	2	['github-actions', 'leanprover-community-mathlib4-bot']	nobody	131-60239 4 months ago	131-60239 4 months ago	0-479 7 minutes
19125	yhtq author:yhtq	feat: add theorems to transfer `IsGalois` between pairs of fraction rings	feat: add theorems to transfer `IsGalois` between pairs of fraction rings. - [x] depends on: #18404 - [x] depends on: #19124 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra merge-conflict label:t-algebra$	121/0	Mathlib.lean,Mathlib/FieldTheory/Galois/IsFractionRing.lean,Mathlib/RingTheory/Localization/FractionRing.lean	3	3	['github-actions', 'mathlib4-dependent-issues-bot', 'tb65536']	nobody	127-28235 4 months ago	133-63658 4 months ago	0-4534 1 hour
11156	smorel394 author:smorel394	feat(LinearAlgebra/{TensorProductBasis,Dual}): basis and dual of `PiTensorProduct`	Construct a basis of a `PiTensorProduct` of modules given bases of the modules, and relationship between the dual of a `PiTensorProduct` and the `PiTensorProduct` of the duals. Main results: * `Basis.piTensorProduct` (in `LinearAlgebra/TensorProductBasis.lean`): Let `ι` be a `Fintype` and `M` be a family of modules indexed by `ι`. If `b i : κ i → M i` is a basis for every `i` in `ι`, then `fun (p : Π i, κ i) ↦ ⨂ₜ[R] i, b i (p i)` is a basis of `⨂[R] i, M i`. * `PiTensorProduct.dualDistrib` (in `LinearAlgebra/Dual.lean`): The canonical linear map from `⨂[R] i, Dual R (M i)` to `Dual R (⨂[R] i, M i)`, sending `⨂ₜ[R] i, f i` to the composition of `PiTensorProduct.map f` with the linear equivalence `⨂[R] i, R →ₗ R` given by multiplication. * `PiTensorProduct.dualDistribEquiv` (also in `LinearAlgebra/Dual.lean`): A linear equivalence between `⨂[R] i, Dual R (M i)` and `Dual R (⨂[R] i, M i)` when all `M i` are finite free modules. If `f : (i : ι) → Dual R (M i)`, then this equivalence sends `⨂ₜ[R] i, f i` to the composition of `PiTensorProduct.map f` with the natural isomorphism `⨂[R] i, R ≃ R` given by multiplication. - [ ] depends on: #11155 (currently used as the base branch; do not merge without switching it back to `master`!) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import new-contributor t-algebra merge-conflict please-adopt blocked-by-other-PR label:t-algebra$	166/2	Mathlib/LinearAlgebra/DirectSum/Finsupp.lean,Mathlib/LinearAlgebra/Dual.lean,Mathlib/LinearAlgebra/TensorProduct/Basis.lean	3	4	['eric-wieser', 'github-actions', 'leanprover-community-mathlib4-bot']	nobody	109-67066 3 months ago	154-82694 5 months ago	0-0 0 seconds
17739	Aaron1011 author:Aaron1011	feat(Topology/Order/DenselyOrdered): prove Not (IsOpen) for intervals	Prove that Iic/Ici/Ioc/Ico/Icc intervals are not open in densely ordered topologies with no min/max element --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-topology merge-conflict awaiting-author	27/0	Mathlib/Topology/Order/DenselyOrdered.lean	1	8	['github-actions', 'vihdzp']	nobody	93-50247 3 months ago	93-50247 3 months ago	0-4704 1 hour
15720	znssong author:znssong	feat(SimpleGraph): The Bondy-Chvátal theorem	The proof of the Bondy-Chvátal theorem, with Dirac's theorem and Ore's theorem as its corollary. - [x] depends on: #15536 - [ ] depends on: #15711 - [ ] depends on: #15578	new-contributor t-combinatorics merge-conflict blocked-by-other-PR	903/3	Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/BondyChvatal.lean,Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean,Mathlib/Combinatorics/SimpleGraph/Path.lean,Mathlib/Combinatorics/SimpleGraph/Walk.lean,Mathlib/Dynamics/FixedPoints/Basic.lean,Mathlib/Dynamics/FixedPoints/Increasing.lean	8	3	['github-actions', 'grunweg', 'leanprover-community-mathlib4-bot']	YaelDillies assignee:YaelDillies	92-69333 3 months ago	92-69333 3 months ago	0-1791 29 minutes
15711	znssong author:znssong	feat(Combinatorics/SimpleGraph): Some lemmas about walk, cycle and Hamiltonian cycle	--- These lemmas are separated from the `meow-sister/BondyChvatal` branch and will be needed for the proof of the Bondy-Chvátal theorem. - [x] depends on: #15536 - [x] depends on: #16294	new-contributor t-combinatorics merge-conflict awaiting-author	407/3	Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean,Mathlib/Combinatorics/SimpleGraph/Path.lean,Mathlib/Combinatorics/SimpleGraph/Walk.lean	4	22	['Rida-Hamadani', 'YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'znssong']	nobody	92-69333 3 months ago	92-69333 3 months ago	9-13962 9 days
18629	tomaz1502 author:tomaz1502	feat(Computability.Timed): Formalization of runtime complexity of List.merge	This PR adds the formalization of the runtime complexity of the merge function, defined in `Data/List/Sort`. Requires: https://github.com/leanprover-community/mathlib4/pull/15450 References: - Previous PR on mathlib3: https://github.com/leanprover-community/mathlib3/pull/14494/ - First discussion on Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/BSc.20Final.20Project/near/220647062 - Second disussion on Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Formalization.20of.20Runtime.20Complexity.20of.20Sorting.20Algorithms/near/284184450 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-computability new-contributor merge-conflict awaiting-author	186/0	Mathlib.lean,Mathlib/Computability/Timed/InsertionSort.lean,Mathlib/Computability/Timed/Merge.lean	3	2	['github-actions', 'trivial1711']	nobody	92-35252 3 months ago	92-35252 3 months ago	33-11262 33 days
19291	PieterCuijpers author:PieterCuijpers	feat(Algebra/Order/Hom): add quantale homomorphism	Definition of quantale homomorphisms as functions that are both semigroup homomorphisms and complete lattice homomorphisms. --- - [x] depends on: #19810 - [x] depends on: #19811 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra merge-conflict awaiting-author label:t-algebra$	209/0	Mathlib.lean,Mathlib/Algebra/Order/Hom/Quantale.lean,scripts/noshake.json	3	29	['PieterCuijpers', 'YaelDillies', 'github-actions', 'kim-em', 'mathlib4-dependent-issues-bot']	nobody	87-56911 2 months ago	87-56912 2 months ago	36-2255 36 days
20372	jvlmdr author:jvlmdr	feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L)	Introduce ContinuousLinearMap.bilinearCompLp and bilinearCompLpL. Generalize eLpNorm_le_eLpNorm_mul_eLpNorm theorems to include constant C in bound condition. --- Expect this may be useful for defining tempered distributions from functions in `L^p`. The definitions more or less follow `ContinuousLinearMap.compLp...`. Names are loosely analogous to `ContinuousLinearMap.bilinearComp` and `SchwartzMap.bilinLeftCLM`. Note: I preferred the spelling `hpqr : p⁻¹ + q⁻¹ = r⁻¹` with `f` in `L^p` and `g` in `L^q` to `hpqr : 1 / p = 1 / q + 1 / r`. It's easier to obtain from `ENNReal.IsConjExponent` too. A few questions: - [ ] I defined `bilinear{Left,Right}LpL` in addition to `bilinearCompLpL` because `LinearMap.mkContinuous₂` is marked as `noncomputable` and `LinearMap.mkContinuous` is not. Is this worth the extra definitions? (Note: This is not visible in the source due to `noncomputable section`.) - [ ] Should I use `C : ℝ` instead of `C : NNReal` for `eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm'`? - [ ] Is it going to be painful to have `[Fact (1 ≤ p)] [Fact (1 ≤ q)] [Fact (1 ≤ r)]`? I don't think there's a way to avoid it though. Maybe providing specialized versions for `p.IsConjExponent q` with `L^1`? Naming: - [ ] Is it satisfactory to add a `'` to the `eLpNorm_le_eLpNorm_mul_eLpNorm ` definitions in `CompareExp.lean` where `≤ ‖f x‖ * ‖g x‖` has been replaced with `≤ C * ‖f x‖ * ‖g x‖`? These could replace the existing theorems, although I don't want to break backwards compatibility. There are 5 instances: `eLpNorm_le_eLpNorm_top_mul_eLpNorm'`, `eLpNorm_le_eLpNorm_mul_eLpNorm_top'`, `eLpNorm'_le_eLpNorm'_mul_eLpNorm''`, `eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm'`, `eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm'` (I'm not sure why the existing theorem `eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm` has an internal `'`) - [ ] Is `bilinearLeftLpL` a suitable name? Other options: `bilinearCompLpLeftL`, `bilinearCompLeftLpL`, `bilinLeftLpL` (analogous to `SchwartzMap.bilinLeftCLM`) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-measure-probability merge-conflict	203/40	Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSpace.lean	2	1	['github-actions']	nobody	80-74259 2 months ago	80-74259 2 months ago	27-43617 27 days
17176	arulandu author:arulandu	feat: integrals and integrability with .re	Lemmas for swapping order of .re and integration/integrability. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-measure-probability merge-conflict awaiting-author	49/0	Mathlib/MeasureTheory/Function/L1Space.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral.lean,Mathlib/MeasureTheory/Integral/SetIntegral.lean	4	30	['EtienneC30', 'arulandu', 'github-actions', 'loefflerd']	nobody	79-48692 2 months ago	79-48692 2 months ago	9-73631 9 days
14799	luigi-massacci author:luigi-massacci	feat(Analysis/MeanInequalities): Weighted QM-AM inequality	The inequality between the quadratic and arithmetic mean as a consequence of Jensen's inequality. Weighted version for positive real valued functions from a `Finset`. Fix notation for sums, switching to `∈` in place of `in`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-analysis easy merge-conflict awaiting-author	26/3	Mathlib/Analysis/MeanInequalities.lean	1	8	['YaelDillies', 'acmepjz', 'github-actions', 'luigi-massacci', 'vihdzp']	nobody	78-41863 2 months ago	78-41863 2 months ago	0-38862 10 hours
20248	peabrainiac author:peabrainiac	feat(Topology/Compactness): first-countable locally path-connected spaces are delta-generated	Shows that all first-countable locally path-connected spaces are delta-generated (so in particular all normed spaces and convex subsets thereof are), and that delta-generated spaces are equivalently generated by the unit interval or standard simplices. --- - [ ] depends on: #21616 In principle, this should be close to all that's required to show that all simplicial complexes and CW-complexes are delta-generated; I just haven't done it yet because I'm not sure which file to best do it in. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import new-contributor t-topology merge-conflict awaiting-author blocked-by-other-PR	1189/813	Mathlib.lean,Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/Topology/Algebra/Module/LocallyConvex.lean,Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean,Mathlib/Topology/Connected/LocPathConnected.lean,Mathlib/Topology/Connected/PathConnected.lean,Mathlib/Topology/ContinuousOn.lean,Mathlib/Topology/Homotopy/HSpaces.lean,Mathlib/Topology/Path.lean	9	22	['YaelDillies', 'github-actions', 'kbuzzard', 'mathlib4-dependent-issues-bot', 'peabrainiac']	nobody	68-31569 2 months ago	68-31569 2 months ago	39-21495 39 days
20334	miguelmarco author:miguelmarco	feat: allow polyrith to use a local Singular/Sage install	Try to call a local install of Singular (either standalone or inside Sage) to find the witness for polyrith before trying to call the online sage cell server. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-meta merge-conflict awaiting-author	171/48	Mathlib/Tactic/Polyrith.lean,scripts/polyrith_sage.py	2	13	['eric-wieser', 'github-actions', 'hanwenzhu', 'kim-em', 'miguelmarco']	nobody	63-82646 2 months ago	63-82646 2 months ago	27-65384 27 days
19943	AlexLoitzl author:AlexLoitzl	feat(Computability): Add Chomsky Normal Form Grammar and translation	- Define Chomsky normal form grammars - Add language-preserving translation between context-free grammars and Chomsky normal form grammars Co-authored-by: Martin Dvorak martin.dvorak@matfyz.cz --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-computability new-contributor merge-conflict awaiting-author	3151/0	Mathlib.lean,Mathlib/Computability/ChomskyNormalForm/Basic.lean,Mathlib/Computability/ChomskyNormalForm/EmptyElimination.lean,Mathlib/Computability/ChomskyNormalForm/LengthRestriction.lean,Mathlib/Computability/ChomskyNormalForm/TerminalRestriction.lean,Mathlib/Computability/ChomskyNormalForm/Translation.lean,Mathlib/Computability/ChomskyNormalForm/UnitElimination.lean,Mathlib/Computability/ContextFreeGrammar.lean	8	59	['AlexLoitzl', 'YaelDillies', 'github-actions', 'kim-em', 'madvorak']	nobody	63-65668 2 months ago	63-65668 2 months ago	37-29014 37 days
10541	Louddy author:Louddy	feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra	# Skew Monoid algebras This file presents a skewed version of `Mathlib.Algebra.MonoidAlgebra.Basic`. ## Definition We define `SkewMonoidAlgebra k G := G →₀ k` attached with a skewed convolution product. Here, the product of two elements `f g : SkewMonoidAlgebra k G` is the finitely supported function whose value at `a` is the sum of `f x * (x • g y)` over all pairs `x, y` such that `x * y = a`. This will be used in a later PR to define skew polynomial rings. Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)> --- - [x] depends on: #15878 - [x] depends on: #19084 - [ ] depends on: #22078 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra merge-conflict blocked-by-other-PR WIP label:t-algebra$	1624/0	Mathlib.lean,Mathlib/Algebra/Group/InjSurj.lean,Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean,Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean	4	105	['AntoineChambert-Loir', 'Louddy', 'YaelDillies', 'eric-wieser', 'fpvandoorn', 'github-actions', 'mariainesdff', 'mathlib4-dependent-issues-bot', 'mattrobball']	AntoineChambert-Loir assignee:AntoineChambert-Loir	58-69294 1 month ago	58-69295 1 month ago	179-12934 179 days
21269	CharredLee author:CharredLee	(WIP) feat (CategoryTheory/Topos): Add topos theory content	This code contains basic definitions and results in topos theory, including the definition of a subobject classifier, power objects, and topoi. It is proved that every topos has exponential objects, i.e. "internal homs". The mathematical content follows chapter IV sections 1-2 of Mac Lane and Moerdijk's text "Sheaves in Geometry and Logic". --- - [x] depends on: #21281 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-category-theory merge-conflict awaiting-author WIP	1269/0	Mathlib.lean,Mathlib/CategoryTheory/Topos/Basic.lean,Mathlib/CategoryTheory/Topos/Classifier.lean,Mathlib/CategoryTheory/Topos/Exponentials.lean,Mathlib/CategoryTheory/Topos/Power.lean	5	10	['CharredLee', 'gio256', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot']	nobody	53-31940 1 month ago	53-31940 1 month ago	0-13879 3 hours
22245	Champitoad author:Champitoad	feat(CategoryTheory/Subobject): add formalization of subobject classifier	This introduces a file `Classifier.lean` defining the notion `Classifier C` of subobject classifier in any category `C` with a terminal object, following Section I.3 of "Sheaves in Geometry and Logic" [MM92]. This is related to but independent from #21281, because our definition associates a characteristic map to every _subobject_ rather than every _monomorphism_. Adopting this "extensional" rather than "intensional" definition allows us to formalize the proof of Proposition 1 in [MM92, Section I.3] (`hasClassifier_isRepresentable_iff`), that `C` has a subobject classifier if and only if the subobjects presheaf `sub C` is representable. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-category-theory merge-conflict awaiting-author	5219/2536	Cache/Hashing.lean,Cache/IO.lean,Cache/Lean.lean,Mathlib.lean,Mathlib/Algebra/Algebra/Defs.lean,Mathlib/Algebra/Category/AlgebraCat/Limits.lean,Mathlib/Algebra/Category/BoolRing.lean,Mathlib/Algebra/Category/FGModuleCat/Basic.lean,Mathlib/Algebra/Category/Grp/AB.lean,Mathlib/Algebra/Category/Grp/EpiMono.lean,Mathlib/Algebra/Category/HopfAlgebraCat/Monoidal.lean,Mathlib/Algebra/Category/ModuleCat/Abelian.lean,Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean,Mathlib/Algebra/Category/ModuleCat/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Biproducts.lean,Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean,Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean,Mathlib/Algebra/Category/ModuleCat/EpiMono.lean,Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean,Mathlib/Algebra/Category/ModuleCat/Kernels.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean,Mathlib/Algebra/Category/ModuleCat/Subobject.lean,Mathlib/Algebra/Category/MonCat/FilteredColimits.lean,Mathlib/Algebra/Category/Ring/Colimits.lean,Mathlib/Algebra/Category/Ring/Limits.lean,Mathlib/Algebra/Group/Commute/Units.lean,Mathlib/Algebra/Group/Pointwise/Set/Card.lean,Mathlib/Algebra/Homology/ComplexShape.lean,Mathlib/Algebra/Homology/Double.lean,Mathlib/Algebra/Homology/HasNoLoop.lean,Mathlib/Algebra/Homology/Homotopy.lean,Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Algebra/Polynomial/Lifts.lean,Mathlib/Algebra/Polynomial/Sequence.lean,Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Complex/AbelLimit.lean,Mathlib/Analysis/Complex/AbsMax.lean,Mathlib/Analysis/Complex/Angle.lean,Mathlib/Analysis/Complex/Arg.lean,Mathlib/Analysis/Complex/Basic.lean,Mathlib/Analysis/Complex/CauchyIntegral.lean,Mathlib/Analysis/Complex/Circle.lean,Mathlib/Analysis/Complex/Hadamard.lean,Mathlib/Analysis/Complex/Isometry.lean,Mathlib/Analysis/Complex/Liouville.lean,Mathlib/Analysis/Complex/LocallyUniformLimit.lean,Mathlib/Analysis/Complex/OpenMapping.lean,Mathlib/Analysis/Complex/Periodic.lean,Mathlib/Analysis/Complex/PhragmenLindelof.lean,Mathlib/Analysis/Complex/Positivity.lean,Mathlib/Analysis/Complex/Schwarz.lean,Mathlib/Analysis/Complex/UnitDisc/Basic.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Exp.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean,Mathlib/Analysis/Fourier/AddCircle.lean,Mathlib/Analysis/Fourier/AddCircleMulti.lean,Mathlib/Analysis/Fourier/FourierTransformDeriv.lean,Mathlib/Analysis/Fourier/Inversion.lean,Mathlib/Analysis/Fourier/PoissonSummation.lean,Mathlib/Analysis/InnerProductSpace/TwoDim.lean,Mathlib/Analysis/MellinTransform.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/Normed/Lp/WithLp.lean,Mathlib/Analysis/PSeries.lean,Mathlib/Analysis/PSeriesComplex.lean,Mathlib/Analysis/SpecialFunctions/CompareExp.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Complex/Log.lean,Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean,Mathlib/Analysis/SpecialFunctions/Exp.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean,Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean,Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean,Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean,Mathlib/Analysis/SpecialFunctions/Integrals.lean,Mathlib/Analysis/SpecialFunctions/Log/Summable.lean,Mathlib/Analysis/SpecialFunctions/PolarCoord.lean,Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean,Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean,Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Pow/Real.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean,Mathlib/CategoryTheory/Abelian/FreydMitchell.lean,Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean,Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Coseparator.lean	205	10	['Champitoad', 'github-actions', 'joelriou']	nobody	52-41755 1 month ago	52-43028 1 month ago	0-38059 10 hours
14313	grhkm21 author:grhkm21	feat(RepresentationTheory/FdRep): FdRep is a full subcategory of Rep	``` /-- Equivalence between `FDRep` and the full subcategory of finite dimensional `Rep`. -/ def equivFiniteDimensional : FDRep k G ≌ FullSubcategory (fun V : Rep k G ↦ FiniteDimensional k V) ```	new-contributor t-algebra t-category-theory merge-conflict label:t-algebra$	47/8	Mathlib/RepresentationTheory/FDRep.lean	1	19	['github-actions', 'grhkm21', 'joelriou', 'kim-em', 'mathlib-bors']	nobody	49-74266 1 month ago	49-74266 1 month ago	125-12755 125 days
18626	hannahfechtner author:hannahfechtner	feat : define Artin braid groups	Define the Artin braid group on infinitely many strands. Includes a toGroup function which defines a function out of the braid group to any other group (given a function which satisfies the braid relations) (more to come in this file; next up: Artin braid groups on finitely many strands) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra merge-conflict awaiting-author label:t-algebra$	91/0	Mathlib.lean,Mathlib/GroupTheory/SpecificGroups/BraidGroup/Basic.lean	2	22	['github-actions', 'hannahfechtner', 'jcommelin', 'joelriou']	nobody	48-58577 1 month ago	48-58577 1 month ago	15-40648 15 days
14060	YnirPaz author:YnirPaz	feat(SetTheory/Ordinal/Clubs): define club sets and prove basic properties	Create a file where club sets are defined and their basic properties are proven. I also created a new recursion principle for ordinals, bounded recursion. --- - [ ] depends on: #19189 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-logic merge-conflict blocked-by-other-PR	315/3	Mathlib.lean,Mathlib/Order/SuccPred/Limit.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Club.lean,Mathlib/SetTheory/Ordinal/Topology.lean	6	93	['YaelDillies', 'YnirPaz', 'alreadydone', 'dupuisf', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp', 'zeramorphic']	nobody	46-16690 1 month ago	46-16690 1 month ago	92-44198 92 days
21959	BGuillemet author:BGuillemet	feat(Topology/ContinuousMap): Stone-Weierstrass theorem for MvPolynomial	Add the subalgebra of multivariate polynomials and prove it separates points, on the same model as `ContinuousMap/Polynomial.lean`. Prove the Stone-Weierstrass theorem and some variations for multivariate polynomials. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-topology merge-conflict	285/1	Mathlib.lean,Mathlib/Topology/ContinuousMap/MvPolynomial.lean,Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean	3	1	['github-actions']	nobody	44-60280 1 month ago	44-60280 1 month ago	16-76141 16 days
22349	dtumad author:dtumad	feat(Control): Laws for monads with compatible `failure` operation	Add a class for a `Monad` that also has an `Alternative` instance, and a class `LawfulAlternative` for types where the failure and monad structures are compatible in the expected way. --- I'm not sure if this should instead go in `Batteries.Control` instead of mathlib, or at least lemmas like `OptionT.run_failure` maybe should. Some of the instances like `Set` would still need to be added in mathlib either way. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-meta merge-conflict WIP	175/3	Mathlib.lean,Mathlib/Control/Lawful.lean,Mathlib/Control/Monad/AlternativeMonad.lean	3	8	['dtumad', 'eric-wieser', 'github-actions', 'quangvdao']	nobody	37-38625 1 month ago	37-38625 1 month ago	1-20563 1 day
15578	znssong author:znssong	feat(Function): Fixed points of function `f` with `f(x) >= x`	We added some lemmas of fixed points of function `f` with `f(x) >= x`, where `f : α → α` is a function on a finite type `α`. This will be needed in proof of Bondy-Chvátal theorem. --- See also branch `meow-sister/BondyChvatal`. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-analysis merge-conflict awaiting-author	82/0	Mathlib.lean,Mathlib/Dynamics/FixedPoints/Basic.lean,Mathlib/Dynamics/FixedPoints/Increasing.lean	3	32	['Ruben-VandeVelde', 'YaelDillies', 'github-actions', 'urkud', 'vihdzp', 'znssong']	nobody	36-56106 1 month ago	36-56106 1 month ago	29-48368 29 days
20171	mitchell-horner author:mitchell-horner	feat(Combinatorics/SimpleGraph): define turanDensity	Define the Turán density `turanDensity H` of a simple graph `H`: `turanDensity H` is the limit of `extremalNumber (Fin n) H / n.choose 2` as `n` approaches `∞`. Also prove - the Turán density of a simple graph is well-defined, that is, the limit `extremalNumber (Fin n) H / n.choose 2` as `n` approaches `∞` exists, - `extremalNumber (Fin n) H` is asymptotically equivalent to `turanDensity H * n.choose 2` as `n` approaches `∞`. --- - [ ] depends on: #19865 - [ ] depends on: #20681 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import new-contributor t-combinatorics merge-conflict blocked-by-other-PR WIP	854/95	Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/TuranDensity.lean,Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean,Mathlib/Combinatorics/SimpleGraph/SubgraphIso.lean,Mathlib/Combinatorics/SimpleGraph/Walk.lean,Mathlib/Data/Sym/Sym2.lean	10	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	35-4825 1 month ago	35-4825 1 month ago	0-2015 33 minutes
20240	mitchell-horner author:mitchell-horner	feat(Combinatorics/SimpleGraph): prove the Kővári–Sós–Turán theorem	Prove the Kővári–Sós–Turán theorem for simple graphs: the `completeBipartiteGraph α β`-free simple graphs on the vertex type `V` have at most `(card β-1)^(1/(card α))(card V)^(2-1/(card α))/2+(card α)(card V)/2` edges. --- - [ ] depends on: #19865 - [ ] depends on: #20738 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-combinatorics merge-conflict blocked-by-other-PR WIP	810/0	Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Pochhammer.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/KovariSosTuran.lean,Mathlib/Combinatorics/SimpleGraph/SubgraphIso.lean,Mathlib/Data/Nat/Choose/Cast.lean,Mathlib/RingTheory/Polynomial/Pochhammer.lean	7	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	35-4808 1 month ago	35-4808 1 month ago	0-555 9 minutes
8102	miguelmarco author:miguelmarco	feat (Tactic): add unify_denoms and collect_signs tactics	feat Tactic: add `unify_denoms` and `collect_signs` tactics --- This PR adds four new tactics: - `unify_denoms` tries to put expressions with several divisions in a form with only one division. In the case of fields, it works similarly to `field_simp`, but if the hypothesis about denominators being nonzero are not present, it assumes them, and leaves them as new goals to prove. In that sense, it is an "unsafe" tactic (but can be useful nevertheless, for example when you can't find which exact hypothesis is missing). It also works with expressions of naturals and Euclidean domains, assuming the corresponding hypothesis about the denominators dividing the numerators. - `unify_denoms!` extends `unify_denoms` to work with (in)equalities, assuming also that the denominators, once in normal form, are positive. - `collect_signs` works similarly with expressions using sums and substractions: it tries to put them in a form of one sum minus other sum. In the case of working with naturals, it assumes that we never substract a bigger number from a smaller one. Both are implemented essentially as a macro that combines several rewriting rules. Some new lemmas with the corresponding rules are added.	new-contributor t-meta merge-conflict awaiting-author enhancement	431/1	Mathlib/Algebra/EuclideanDomain/Basic.lean,Mathlib/Algebra/Group/Basic.lean,Mathlib/Data/Int/Order/Lemmas.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Nat/Order/Lemmas.lean,Mathlib/Tactic.lean,Mathlib/Tactic/CollectSigns.lean,Mathlib/Tactic/UnifyDenoms.lean	8	16	['github-actions', 'joneugster', 'kbuzzard', 'miguelmarco']	nobody	30-56512 30 days ago	64-577 2 months ago	17-12620 17 days
15686	robertmaxton42 author:robertmaxton42	refactor(LinearAlgebra/FreeProduct): move PowerAlgebra construction to its own namespace, minor simp opts	* Make the namespace `asPowers` to simplify/shorten names when working primarily with the power algebra construction of the free product * Also adds related some convenience API to `rel'` * Add simp shortcut attribute to `lift_comp_ι` and add simp shortcut lemma `lift_algebraMap` * Replaces some `aesop` calls with `simp_rw` for performance --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-algebra merge-conflict awaiting-author label:t-algebra$	143/11	Mathlib/LinearAlgebra/FreeProduct/Basic.lean	1	19	['YaelDillies', 'github-actions', 'kbuzzard', 'robertmaxton42']	nobody	27-27669 27 days ago	131-60239 4 months ago	80-18014 80 days
22714	pfaffelh author:pfaffelh	feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring.	~~Move results for rings (in terms of measure theory) to a separate file; was in Semiring.lean before.~~ For `∀ i ∈ s, IsSetSemiring (C i))`, the product `s.pi '' s.pi C` is a semiring. Prove two auxiliary lemmas in `Data.Set.Prod` needed on the way.	large-import new-contributor t-measure-probability merge-conflict awaiting-author	300/14	Mathlib/Data/Set/Pairwise/Lattice.lean,Mathlib/Data/Set/Prod.lean,Mathlib/MeasureTheory/MeasurableSpace/Pi.lean,Mathlib/MeasureTheory/PiSystem.lean,Mathlib/MeasureTheory/SetSemiring.lean	5	6	['EtienneC30', 'Paul-Lez', 'github-actions']	EtienneC30 assignee:EtienneC30	24-60443 24 days ago	28-42553 28 days ago	12-38130 12 days
21018	markimunro author:markimunro	feat(Data/Matrix): add file with key definitions and theorems about elementary row operations	Prove that each elementary row operation is equivalent to a multiplication by an elementary matrix, has another row operation which inverts it, and that each elementary matrix has a left inverse. This is a very large PR and I understand it will take time. This is my first one and will likely have issues but I will be ready to answer questions/fix them as soon as possible. Co-authored-by: Christopher Lynch --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data new-contributor merge-conflict awaiting-author enhancement	1230/0	Mathlib.lean,Mathlib/Data/Matrix/ElementaryRowOperations.lean,Mathlib/Data/Matrix/GaussianElimination.lean,Mathlib/Data/Matrix/GaussianEliminationOld,Mathlib/Data/Matrix/oldnames,et --hard 18533caba32,lean-toolchain	7	n/a	['chrisflav', 'eric-wieser', 'github-actions', 'j-loreaux', 'markimunro']	nobody	18-5105 18 days ago	unknown	unknown
11768	JovanGerb author:JovanGerb	feat: Interactive Library Rewrite	This PR defines the `rw??` library rewrite tactic that uses my `RefinedDiscrTree`. This is a point&click tactic, letting the user click on subexpressions in the main goal. The results are sorted by relevance, and are separated into sections based on the matched pattern. It comes with a filter button that allows you to switch between the (default) filtered view, with removed duplicate lemmas and not showing lemma names, and the complete view. There is also a section for definitionally unfolding the selected expression - these rewrites do not correspond to a library lemma. --- - [ ] depends on: #11968 - [x] depends on: #12016 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-meta merge-conflict blocked-by-other-PR	2788/1253	Mathlib.lean,Mathlib/Lean/GoalsLocation.lean,Mathlib/Lean/Meta/RefinedDiscrTree.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Pi.lean,Mathlib/Tactic.lean,Mathlib/Tactic/FunProp.lean,Mathlib/Tactic/FunProp/Elab.lean,Mathlib/Tactic/FunProp/StateList.lean,Mathlib/Tactic/FunProp/Theorems.lean,Mathlib/Tactic/FunProp/Types.lean,Mathlib/Tactic/Widget/InteractiveUnfold.lean,Mathlib/Tactic/Widget/LibraryRewrite.lean,Mathlib/Topology/Defs/Basic.lean,MathlibTest/LibraryRewrite.lean,MathlibTest/RefinedDiscrTree.lean,scripts/noshake.json	20	n/a	['JovanGerb', 'eric-wieser', 'fpvandoorn', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot']	nobody	16-72539 16 days ago	unknown	unknown
15212	victorliu5296 author:victorliu5296	feat: Add fundamental theorem of calculus-2 for Banach spaces	add the Mean Value Theorem for Banach spaces to the library and include reference for the theorem statement This theorem states that if `f : X → Y` is differentiable along the line segment from `a` to `b`, then the change in `f` equals the integral of its derivative along this path. This extends the mean value theorem to Banach spaces. This can be used for the eventual proof of the Newton-Kantorovich theorem with 1 constant contained inside the added reference. Here is the discussion on Zulipchat: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Contributing.20FTC-2.20for.20Banach.20spaces	new-contributor t-measure-probability t-analysis merge-conflict awaiting-author	60/1	Mathlib/MeasureTheory/Integral/FundThmCalculus.lean	1	3	['github-actions', 'hrmacbeth', 'victorliu5296']	nobody	13-94 13 days ago	13-94 13 days ago	51-85104 51 days
22701	ctchou author:ctchou	feat(Combinatorics): the Katona circle method	This file formalizes the Katona circle method. From PlainCombi (LeanCamCombi): https://github.com/YaelDillies/LeanCamCombi/blob/master/LeanCamCombi/PlainCombi/KatonaCircle.lean Co-authored-by: Yaël Dillies	new-contributor t-combinatorics merge-conflict	121/0	Mathlib.lean,Mathlib/Combinatorics/KatonaCircle.lean	2	1	['github-actions']	nobody	12-36049 12 days ago	12-36049 12 days ago	30-8337 30 days
21488	imbrem author:imbrem	feat(CategoryTheory/Monoidal): premonoidal categories	Add support for premonoidal categories --- Still want to add support for: - Premonoidal braided/symmetric categories - The monoidal coherence theorem, which I've already ported in my `discretion` library - The `coherence` tactic, which should work fine for premonoidal categories too but wanted to get this in front of reviewers ASAP to make sure my general approach was alright [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-category-theory merge-conflict	900/361	Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean,Mathlib/CategoryTheory/Bicategory/End.lean,Mathlib/CategoryTheory/GradedObject/Monoidal.lean,Mathlib/CategoryTheory/Localization/Monoidal.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Center.lean,Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/CategoryTheory/Monoidal/End.lean,Mathlib/CategoryTheory/Monoidal/Free/Basic.lean,Mathlib/CategoryTheory/Monoidal/Functor.lean,Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/CategoryTheory/Monoidal/Opposite.lean,Mathlib/CategoryTheory/Monoidal/Transport.lean,Mathlib/Tactic/CategoryTheory/Monoidal/Datatypes.lean,Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean,Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean,Mathlib/Tactic/CategoryTheory/MonoidalComp.lean,MathlibTest/StringDiagram.lean	21	9	['YaelDillies', 'github-actions', 'grunweg', 'imbrem', 'kim-em', 'leanprover-community-bot-assistant']	nobody	9-68682 9 days ago	9-68683 9 days ago	58-20339 58 days
20873	vbeffara author:vbeffara	feat(Topology/Covering): path lifting and homotopy lifting	This proves the existence and uniqueness of path and homotopy lifts through covering maps. --- I tried to separate as much of the proof as possible into separate PRs (which are already in Mathlib now), but the proof here relies on a monolithic construction of an explicit lift along a well-chosen subdivision, in `partial_lift`, with associated definitions. Only one standalone lean file added. An older WIP PR #10084 by Junyan Xu @alreadydone proves similar results using a very similar construction for path lifting, with a different argument to obtain continuity for homotopy lifting. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-topology merge-conflict awaiting-author	281/1	Mathlib.lean,Mathlib/Topology/Covering/Basic.lean,Mathlib/Topology/Covering/Lift.lean	3	9	['alreadydone', 'github-actions', 'grunweg', 'vbeffara']	nobody	8-71410 8 days ago	8-71410 8 days ago	55-53553 55 days

Stale delegated PRs

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
19633	grunweg author:grunweg	fix(CI): build the Archive and Counterexamples with --wfail also	This appears to be an oversight --- which has no consequences right now (the check for noisy output later would catch any warnings), but fixing it doesn't hurt either. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/No.20.60--wfail.60.20when.20building.20archive). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	CI awaiting-CI easy delegated	20/8	.github/build.in.yml,.github/workflows/bors.yml,.github/workflows/build.yml,.github/workflows/build_fork.yml	4	5	['adomani', 'github-actions', 'grunweg', 'kim-em', 'mathlib-bors']	nobody	130-23649 4 months ago	130-23649 4 months ago	7-42070 7 days
13483	adomani author:adomani	feat: automatically replace deprecations	This PR introduces `lake exe update_deprecations` that uses the cache to automatically replace deprecated declarations with the corresponding un-deprecated one. The script handles namespacing, replacing a possibly non-fully-qualified, deprecated name with the fully-qualified non-deprecated name. It is also possible to use ```bash lake exe update_deprecations --mods One.Two.Three,Dd.Ee.Ff ``` to limit the scope of the replacements to the modules `One.Two.Three` and `Dd.Ee.Ff`. This is intended to be a first step in automating updates: combining this with a linter that emits appropriate warnings, the functionality of `lake exe update_deprecations` can be extended to perform more complicated updates. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta delegated awaiting-author	306/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/UpdateDeprecations.lean,MathlibTest/UpdateDeprecations.lean,lakefile.lean,scripts/README.md,scripts/update_deprecations.lean	7	15	['YaelDillies', 'adomani', 'github-actions', 'j-loreaux', 'jcommelin', 'mathlib-bors', 'sgouezel']	joneugster assignee:joneugster	98-58441 3 months ago	98-58441 3 months ago	34-82472 34 days
21265	ADedecker author:ADedecker	feat: some lemmas about pointwise actions of units on filters and uniformities	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra t-topology delegated label:t-algebra$	45/0	Mathlib/Order/Filter/Pointwise.lean,Mathlib/Topology/Algebra/UniformMulAction.lean	2	7	['github-actions', 'mathlib-bors', 'ocfnash']	nobody	63-41970 2 months ago	63-41970 2 months ago	15-25642 15 days
23240	urkud author:urkud	feat(Topology/Maps): `IsOpenMap` and `ClusterPt`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-topology delegated	17/4	Mathlib/Topology/Maps/Basic.lean	1	6	['eric-wieser', 'github-actions', 'grunweg', 'mathlib-bors', 'urkud']	nobody	26-27169 26 days ago	26-34248 26 days ago	0-12104 3 hours
22366	kim-em author:kim-em	feat: `check_equalities` tactic for diagnosing defeq problems	The `check_equalities` tactic, which checks the typing of equalities in the goal, reporting discrepancies between the implicit type argument of the equality, and the inferred types of the left and right hand sides, at "instances and reducible" transparency. Reports from this tactic do not necessarily indicate a problem, although typically `simp` should reduce rather than increase the reported discrepancies. `check_equalities` may be useful in diagnosing uses of `erw`.	t-meta delegated	119/3	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Basic.lean,Mathlib/Tactic/CategoryTheory/CheckCompositions.lean,Mathlib/Tactic/CheckEqualities.lean,Mathlib/Tactic/Common.lean,MathlibTest/check_equalities.lean	7	12	['adomani', 'b-mehta', 'eric-wieser', 'github-actions', 'mathlib-bors']	nobody	14-71933 14 days ago	35-62158 1 month ago	15-14325 15 days
17129	joneugster author:joneugster	feat(Tactic/Linter): add unicode linter for unicode variant-selectors	Unicode characters can be followed by one of the two "variant-selectors" `\FE0E` (text) or `\FE0F` (emoji). These appear to the user as a single unicode character and they might copy them by accident. For example `✅️` (`\u2705\uFE0F`), `✅` (`\u2705`) and `✅︎` (`\u2705\uFE0E`) are three variants of the "same" unicode character. The one without variant-selector might display as either emoji or not, depending on the user's device and font. Add unicode linter ensuring variant-selector only appear on specified characters and also ensuring these characters always have the correct variant selector to avoid confusions. Everything flagged by this linter can be fixed fully automatically with `lake exe lint-style --fix` or by commenting `bot fix style` on the PR. --- - tracking PR: #16215 ## Zulip discussions: - https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Whitelist.20for.20Unicode.3F - https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20specific.20font ## Related PRs: - leanprover/lean4#5015 added some emoji-variant selectors to Emojis used in `Lean` itself. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import t-linter delegated awaiting-author	245/14	Mathlib.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/TextBased.lean,Mathlib/Tactic/Linter/UnicodeLinter.lean,Mathlib/Tactic/Widget/Calc.lean,Mathlib/Tactic/Widget/CongrM.lean,Mathlib/Tactic/Widget/Conv.lean,Mathlib/Tactic/Widget/GCongr.lean,Mathlib/Topology/ContinuousMap/Weierstrass.lean,MathlibTest/LintStyleTextBased.lean	11	24	['YaelDillies', 'adomani', 'github-actions', 'grunweg', 'joneugster', 'kim-em']	nobody	8-83929 8 days ago	12-5695 12 days ago	82-54712 82 days
22959	ScottCarnahan author:ScottCarnahan	chore (RingTheory/HahnSeries/SummableFamily): refactor HahnSeries.SummableFamily.powers to take junk values	This PR removes the positive order condition on the function `HahnSeries.SummableFamily.powers`, and instead takes the junk value zero when the input has non-positive order. This follows a reviewer suggestion from #20205. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra delegated label:t-algebra$	169/93	Mathlib/RingTheory/HahnSeries/HEval.lean,Mathlib/RingTheory/HahnSeries/Summable.lean	2	3	['github-actions', 'jcommelin', 'mathlib-bors']	nobody	6-41585 6 days ago	18-70843 18 days ago	15-77138 15 days
24078	jcommelin author:jcommelin	chore(LinearAlgebra): golf two proofs and remove porting notes	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra delegated label:t-algebra$	62/89	Mathlib/LinearAlgebra/Dimension/DivisionRing.lean,Mathlib/LinearAlgebra/LinearIndependent/Basic.lean	2	6	['b-mehta', 'github-actions', 'grunweg', 'mathlib-bors', 'riccardobrasca']	nobody	3-60494 3 days ago	3-62503 3 days ago	0-10728 2 hours
24074	ooovi author:ooovi	chore(Probability/Distributions): remove `open Classical ...` from `toMeasure_uniformOfFintype_apply`	Remove `open scoped Classical in` in front of the `toOuterMeasure_uniformOfFintype_apply` and `toMeasure_uniformOfFintype_apply` theorems --- I encountered a hard-to-debug error due to this, leading to the implicit use of the classical `Finset s` instance in the theorem statement, see [the zulip thread](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/coercing.20between.20types.20with.20different.20instances). I hear the removal of the use of the `Classical` namespace for theorem statements is an ongoing project, so feel free to either tell me to remove more occurances e.g. in this file, or defer this PR in favour of the ongoing project.	t-measure-probability delegated	7/7	Mathlib/Probability/Distributions/Uniform.lean	1	4	['eric-wieser', 'github-actions', 'mathlib-bors', 'ooovi']	nobody	2-81841 2 days ago	3-32051 3 days ago	0-47844 13 hours
23549	bryangingechen author:bryangingechen	chore: make dependabot group updates into a single PR	cf. docs at https://docs.github.com/en/code-security/dependabot/dependabot-version-updates/optimizing-pr-creation-version-updates --- It was a bit annoying to make a single bors batch for [#23544](https://github.com/leanprover-community/mathlib4/pull/23544) [#23543](https://github.com/leanprover-community/mathlib4/pull/23543) [#23541](https://github.com/leanprover-community/mathlib4/pull/23541) [#23540](https://github.com/leanprover-community/mathlib4/pull/23540).	CI delegated	10/0	.github/dependabot.yml	1	5	['adomani', 'github-actions', 'joneugster', 'mathlib-bors']	nobody	1-37707 1 day ago	1-37707 1 day ago	16-27325 16 days
22163	kebekus author:kebekus	feat: canonical tensors in inner product spaces	Given an `InnerProductSpace ℝ E`, this file defines two canonical tensors. * `InnerProductSpace.canonicalContravariantTensor E : E ⊗[ℝ] E →ₗ[ℝ] ℝ`. This is the element corresponding to the inner product. * If `E` is finite-dimensional, then `E ⊗[ℝ] E` is canonically isomorphic to its dual. Accordingly, there exists an element `InnerProductSpace.canonicalCovariantTensor E : E ⊗[ℝ] E` corresponding to `InnerProductSpace.canonicalContravariantTensor E` under this identification. This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. The canonical tensors are useful for defining the Laplace operator on inner product spaces in a coordinate-free way. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis delegated	63/0	Mathlib.lean,Mathlib/Analysis/InnerProductSpace/CanonicalTensor.lean	2	10	['adomani', 'github-actions', 'kebekus', 'loefflerd', 'mathlib-bors', 'sgouezel']	nobody	1-5897 1 day ago	1-61028 1 day ago	55-5556 55 days
14712	FR-vdash-bot author:FR-vdash-bot	perf: change instance priority and order about `OfNat`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	slow-typeclass-synthesis t-algebra merge-conflict delegated label:t-algebra$	49/20	Mathlib/Algebra/Group/Nat.lean,Mathlib/Algebra/Group/ZeroOne.lean,Mathlib/Algebra/Homology/Embedding/Basic.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Data/BitVec.lean,Mathlib/Data/Nat/Cast/Defs.lean,Mathlib/Data/Rat/Defs.lean,Mathlib/Data/UInt.lean,Mathlib/NumberTheory/ArithmeticFunction.lean	9	24	['FR-vdash-bot', 'MichaelStollBayreuth', 'eric-wieser', 'github-actions', 'j-loreaux', 'leanprover-bot', 'mathlib-bors']	nobody	194-78352 6 months ago	197-15428 6 months ago	20-15089 20 days
21761	JovanGerb author:JovanGerb	feat(Algebra): add lemmas `mul_self` and `add_self`	This is point (4) in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Possible.20improvements.20to.20Lean.2FMathlib/near/499085779 I decided to go with `n + n = 2 * n` instead of `n + n = n * 2` because it feels more natural. Feel free to suggest the opposite. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra merge-conflict delegated label:t-algebra$	206/196	Archive/Imo/Imo1959Q2.lean,Archive/Imo/Imo1961Q3.lean,Archive/Imo/Imo2008Q4.lean,Archive/Imo/Imo2013Q1.lean,Archive/Imo/Imo2024Q3.lean,Archive/MiuLanguage/DecisionSuf.lean,Archive/Wiedijk100Theorems/Partition.lean,Archive/ZagierTwoSquares.lean,Mathlib/Algebra/CharP/Two.lean,Mathlib/Algebra/CharZero/Lemmas.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Even.lean,Mathlib/Algebra/Lie/Weights/RootSystem.lean,Mathlib/Algebra/Order/Field/Basic.lean,Mathlib/Algebra/Order/Group/Lattice.lean,Mathlib/Algebra/Order/Group/Unbundled/Abs.lean,Mathlib/Algebra/Order/Ring/Basic.lean,Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean,Mathlib/Algebra/Order/Round.lean,Mathlib/Algebra/Polynomial/Taylor.lean,Mathlib/Algebra/Ring/BooleanRing.lean,Mathlib/Algebra/Ring/Defs.lean,Mathlib/Algebra/Ring/Hom/Defs.lean,Mathlib/Algebra/Ring/Int/Parity.lean,Mathlib/Algebra/Ring/Invertible.lean,Mathlib/Algebra/Ring/Parity.lean,Mathlib/Algebra/Ring/SumsOfSquares.lean,Mathlib/Algebra/Symmetrized.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean,Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean,Mathlib/Analysis/Complex/Isometry.lean,Mathlib/Analysis/Complex/PhragmenLindelof.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean,Mathlib/Analysis/Convex/Mul.lean,Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean,Mathlib/Analysis/InnerProductSpace/LinearMap.lean,Mathlib/Analysis/Normed/Lp/ProdLp.lean,Mathlib/Analysis/NormedSpace/MStructure.lean,Mathlib/Analysis/RCLike/Basic.lean,Mathlib/Analysis/SpecialFunctions/Bernstein.lean,Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean,Mathlib/Analysis/SpecialFunctions/PolarCoord.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean,Mathlib/Combinatorics/Additive/AP/Three/Defs.lean,Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean,Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean,Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Computability/AkraBazzi/AkraBazzi.lean,Mathlib/Computability/Language.lean,Mathlib/Data/Complex/Abs.lean,Mathlib/Data/Complex/Module.lean,Mathlib/Data/Complex/Norm.lean,Mathlib/Data/ENNReal/Holder.lean,Mathlib/Data/ENNReal/Inv.lean,Mathlib/Data/Nat/Bitwise.lean,Mathlib/Data/Nat/Cast/Order/Ring.lean,Mathlib/Data/Nat/Choose/Central.lean,Mathlib/Data/Num/Lemmas.lean,Mathlib/Data/Num/Prime.lean,Mathlib/Data/Real/Pi/Irrational.lean,Mathlib/Data/ZMod/Basic.lean,Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean,Mathlib/GroupTheory/Coxeter/Inversion.lean,Mathlib/GroupTheory/Perm/Cycle/Type.lean,Mathlib/GroupTheory/SpecificGroups/Alternating.lean,Mathlib/GroupTheory/SpecificGroups/Dihedral.lean,Mathlib/GroupTheory/SpecificGroups/KleinFour.lean,Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean,Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean,Mathlib/LinearAlgebra/Matrix/PosDef.lean,Mathlib/LinearAlgebra/QuadraticForm/Complex.lean,Mathlib/LinearAlgebra/SesquilinearForm.lean,Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean,Mathlib/MeasureTheory/Integral/Bochner.lean,Mathlib/MeasureTheory/Integral/Gamma.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/NumberTheory/Cyclotomic/Embeddings.lean,Mathlib/NumberTheory/FLT/Three.lean,Mathlib/NumberTheory/GaussSum.lean,Mathlib/NumberTheory/LegendreSymbol/Basic.lean,Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean,Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean,Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean,Mathlib/NumberTheory/Multiplicity.lean,Mathlib/NumberTheory/NumberField/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean,Mathlib/NumberTheory/PellMatiyasevic.lean,Mathlib/NumberTheory/SumPrimeReciprocals.lean	117	13	['JovanGerb', 'YaelDillies', 'github-actions', 'grunweg', 'mathlib-bors', 'riccardobrasca']	nobody	61-40246 2 months ago	61-71417 2 months ago	0-54729 15 hours
21266	ADedecker author:ADedecker	feat: restate uniformContinuous_mul in terms of convergence to uniformity	This is convenient when working with [Filter.Tendsto.congr_uniformity](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/UniformSpace/Basic.html#Filter.Tendsto.congr_uniformity) or [Filter.Tendsto.uniformity_trans](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/UniformSpace/Basic.html#Filter.Tendsto.uniformity_trans), for example. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-topology easy merge-conflict delegated	8/0	Mathlib/Topology/Algebra/UniformGroup/Defs.lean	1	5	['ADedecker', 'github-actions', 'j-loreaux', 'mathlib-bors']	nobody	18-69073 18 days ago	18-69073 18 days ago	0-18788 5 hours
19275	eric-wieser author:eric-wieser	fix: if nolint files change, do a full rebuild	Otherwise CI will succeed when removing entries from the file, but fail later when someone changes something unrelated. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict delegated	8/0	lakefile.lean	1	20	['YaelDillies', 'adomani', 'eric-wieser', 'github-actions', 'grunweg', 'mathlib-bors']	nobody	14-64696 14 days ago	14-64696 14 days ago	0-214 3 minutes