Welcome to the mathlib review page. Everybody's help with reviewing is appreciated. Reviewing contributions is important, and everybody is welcome to review pull requests! If you're not sure how, the pull request review guide is there to help you.
This page contains tables of
| 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 |
| 21129 |
chrisflav author:chrisflav |
perf(RingTheory/Kaehler/JacobiZariski): reorder universe variables |
Naming of universe variables has an impact on universe unification. It seems to matter that the universe variables of `R`, `S` and `T` appear before the universe variables of the generators in alphabetical order.
---
[](https://gitpod.io/from-referrer/)
|
performance-hack
t-algebra
label:t-algebra$ |
18/20 |
Mathlib/RingTheory/Kaehler/JacobiZariski.lean |
1 |
37 |
['chrisflav', 'erdOne', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'mattrobball'] |
nobody |
64-32603 2 months ago |
98-35064 3 months ago |
107-16368 107 days |
| 21909 |
erdOne author:erdOne |
feat(RingTheory/Invariants): Generalize to profinite groups |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
350/5 |
Mathlib.lean,Mathlib/Algebra/Algebra/Subalgebra/Operations.lean,Mathlib/NumberTheory/RamificationInertia/Galois.lean,Mathlib/RingTheory/Frobenius.lean,Mathlib/RingTheory/Invariant/Basic.lean,Mathlib/RingTheory/Invariant/Profinite.lean |
6 |
2 |
['TwoFX', 'github-actions'] |
nobody |
43-74136 1 month ago |
43-74136 1 month ago |
47-62311 47 days |
| 23684 |
alreadydone author:alreadydone |
feat(RingTheory): integral extensions of comm. rings are local homs |
---
The import increase only affects one file so I hope it's okay.
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
57/64 |
Mathlib/Algebra/Field/Equiv.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/Proper.lean,Mathlib/FieldTheory/LinearDisjoint.lean,Mathlib/LinearAlgebra/Dimension/Localization.lean,Mathlib/RingTheory/Artinian/Ring.lean,Mathlib/RingTheory/IntegralClosure/Algebra/Defs.lean,Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean,Mathlib/RingTheory/LinearDisjoint.lean,Mathlib/RingTheory/Localization/FractionRing.lean,Mathlib/RingTheory/Localization/Integral.lean,Mathlib/RingTheory/SimpleRing/Field.lean |
12 |
4 |
['alreadydone', 'github-actions', 'xroblot'] |
nobody |
39-37723 1 month ago |
39-69121 1 month ago |
39-69142 39 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`.
---
[](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 |
36-14542 1 month ago |
38-9610 1 month ago |
84-82835 84 days |
| 22474 |
joelriou author:joelriou |
feat(CategoryTheory/Functor): more API for pointwise Kan extensions |
Transport pointwise Kan extensions via isomorphisms/equivalences.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
157/7 |
Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean,Mathlib/CategoryTheory/Limits/HasLimits.lean,Mathlib/CategoryTheory/Limits/Opposites.lean,Mathlib/CategoryTheory/Limits/Shapes/Products.lean |
4 |
1 |
['github-actions'] |
nobody |
35-36312 1 month ago |
71-40175 2 months ago |
72-70447 72 days |
| 24041 |
YuvalFilmus author:YuvalFilmus |
feat: add support for bigop binders of the form "not in" and "not equal" |
feat: add support for bigop binders of the form "not in" and "not equal"
Added two new binders which can be used with big operators (product and summation).
The first, "not in", translates into "in ... complement".
The second, "not equal to", translates to `univ.erase ...`.
Also, improved documentation in the file header.
Delaboration updates can be considered next if wanted (to be coordinated with #22048).
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
7/0 |
Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean |
1 |
1 |
['github-actions'] |
nobody |
30-15322 1 month ago |
30-16623 1 month ago |
30-16678 30 days |
| 24053 |
plp127 author:plp127 |
feat(Topology): Priestley spaces are totally separated |
This generalizes `PriestleySpace.toT2Space`
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
9/5 |
Mathlib/Topology/Order/Priestley.lean |
1 |
3 |
['github-actions', 'plp127', 'urkud'] |
nobody |
29-74174 29 days ago |
29-77986 29 days ago |
29-77969 29 days |
| 24065 |
kim-em author:kim-em |
chore: script to give topological sort of modules |
This script is not useful by itself: it just gives a topological sort of Mathlib's import graph. But I've several times found it useful when I want to modify many files systematically with minimal rebuilding: just work backwards through the list.
|
|
96/0 |
scripts/README.md,scripts/topological_sort.py |
2 |
4 |
['github-actions', 'jcommelin', 'kim-em'] |
nobody |
29-43103 29 days ago |
29-54141 29 days ago |
29-54124 29 days |
| 23643 |
AntoineChambert-Loir author:AntoineChambert-Loir |
chore(RingTheory/MvPowerSeries/PiTopology): limit of truncation of power series |
Extract a lemma that says that for a multivariate power series, `trunc' R d f` converges to `f` when `d` converges to infinity.
Prove the analogous lemma for `MvPowerSeries.trunc` (if the set of indeterminates is nonempty).
Move this lemma and the denseness of polynomials to the `PiTopology` file.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
44/13 |
Mathlib/RingTheory/MvPowerSeries/Evaluation.lean,Mathlib/RingTheory/MvPowerSeries/PiTopology.lean,Mathlib/RingTheory/PowerSeries/PiTopology.lean |
3 |
17 |
['AntoineChambert-Loir', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'pechersky'] |
nobody |
28-80001 28 days ago |
29-24251 29 days ago |
40-77573 40 days |
| 23767 |
grunweg author:grunweg |
refactor: make library notes a definition |
Make library notes a definition of `Unit` type, whose doc-string is the note's content. As a consequence,
- doc-gen will display all library notes without any custom logic,
- library notes are shown upon hover (via the use of the doc-string),
- go do definition for library notes is easy
Automate this using a macro, which also enforces that all library notes are inside the Mathlib.LibraryNote namespace.
*Temporarily*, we use the `library_note2` name; if/when the batteries version is changed, we can reclaim the original name.
This PR does not address how to *refer* to library notes nicely (in a way that is shown in the documentation, checked for typos, with sufficient imports ensured etc.). That is left to a future PR.
This is proposal 2a from this [zulip discussion]([#mathlib4 > library notes @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/library.20notes/near/510614740))
------------
Open questions/TODOs:
- should this go in batteries instead? can the old definition just be overwritten?
- otherwise, what's the best place for the `LibraryNote` definition? A single file just for this feels overkill; I put it in Mathlib.Tactic.Basic for now. I could use Mathlib.Init, of course (but that might be excessive)
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
48/48 |
Archive/Imo/Imo2019Q2.lean,Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean,Mathlib/Algebra/Category/Ring/Limits.lean,Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Conj.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Hom/Defs.lean,Mathlib/Algebra/Group/Pointwise/Set/Basic.lean,Mathlib/Algebra/Group/Pointwise/Set/Scalar.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/HierarchyDesign.lean,Mathlib/Algebra/Order/Hom/Basic.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Note.lean,Mathlib/Analysis/RCLike/Lemmas.lean,Mathlib/CategoryTheory/Category/Basic.lean,Mathlib/Data/NNRat/Defs.lean,Mathlib/Data/Nat/Cast/Defs.lean,Mathlib/Data/Nat/Init.lean,Mathlib/Geometry/Manifold/Algebra/Monoid.lean,Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/Logic/Basic.lean,Mathlib/Tactic/Basic.lean,Mathlib/Tactic/NormNum/Basic.lean,Mathlib/Tactic/Simps/Basic.lean,Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean,Mathlib/Topology/Continuous.lean |
26 |
8 |
['adomani', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] |
nobody |
28-56895 28 days ago |
28-56895 28 days ago |
37-2748 37 days |
| 22039 |
YaelDillies author:YaelDillies |
feat: simproc for computing `Finset.Ixx` of natural numbers |
---
- [x] depends on: #22290
- [x] depends on: #22559
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
315/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Simproc/FinsetInterval.lean,Mathlib/Util/Qq.lean |
4 |
58 |
['FLDutchmann', 'Paul-Lez', 'YaelDillies', 'eric-wieser', 'github-actions', 'kim-em', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
28-32355 28 days ago |
28-32373 28 days ago |
83-79495 83 days |
| 22582 |
vlad902 author:vlad902 |
feat: generalize theorems with linter fixes |
This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile. Otherwise, the type class is not being generalized, but can simply be replaced by implicit type class synthesis (or an implicit type class in a variable block being pulled in.)
The linter currently output debug statements indicating source file positions where type classes should be generalized, and a script then makes those edits. This file contains a subset of those generalizations. The linter and the script performing re-writes is available in commit 7b436512017640c3c33aea50b2435b2ee0d995c9.
Note that this PR specifically generalizes theorems across a range of files and type classes, the common theme is that the resulting changes all cause type classes in variable declarations to go unused.
Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855 |
new-contributor
t-algebra
t-analysis
label:t-algebra$ |
30/50 |
Mathlib.lean,Mathlib/Algebra/Algebra/Basic.lean,Mathlib/Algebra/Group/Action/Faithful.lean,Mathlib/Algebra/GroupWithZero/Action/Faithful.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Operator/Compact.lean,Mathlib/GroupTheory/Perm/Subgroup.lean,Mathlib/Topology/Algebra/ConstMulAction.lean |
8 |
11 |
['github-actions', 'urkud', 'vlad902'] |
urkud assignee:urkud |
26-82038 26 days ago |
26-82038 26 days ago |
69-62970 69 days |
| 11968 |
JovanGerb author:JovanGerb |
feat: improvements to RefinedDiscrTree |
This PR defines `RefinedDiscrTree`, which is an improved version of `DiscrTree` with many new features, such as
- indexing lambda terms, dependent forall terms, and bound variables.
- giving a score to matches, in order to sort them
- indexing star patterns so that `a+b` and `a+a` are indexed differently
- taking into account eta reductions, so that `exp` can still be matched with the library pattern `fun x => exp (f x)`.
This PR makes `RefinedDiscrTree` into a lazy data structure, meaning that it can be used without a cache, just like `LazyDiscrTree`.
This PR also removes these features:
- indexing `fun x => x` as `id`
- indexing `fun x => f x + g x` as `f + g`, and similarly for `-`, `*`, `/`, `⁻¹`, `^`.
- indexing `fun _ => 42` as `42`
These equivalent indexings do not hold definitionally in the `reducible` transparency, which is the transparency that is used for unification when using a discrimination tree. Therefore, indexing these different expressions the same is actually inefficient rather than helpful.
This is part of the bigger #11768, which uses this discrimination tree for a library rewriting tactic.
This replaces an older version of `RefinedDiscrTree`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
|
1631/1242 |
Mathlib.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/Topology/Defs/Basic.lean,MathlibTest/RefinedDiscrTree.lean,scripts/noshake.json |
16 |
78 |
['0art0', 'JovanGerb', 'eric-wieser', 'github-actions', 'grunweg', 'joneugster', 'leanprover-bot', 'rosborn'] |
nobody |
26-76559 26 days ago |
37-74462 1 month ago |
212-12824 212 days |
| 19668 |
YaelDillies author:YaelDillies |
refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction |
The motivation for this change is that it is really confusing to run `intro r s shouldnthaveintroedthat` on a goal of the form `∀ r s : ℝ≥0∞, r ≤ s` and get the nonsense-looking goal `r = ↑shouldnthaveintroedthat → ∃ b : α, s = ↑b ∧ shouldnthaveintroedthat ≤ b⟩` instead of an error, and similarly when destructing something of the form `∃ r s : ℝ≥0∞, r < s`.
Furthermore, I suspect this improves performance.
---
- [x] depends on: #20317
- [x] depends on: #20318
- [x] depends on: #21274
- [x] depends on: #22109
[](https://gitpod.io/from-referrer/)
|
t-order |
65/47 |
Mathlib/Analysis/Analytic/OfScalars.lean,Mathlib/Analysis/Oscillation.lean,Mathlib/Data/Finset/Lattice/Fold.lean,Mathlib/Data/Finset/Max.lean,Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Countable.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/Order/Interval/Basic.lean,Mathlib/Order/Interval/Set/WithBotTop.lean,Mathlib/Order/WithBot.lean,Mathlib/Probability/Variance.lean,Mathlib/RingTheory/PowerBasis.lean,Mathlib/Topology/MetricSpace/Holder.lean,Mathlib/Topology/MetricSpace/HolderNorm.lean |
14 |
17 |
['YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
25-74806 25 days ago |
35-48407 1 month ago |
47-82680 47 days |
| 24050 |
Paul-Lez author:Paul-Lez |
feat(Data/Finsupp/Pointwise): generalise pointwise scalar multiplication of finsupps |
As pointed out by @eric-wieser, this creates an instance diamond with `SMul (α → β) (α →₀ (α → β))`
---
[](https://gitpod.io/from-referrer/)
|
t-data |
7/4 |
Mathlib/Data/Finsupp/Pointwise.lean |
1 |
6 |
['Paul-Lez', 'eric-wieser', 'github-actions'] |
nobody |
25-13772 25 days ago |
29-82186 29 days ago |
29-82238 29 days |
| 12561 |
BoltonBailey author:BoltonBailey |
doc: suggest !bench in `lake exe pole` |
This change explains what to do if the benchmarks haven't been run.
---
- [x] depends on: #12322
[](https://gitpod.io/from-referrer/)
|
|
2/1 |
LongestPole/Main.lean |
1 |
2 |
['github-actions', 'leanprover-community-mathlib4-bot'] |
nobody |
24-64920 24 days ago |
unknown |
unknown |
| 23964 |
BoltonBailey author:BoltonBailey |
docs: Add documentation arbitrarily |
@mattrobball asked in the Mathlib Community meeting today what it would look like if we asked Claude code to give us improved documentation. I made this draft PR by selecting five declarations arbitrarily from `nolints.json` and asking Cursor to document them.
---
[](https://gitpod.io/from-referrer/)
|
documentation |
52/14 |
Mathlib/Algebra/Homology/Homotopy.lean,Mathlib/Analysis/BoxIntegral/Partition/Filter.lean,Mathlib/Control/Monad/Cont.lean,Mathlib/Data/Stream/Defs.lean,Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean |
5 |
10 |
['ADedecker', 'BoltonBailey', 'eric-wieser', 'github-actions', 'jcommelin', 'mattrobball'] |
nobody |
24-42575 24 days ago |
31-83418 1 month ago |
32-60036 32 days |
| 24218 |
alreadydone author:alreadydone |
chore(Algebra): remove `mid_assoc` from `IsMulCentral` |
as it is a consequence of left and right associativity in the presence of commutativity. Also change the commutativity condition to use `Commute`.
---
Even without commutativity, left and right associativity of an element `e` in a magma is sufficient to prove that elements of the form `e * x * e` (the "corner" of `e`) form a submagma.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
31/69 |
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Group/Center.lean,Mathlib/Algebra/GroupWithZero/Center.lean,Mathlib/Algebra/Ring/Center.lean,Mathlib/Algebra/Ring/CentroidHom.lean,Mathlib/Algebra/Star/Center.lean,Mathlib/Algebra/Star/CentroidHom.lean,Mathlib/GroupTheory/Submonoid/Center.lean,Mathlib/LinearAlgebra/Basis/Submodule.lean,Mathlib/LinearAlgebra/QuadraticForm/Basic.lean,Mathlib/RingTheory/Idempotents.lean,Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean |
12 |
8 |
['alreadydone', 'github-actions', 'mans0954'] |
nobody |
24-9093 24 days ago |
24-24153 24 days ago |
24-24143 24 days |
| 22771 |
alreadydone author:alreadydone |
feat(Homotopy/Lifting): monodromy of a covering map and lifting criterion |
Definition 2.1 in https://ncatlab.org/nlab/show/monodromy.
Also:
+ Extract `FundamentalGroupoid.map (f : C(X, Y)) : FundamentalGroupoid X ⥤ FundamentalGroupoid Y` from `fundamentalGroupoidFunctor : TopCat ⥤ CategoryTheory.Grpd`
+ Define `FundamentalGroup.map (f : C(X, Y)) (x : X) : FundamentalGroup X x →* FundamentalGroup Y (f x)` and `mapOfEq : FundamentalGroup X x →* FundamentalGroup Y y` that takes an assumption `f x = y`.
+ Redefine `FundamentalGroup` to be `End` rather than `Aut`: since `FundamentalGroupoid` is a groupoid, `End` already has a group structure.
+ Golf within the file FundamentalGroupoid/Basic.
+ Generalize `toArrow` up to `fromPath` in `FundamentalGroupoid/FundamentalGroup` from `X : TopCat` to `[TopologicalSpace X]`.
Also golfs some proofs and redefines
---
- [x] depends on: #22649
[](https://gitpod.io/from-referrer/)
|
t-topology |
193/147 |
Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean,Mathlib/CategoryTheory/Groupoid.lean,Mathlib/Topology/Covering.lean,Mathlib/Topology/Homotopy/HomotopyGroup.lean,Mathlib/Topology/Homotopy/Lifting.lean,Mathlib/Topology/Homotopy/Product.lean |
9 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
22-70774 22 days ago |
56-32395 1 month ago |
56-34290 56 days |
| 24295 |
jsm28 author:jsm28 |
feat(Topology/Algebra/AffineSubspace): `AffineSubspace.subtypeA` |
Define the embedding map from an affine subspace to the ambient space as a continuous affine map, analogous to `Submodule.subtypeL`. There wasn't an immediately obvious location importing both continuous affine maps and affine subspaces, so I put this in its own file.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-topology
label:t-algebra$ |
42/0 |
Mathlib.lean,Mathlib/Topology/Algebra/AffineSubspace.lean |
2 |
1 |
['github-actions'] |
nobody |
21-84275 21 days ago |
21-84340 21 days ago |
21-84323 21 days |
| 24103 |
plp127 author:plp127 |
feat(Topology/UniformSpace/OfCompactT2): generalize theorem |
Generalize `uniformSpaceOfCompactT2` to `uniformSpaceOfCompactR1`.
---
- [ ] depends on: #24098
[](https://gitpod.io/from-referrer/)
|
t-topology |
57/24 |
Mathlib/Topology/Separation/Basic.lean,Mathlib/Topology/Separation/Regular.lean,Mathlib/Topology/UniformSpace/OfCompactT2.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
21-6812 21 days ago |
21-6815 21 days ago |
21-8407 21 days |
| 24215 |
BoltonBailey author:BoltonBailey |
chore: remove erw from WSeq.bind_assoc |
---
[](https://gitpod.io/from-referrer/)
|
tech debt |
9/2 |
Mathlib/Data/WSeq/Relation.lean |
1 |
5 |
['BoltonBailey', 'github-actions', 'kim-em', 'mathlib-bors'] |
nobody |
20-63984 20 days ago |
20-63984 20 days ago |
20-85464 20 days |
| 24260 |
plp127 author:plp127 |
feat(Topology): Add API for Hereditarily Lindelof spaces |
Copies the stuff about Lindelof spaces to Hereditarily Lindelof spaces.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
222/42 |
Mathlib/Topology/Compactness/Lindelof.lean |
1 |
13 |
['github-actions', 'urkud'] |
nobody |
20-49355 20 days ago |
20-83737 20 days ago |
22-67962 22 days |
| 23926 |
b-reinke author:b-reinke |
feat(Algebra/BigOperators/Finprod): add powerset projection lemmas |
This PR adds lemmas in `Mathlib/Algebra/BigOperators/Finprod.lean` related to products/sums over the powerset `𝒫 s` when we add or remove an element of `s`.
The motivation comes from the proof of the deletion/contraction properties of matroids.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
30/0 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Image.lean |
2 |
5 |
['b-reinke', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
20-39689 20 days ago |
20-41481 20 days ago |
33-42004 33 days |
| 18693 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: add ConjRootClass |
Co-authored-by: FR
---
From #6718
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
213/0 |
Mathlib.lean,Mathlib/FieldTheory/Minpoly/ConjRootClass.lean,Mathlib/FieldTheory/Minpoly/IsConjRoot.lean |
3 |
13 |
['LessnessRandomness', 'Vierkantor', 'alreadydone', 'github-actions', 'grunweg'] |
nobody |
20-4939 20 days ago |
20-42702 20 days ago |
82-24447 82 days |
| 23547 |
chrisflav author:chrisflav |
feat(AlgebraicGeometry): codescent implies descent |
Let `P` and `P'` be morphism properties of schemes. We show some results to deduce
that `P` descends along `P'` from a codescent property of ring homomorphisms.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
258/1 |
Mathlib.lean,Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean,Mathlib/AlgebraicGeometry/Morphisms/Descent.lean,Mathlib/RingTheory/RingHomProperties.lean |
4 |
14 |
['chrisflav', 'erdOne', 'github-actions'] |
nobody |
18-77350 18 days ago |
18-77350 18 days ago |
39-65166 39 days |
| 24394 |
wwylele author:wwylele |
feat(Analysis/Asymptotics): Add filter operation theorems to `IsEquivalent` |
These are simply restating the corresponding theorems for `isLittleO`, but adding them provides better discovery when one is not familiar with how `IsEquivalent` is defined.
I tagged `isEquivalent_map` as `@[simp]` because all of `isBigOWith/isBigO/isLittleO_map` are tagged, but I am not sure if this appropriate. Please let me know if I should remove the tag
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-analysis
|
13/0 |
Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean |
1 |
1 |
['github-actions'] |
nobody |
18-238 18 days ago |
18-238 18 days ago |
18-297 18 days |
| 16074 |
Rida-Hamadani author:Rida-Hamadani |
feat: combinatorial maps and planar graphs |
We define combinatorial maps, then we define planar graph using combinatorial maps.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
243/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Planar.lean,Mathlib/Data/CombinatorialMap.lean |
3 |
27 |
['Parcly-Taxel', 'Rida-Hamadani', 'github-actions', 'lambda-fairy', 'leanprover-community-bot-assistant'] |
nobody |
17-30754 17 days ago |
17-32738 17 days ago |
21-20170 21 days |
| 22631 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): define associated graded structure for abelian group |
In this PR we define the associated graded structure for abelian group when given a filtration and only give some basic lemmas about it.
Further results would be given in #20913
---
- [x] depends on: #24071
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
155/0 |
Mathlib.lean,Mathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean |
2 |
16 |
['AntoineChambert-Loir', 'Thmoas-Guan', 'eric-wieser', 'github-actions', 'kbuzzard', 'mathlib4-dependent-issues-bot'] |
nobody |
17-29452 17 days ago |
29-1517 29 days ago |
68-81525 68 days |
| 24303 |
robin-carlier author:robin-carlier |
feat(Tactic/CategoryTheory): extension of `reassoc` to equality of isomorphisms |
Extend the `reassoc` attribute so that it can also generate `_assoc` variants of lemmas of shape `∀ .., f = g`,
where `f g : X ≅ Y`. We similarly extend `reassoc_of%`.
We also provide a very basic test suite for this extension.
---
requested by @joelriou in #24252.
[](https://gitpod.io/from-referrer/)
|
t-category-theory
t-meta
|
201/9 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/CategoryTheory/IsoReassoc.lean,Mathlib/Tactic/CategoryTheory/Reassoc.lean,MathlibTest/CategoryTheory/Reassoc.lean |
5 |
6 |
['github-actions', 'joelriou', 'leanprover-bot', 'robin-carlier'] |
nobody |
17-23540 17 days ago |
21-13778 21 days ago |
21-39018 21 days |
| 24412 |
pechersky author:pechersky |
feat(UniformSpace/Ultra/Constructions): IsUltraUniformity.{bot,top} |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
29/0 |
Mathlib/Order/Filter/Bases/Basic.lean,Mathlib/Topology/UniformSpace/Defs.lean,Mathlib/Topology/UniformSpace/Ultra/Basic.lean,Mathlib/Topology/UniformSpace/Ultra/Constructions.lean |
4 |
1 |
['github-actions'] |
nobody |
17-13764 17 days ago |
17-13920 17 days ago |
17-13913 17 days |
| 22586 |
joelriou author:joelriou |
feat(CategoryTheory/Localization): the right derivability structure given by functorial resolutions |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
152/0 |
Mathlib.lean,Mathlib/CategoryTheory/Localization/DerivabilityStructure/OfFunctorialResolutions.lean,Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean |
3 |
1 |
['github-actions'] |
nobody |
16-85930 16 days ago |
70-31433 2 months ago |
70-31415 70 days |
| 24405 |
mcdoll author:mcdoll |
refactor(Topology/Algebra/Module/WeakDual): Clean up |
- Move `Dual` and `dualPairing` lower in the import-hierachy
- deduplicate `dualPairing`
- Make `WeakDual` and `WeakSpace` reducible
---
New version of #11500
[](https://gitpod.io/from-referrer/)
|
large-import
t-topology
|
146/162 |
Mathlib.lean,Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean,Mathlib/Analysis/InnerProductSpace/Adjoint.lean,Mathlib/Analysis/InnerProductSpace/Dual.lean,Mathlib/Analysis/LocallyConvex/WeakSpace.lean,Mathlib/Analysis/Normed/Module/Dual.lean,Mathlib/Analysis/Normed/Module/WeakDual.lean,Mathlib/Analysis/VonNeumannAlgebra/Basic.lean,Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean,Mathlib/MeasureTheory/Measure/FiniteMeasure.lean,Mathlib/Topology/Algebra/Module/Dual.lean,Mathlib/Topology/Algebra/Module/WeakDual.lean,docs/overview.yaml,docs/undergrad.yaml |
14 |
1 |
['github-actions'] |
nobody |
16-62765 16 days ago |
16-71458 16 days ago |
16-71441 16 days |
| 22961 |
xroblot author:xroblot |
feat(ZLattice/Covolume): add `covolume_div_covolume_eq_relindex` |
Add the following result:
Let `L₁` be a sub-`ℤ`-lattice of `L₂`. Then the index of `L₁` inside `L₂` is equal to `covolume L₁ / covolume L₂`.
---
- [x] depends on: #22940
- [x] depends on: #23759
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
66/4 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Algebra/Module/ZLattice/Covolume.lean,Mathlib/GroupTheory/Index.lean,Mathlib/LinearAlgebra/Determinant.lean |
4 |
10 |
['Ruben-VandeVelde', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'xroblot'] |
nobody |
16-37992 16 days ago |
16-38008 16 days ago |
52-80568 52 days |
| 24439 |
mariainesdff author:mariainesdff |
feat(Data/Nat/Factorial/NatCast): add natCast_factorial_of_isNilpotent |
Co-authored-by: @AntoineChambert-Loir.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
32/2 |
Mathlib/Data/Nat/Factorial/NatCast.lean |
1 |
3 |
['b-mehta', 'github-actions', 'mariainesdff'] |
nobody |
15-24753 15 days ago |
15-24753 15 days ago |
16-12111 16 days |
| 24447 |
dagurtomas author:dagurtomas |
feat(Condensed): light condensed modules form a Grothendieck abelian category |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-condensed
|
32/4 |
Mathlib/Algebra/Category/ModuleCat/AB.lean,Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean,Mathlib/Condensed/Light/AB.lean |
3 |
3 |
['dagurtomas', 'erdOne', 'github-actions'] |
nobody |
15-21627 15 days ago |
15-21627 15 days ago |
15-27011 15 days |
| 23657 |
grunweg author:grunweg |
feat: euclidean half spaces and quadrants have convex interior |
These lemmas are a prerequisite for #23658, which will impose that real or complex models with corners have convex interior.
---
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
48/0 |
Mathlib/Geometry/Manifold/Instances/Real.lean |
1 |
14 |
['Ruben-VandeVelde', 'github-actions', 'grunweg', 'sgouezel', 'urkud'] |
nobody |
15-18813 15 days ago |
15-18814 15 days ago |
40-39399 40 days |
| 24448 |
Hagb author:Hagb |
feat(RingTheory/Ideal/Span.lean): some lemmas about zero and span |
`simp` would be able to solve them.
Notice that `span_singleton_zero : span {(0 : R)} = ⊥` itself can be solved by `simp` without this commit, which uses `span_singleton_eq_bot : span ({x} : Set α) = ⊥ ↔ x = 0`, while `simp` cannot solve goals like `f (Ideal.span {(0 : R)}) = f ⊥`, which would be solvable by `simp` with `span_singleton_zero` marked with `@[simp]`.
Without adding also `Ideal.dvd_span_bot` to `Mathlib/RingTheory/DedekindDomain/Ideal.lean`, these lemmas on `Span.lean` would make the following failed, since `simp` would rewrite `{0}` with `⊥` and result in a goal `v.asIdeal ∣ ⊥` that it can't solve.
https://github.com/leanprover-community/mathlib4/blob/3f2556372f27171259a381d4d57db71440700cd8/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean#L123
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
16/1 |
Mathlib/Algebra/Module/PID.lean,Mathlib/RingTheory/DedekindDomain/Ideal.lean,Mathlib/RingTheory/Ideal/Span.lean |
3 |
1 |
['github-actions'] |
nobody |
15-14341 15 days ago |
15-24332 15 days ago |
15-24386 15 days |
| 23888 |
j-loreaux author:j-loreaux |
feat: properties of graded rings indexed by canonically linearly ordered additive monoids |
---
- [ ] depends on: #23883
- [ ] depends on: #23886
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
100/0 |
Mathlib/Algebra/DirectSum/Internal.lean |
1 |
12 |
['adomani', 'eric-wieser', 'github-actions', 'j-loreaux', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
14-78663 14 days ago |
34-8153 1 month ago |
34-8951 34 days |
| 16408 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprecate `Order.Nat` |
* Move the two `Nat` instances and `bot_eq_zero` to `Order.BoundedOrder.Basic`. We also remove the TODO relating to #13092, as it was tried and it was agreed not to be a good idea.
* Move the other two lemmas in `Order.Nat` to `Data.Nat.Find`. |
will-close-soon
tech debt
|
35/54 |
Mathlib/Algebra/IsPrimePow.lean,Mathlib/Data/Finset/Grade.lean,Mathlib/Data/Finset/Lattice/Fold.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Nat/Cast/SetInterval.lean,Mathlib/Data/Nat/Find.lean,Mathlib/Data/Nat/SuccPred.lean,Mathlib/Data/Rat/Cast/Defs.lean,Mathlib/Order/BoundedOrder/Basic.lean,Mathlib/Order/Filter/AtTopBot/Basic.lean,Mathlib/Order/Nat.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/SetTheory/Cardinal/Order.lean |
13 |
8 |
['Parcly-Taxel', 'YaelDillies', 'github-actions', 'grunweg'] |
nobody |
14-78590 14 days ago |
14-78590 14 days ago |
31-11635 31 days |
| 24265 |
yoh-tanimoto author:yoh-tanimoto |
feat(MeasureTheory/Integral): the Riesz-Markov-Kakutani theorem for `NNReal`-linear functionals |
prove the Riesz-Markov-Kakutani theorem for `NNReal`-linear functional, by reducing the statement to the `Real`-version, but for `lintegral` instead of `integral`.
The bulk of the PR is the definitions and lemmas to go back and forth between `Real` and `NNReal` linear functionals.
Motivation: this is the version first aimed at, perhaps for applications in probability. |
t-measure-probability |
233/16 |
Mathlib.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/NNReal.lean,Mathlib/Topology/ContinuousMap/CompactlySupported.lean |
4 |
24 |
['github-actions', 'oliver-butterley', 'sgouezel', 'yoh-tanimoto'] |
nobody |
14-64488 14 days ago |
16-85678 16 days ago |
21-75279 21 days |
| 24471 |
IvanRenison author:IvanRenison |
feat: define `IsPositive` and Löwner order for `LinearMap` |
---
Discussion in zulip: https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Positive-semidefinite.20linear.20operator
I don't now if what I'm doing is the best way to do this.
Probably it is possible to have `StarOrderedRing (H →ₗ[𝕜] H)`, but it is not so easy, so I think maybe is better to add it in a different pull request
[](https://gitpod.io/from-referrer/)
|
t-analysis |
117/9 |
Mathlib/Analysis/InnerProductSpace/LinearMap.lean,Mathlib/Analysis/InnerProductSpace/Positive.lean,Mathlib/Analysis/InnerProductSpace/Symmetric.lean |
3 |
1 |
['github-actions'] |
nobody |
14-26130 14 days ago |
14-27208 14 days ago |
14-27275 14 days |
| 24497 |
Parcly-Taxel author:Parcly-Taxel |
feat: IMO 1985 Q2 |
|
IMO |
100/0 |
Archive.lean,Archive/Imo/Imo1985Q2.lean |
2 |
1 |
['github-actions'] |
nobody |
13-34654 13 days ago |
13-34717 13 days ago |
13-34701 13 days |
| 24380 |
chrisflav author:chrisflav |
chore(RingTheory/TensorProduct): more product compatibilities |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
48/4 |
Mathlib/RingTheory/TensorProduct/Pi.lean |
1 |
3 |
['erdOne', 'github-actions'] |
nobody |
13-26213 13 days ago |
13-26213 13 days ago |
14-70573 14 days |
| 24452 |
robin-carlier author:robin-carlier |
feat(Tactic/CategoryTheory): `Cancelable` boilerplate for the `rotate_isos` WIP tactic |
This PR adds some boilerplate that will be used in a forthcoming PR implementing a `rotate_isos` tactic that aims to provide easy ways of moving one or more morphisms that can be inferred to be isomorphisms (not necessarily through the `IsIso typeclass, but also directly by recognizing them as e.g components of natural isomorphisms, or functor application to such morphisms).
The boilerplate in this PR abstracts the notion of a cancelable expression for a morphism in a composition of (iso)morphisms in a category, and records a global reference to a list of "cancelable factories", _i.e_ functions that try to recognize term in an expression as a "cancelable" morphism, and provides helper to register such functions.
---
First part of a series of 3 PRs contributing the `rotate_isos` tactic to mathlib. Second part will actually implement the tactic, and provide a test suite. Please read the description of the second PR (#24454) to get more details.
[](https://gitpod.io/from-referrer/)
|
t-category-theory
t-meta
|
162/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/CategoryTheory/RotateIsos/Cancelable.lean,scripts/noshake.json |
4 |
1 |
['github-actions'] |
nobody |
13-23518 13 days ago |
13-25647 13 days ago |
13-33786 13 days |
| 24517 |
upobir author:upobir |
feat(Algebra/QuadraticDiscriminant): Adding inequalities on quadratic from inequalities on discriminant |
---
This pr adds inequalities that relate `0` and `a * (x * x) + b * x + c` from inequalities of `a` and `discrim a b c`. For example, negative discriminant and negative leading coefficient implies value of quadratic expression is always negative and similar.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
35/0 |
Mathlib/Algebra/QuadraticDiscriminant.lean |
1 |
1 |
['github-actions'] |
nobody |
13-13581 13 days ago |
13-13581 13 days ago |
13-13634 13 days |
| 24522 |
dagurtomas author:dagurtomas |
chore(Condensed): introduce an abbrev for the equivalence of light condensed sets with a category of sheaves on a small site |
---
[](https://gitpod.io/from-referrer/)
|
t-condensed |
39/0 |
Mathlib.lean,Mathlib/Condensed/Light/Small.lean |
2 |
1 |
['github-actions'] |
nobody |
13-6673 13 days ago |
13-6874 13 days ago |
13-6930 13 days |
| 20719 |
gio256 author:gio256 |
feat(AlgebraicTopology): delaborators for truncated simplicial notations |
We add delaborators for the following notations, introduced in #20688:
- `⦋m⦌ₙ`, which denotes the `m`-dimensional simplex in the `n`-truncated simplex category.
- `X _⦋m⦌ₙ`, which denotes the `m`-th term of an `n`-truncated simplicial object `X`.
- `X ^⦋m⦌ₙ`, which denotes the `m`-th term of an `n`-truncated cosimplicial object `X`.
If `pp.proofs` is set to `true`, we also pretty-print the proof `p : m ≤ n` for all three notations as `⦋m, p⦌ₙ`, `X _⦋m, p⦌ₙ`, and `X ^⦋m, p⦌ₙ`, respectively.
Credit to @kmill for one piece of code and much metaprogramming inspiration.
---
- [x] depends on: #20688
- [x] depends on: #23018
[](https://gitpod.io/from-referrer/)
|
infinity-cosmos
t-category-theory
t-meta
|
525/33 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean,Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean,Mathlib/Tactic.lean,Mathlib/Tactic/SimplexCategory.lean,Mathlib/Util/Superscript.lean,MathlibTest/SimplexCategory.lean,MathlibTest/SimplicialObject.lean,MathlibTest/superscript.lean,scripts/noshake.json |
11 |
22 |
['eric-wieser', 'gio256', 'github-actions', 'kim-em', 'mathlib4-dependent-issues-bot'] |
eric-wieser assignee:eric-wieser |
13-4102 13 days ago |
13-6743 13 days ago |
21-78285 21 days |
| 23752 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Incenter): incenters and excenters |
Define the exspheres and insphere of a simplex (in dimension 1 and greater), and corresponding definitions for their center and radius. Give necessary and sufficient conditions for them to exist (in terms of the barycentric coordinates, being signed versions of the inverses of the distances between vertices and opposite faces, having a nonzero sum) and show that they do always exist in the case of the incenter and of the excenter opposite a single vertex (the latter in dimensions 2 and greater), and that any point lying in the span of the vertices and equidistant from the faces opposite the vertices is an excenter (and, when signs of the equal distances are given, is the excenter with corresponding signs).
Some major pieces are deferred to followups, in particular definitions of touchpoints, tangency of exspheres and insphere to faces, and the relation to angle bisectors in various forms. But since the file is already over 600 lines, I think this is a reasonable starting point (and since the lemmas do show that the definitions have their characteristic properties of points being equidistant from the faces on the desired sides, I think it sufficiently justifies that the definitions are correct and usable as-is).
Feel free to golf; the calculations involved in showing that the excenter opposite a vertex always exists (in dimensions 2 and greater) are rather long.
---
[](https://gitpod.io/from-referrer/)
- [x] depends on: #23712
- [x] depends on: #23751
- [x] depends on: #24503 |
t-euclidean-geometry |
582/0 |
Mathlib.lean,Mathlib/Geometry/Euclidean/Incenter.lean |
2 |
26 |
['JovanGerb', 'eric-wieser', 'github-actions', 'jsm28', 'mathlib4-dependent-issues-bot'] |
nobody |
12-71902 12 days ago |
13-17593 13 days ago |
37-34439 37 days |
| 24245 |
JovanGerb author:JovanGerb |
feat(Geometry/Euclidean/SignedDist): `signedDist` between two points |
This PR defines `signedDist`, the signed distance between two points.
It redefines `signedInfDist` so that it uses `signedDist`.
The motivation is to use this in IMO2020Q6. Additionally this definition will be useful for properly reasoning about the power of a point
[#mathlib4 > Signed distance between points](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Signed.20distance.20between.20points)
some comments:
* should `signedDistLinear` be `private`?
* should `signedDist` and `signedInfDist` be made continuous bunled maps in this PR?
* I'm not too happy about the hypothesis in `signedDist_congr (h : ∃ r > (0 : ℝ), r • v = w)`. This relationship between `v` and `w` is a symmetric one that should have some API around it, similar to `SameRay`. It could also be spelled as `(ℝ≥0 ∙ v) = ℝ≥0 ∙ w`
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
206/23 |
Mathlib/Analysis/InnerProductSpace/Basic.lean,Mathlib/Geometry/Euclidean/SignedDist.lean,Mathlib/Topology/MetricSpace/Pseudo/Defs.lean |
3 |
1 |
['github-actions'] |
nobody |
12-40212 12 days ago |
12-40212 12 days ago |
23-56784 23 days |
| 24533 |
robertmaxton42 author:robertmaxton42 |
feat (ULift): conjugation by ULift.up/down, misc cast/heq lemmas |
* Adds the convenience def `ULift.conj x := `down (f (up x))`, and corresponding basic lemmas
* Adds lemmas showing that `ULift.up` and `.down` commute with casts and preserve `HEq`.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
31/0 |
Mathlib/Data/ULift.lean |
1 |
14 |
['eric-wieser', 'github-actions', 'robertmaxton42'] |
nobody |
12-35419 12 days ago |
12-35419 12 days ago |
12-43335 12 days |
| 24379 |
chrisflav author:chrisflav |
feat(Algebra/AlgHom): `Unique` if target is `Subsingleton` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
32/0 |
Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/Algebra/Hom.lean |
2 |
5 |
['chrisflav', 'eric-wieser', 'github-actions'] |
nobody |
12-25378 12 days ago |
13-25659 13 days ago |
13-61596 13 days |
| 21969 |
peabrainiac author:peabrainiac |
feat(Geometry/Diffeology): basics of diffeological spaces |
Introduces diffeological spaces, smooth maps between them, the D-topology and the standard diffeology on finite-dimensional normed spaces.
---
This is the first of hopefully many PRs upstreaming work that I have done on diffeological spaces in [my orbifolds repo](https://github.com/peabrainiac/lean-orbifolds), containing the first half of `Diffeology/Basic.lean`.
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
473/0 |
Mathlib.lean,Mathlib/Geometry/Diffeology/Basic.lean,docs/references.bib,scripts/noshake.json |
4 |
25 |
['github-actions', 'grunweg', 'leanprover-community-bot-assistant', 'lecopivo', 'peabrainiac'] |
nobody |
11-72255 11 days ago |
11-77317 11 days ago |
48-36072 48 days |
| 24266 |
plp127 author:plp127 |
feat(Order): `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)` |
Proves that `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)`, and also the dual theorem.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
14/0 |
Mathlib/Order/Directed.lean |
1 |
4 |
['github-actions', 'plp127', 'urkud'] |
nobody |
11-59985 11 days ago |
22-71366 22 days ago |
22-71350 22 days |
| 24514 |
b-mehta author:b-mehta |
chore(Int/GCD): use fuel in xgcd |
Modify the definition of xgcd to use fuel recursion, to allow it to be reduced in the kernel. As a consequence, this means the evaluation of field operations in ZMod p become provable by `rfl` and `decide`.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
44/22 |
Mathlib/Data/Int/GCD.lean |
1 |
3 |
['b-mehta', 'github-actions', 'nomeata', 'urkud'] |
nobody |
11-58624 11 days ago |
13-16361 13 days ago |
13-16414 13 days |
| 23498 |
Ruben-VandeVelde author:Ruben-VandeVelde |
chore(Topology.MetricSpace.Lipschitz): stop depending on Topology.Algebra |
Noticed while playing with the new `directoryDependency` linter. Not sure if these could be proved without assuming the continuity of real multiplication.
Copyright from https://github.com/leanprover-community/mathlib3/pull/1921 and https://github.com/leanprover-community/mathlib4/pull/11840.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
60/34 |
Mathlib.lean,Mathlib/Analysis/Normed/Group/AddTorsor.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Analysis/SpecialFunctions/Exp.lean,Mathlib/Topology/Algebra/MetricSpace/Lipschitz.lean,Mathlib/Topology/MetricSpace/Algebra.lean,Mathlib/Topology/MetricSpace/IsometricSMul.lean,Mathlib/Topology/MetricSpace/Lipschitz.lean,Mathlib/Topology/MetricSpace/PiNat.lean |
9 |
1 |
['github-actions'] |
nobody |
11-43122 11 days ago |
11-43122 11 days ago |
44-22846 44 days |
| 23360 |
kim-em author:kim-em |
chore: review of `erw` in `Algebra/Homology/DerivedCategory` |
|
t-algebra label:t-algebra$ |
21/15 |
Mathlib/Algebra/Homology/DerivedCategory/Basic.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean,Mathlib/Algebra/Homology/DerivedCategory/SingleTriangle.lean,Mathlib/Algebra/Homology/HomotopyCategory/SingleFunctors.lean,Mathlib/CategoryTheory/Shift/SingleFunctors.lean |
5 |
2 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
11-43110 11 days ago |
11-43110 11 days ago |
48-54578 48 days |
| 23676 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprime `induction'` for localizations and quotients |
All these removed instances of `induction'` generate only one subgoal. In some cases `obtain` can be used.
The relevant instances were identified by adding the following to `Mathlib.Tactic.Cases`
```diff
diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean
index 4a60db6c551..08c06520879 100644
--- a/Mathlib/Tactic/Cases.lean
+++ b/Mathlib/Tactic/Cases.lean
@@ -122,6 +122,16 @@ elab (name := induction') "induction' " tgts:(Parser.Tactic.elimTarget,+)
g.assign result.elimApp
let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
(generalized := fvarIds) (toClear := targetFVarIds) (toTag := toTag)
+ let body ← inferType targets[0]!
+ let names : Array Format := if withArg.1.getArgs.size > 1 then
+ (withArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+ let gens : Array Format := if genArg.1.getArgs.size > 1 then
+ (genArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+ let inductor : Format := if usingArg.1.getArgs.size > 1 then
+ Syntax.prettyPrint usingArg.1.getArgs[1]! else "~"
+ if subgoals.toList.length ≤ 1 then
+ logInfoAt tgts m!"{body.getAppFn.setPPExplicit true} {inductor} {gens} {names} \
+ {subgoals.toList.length}"
setGoals <| (subgoals ++ result.others).toList ++ gs
/-- The `cases'` tactic is similar to the `cases` tactic in Lean 4 core, but the syntax for giving
```
and then examining [the output](https://github.com/leanprover-community/mathlib4/actions/runs/14270845291/job/40003467676). |
tech debt |
94/113 |
Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Pointwise/Stabilizer.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Limits/Types/Colimits.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Finsupp/BigOperators.lean,Mathlib/Data/Fintype/Quotient.lean,Mathlib/Data/List/Cycle.lean,Mathlib/Data/Nat/ChineseRemainder.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/FieldTheory/RatFunc/Basic.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/GroupTheory/OreLocalization/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Concrete.lean,Mathlib/GroupTheory/Perm/Sign.lean,Mathlib/GroupTheory/Torsion.lean,Mathlib/RingTheory/OreLocalization/Basic.lean,Mathlib/RingTheory/OreLocalization/Ring.lean,Mathlib/SetTheory/Surreal/Basic.lean |
25 |
10 |
['Parcly-Taxel', 'apnelson1', 'eric-wieser', 'github-actions', 'grunweg', 'urkud'] |
nobody |
11-40574 11 days ago |
11-41617 11 days ago |
39-15937 39 days |
| 23394 |
BoltonBailey author:BoltonBailey |
chore(Data/Int/WithZero): fix erw |
---
Removing an `erw`. This is my first time doing this, so please tell me if I am doing something wrong here (e.g. should the new lemma be `simp`?).
[](https://gitpod.io/from-referrer/)
|
tech debt |
5/3 |
Mathlib/Algebra/Group/WithOne/Defs.lean,Mathlib/Algebra/GroupWithZero/WithZero.lean,Mathlib/Data/Int/WithZero.lean |
3 |
13 |
['BoltonBailey', 'Ruben-VandeVelde', 'eric-wieser', 'github-actions'] |
nobody |
11-13173 11 days ago |
11-42130 11 days ago |
27-29773 27 days |
| 24527 |
matthewjasper author:matthewjasper |
feat(Topology/Algebra/Module): Add more theorems for IsModuleTopology |
Add theorems that surjective linear maps to the module topology are open.
Add IsModuleTopology instance for quotients.
Add IsModuleTopology instance for finite dimensional T2 vector spaces over a complete normed field and use it to shorten some proofs.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
t-topology
label:t-algebra$ |
48/24 |
Mathlib/Topology/Algebra/Module/FiniteDimension.lean,Mathlib/Topology/Algebra/Module/ModuleTopology.lean |
2 |
5 |
['erdOne', 'github-actions', 'matthewjasper'] |
nobody |
11-10245 11 days ago |
11-27315 11 days ago |
12-82015 12 days |
| 24237 |
YaelDillies author:YaelDillies |
chore(Convex/Cone): move `ConvexCone` under `Geometry` |
This PR introduces a new folder under `Geometry` for convex geometry, and inside it a folder for convex cones.
Explain the purposes of both subfolders in contrast to the old ones.
Christen the new subfolders by moving `Analysis.Convex.Cone.Basic` to `Geometry.Convex.Cone.Basic`.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-analysis
|
85/11 |
Mathlib.lean,Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Analysis/Convex/Cone/InnerDual.lean,Mathlib/Analysis/Convex/Cone/README.md,Mathlib/Analysis/Convex/README.md,Mathlib/Geometry/Convex/Cone/Basic.lean,Mathlib/Geometry/Convex/Cone/README.md,Mathlib/Geometry/Convex/README.md,Mathlib/Tactic/Linter/DirectoryDependency.lean |
9 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
11-6091 11 days ago |
11-6107 11 days ago |
21-75108 21 days |
| 24546 |
jt496 author:jt496 |
feat(Combinatorics/SimpleGraph): add homOfConnectedComponents and related results |
Given homomorphisms of each connected component of `G : SimpleGraph α` into `H : SimpleGraph β `give the corresponding `G →g H`
Hence prove that G is n - colorable iff each connected component is n - colorable.
Also prove that G is 2-colorable iff it does not contain an odd length loop (closed walk).
I wasn't sure where to put this - it probably belongs in SimpleGraph.ConcreteColorings?
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
36/0 |
Mathlib/Combinatorics/SimpleGraph/Coloring.lean,Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean,Mathlib/Combinatorics/SimpleGraph/Path.lean |
3 |
3 |
['IvanRenison', 'github-actions', 'jt496'] |
nobody |
11-3708 11 days ago |
12-21775 12 days ago |
12-37286 12 days |
| 24567 |
joelriou author:joelriou |
feat(CategoryTheory): the shift functors on the localized category are linear |
If `L : C ⥤ D` is a localization functor with respect to `W : MorphismProperty C` and both `C` and `D` have been equipped with `R`-linear category structures such that `L` is `R`-linear and the shift functors on `C` are `R`-linear, then the shift functors on `D` are `R`-linear.
---
- [x] depends on: #24309
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
48/0 |
Mathlib.lean,Mathlib/CategoryTheory/Shift/Linear.lean |
2 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
10-81922 10 days ago |
10-81930 10 days ago |
10-81914 10 days |
| 24581 |
pechersky author:pechersky |
feat(Algebra/Group/Subgroup): map_top_of_mulEquivClass |
also remove simp from `map_to_of_surjective` because it doesn't fire even on this new lemma
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
7/1 |
Mathlib/Algebra/Group/Subgroup/Map.lean |
1 |
1 |
['github-actions'] |
nobody |
10-60819 10 days ago |
10-60874 10 days ago |
10-60869 10 days |
| 22231 |
pechersky author:pechersky |
feat(Algebra/Valued): `AdicExpansion` initial defns |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-topology
label:t-algebra$ |
299/0 |
Mathlib.lean,Mathlib/Topology/Algebra/Valued/AdicExpansion.lean |
2 |
2 |
['Thmoas-Guan', 'github-actions'] |
nobody |
10-56744 10 days ago |
79-58386 2 months ago |
79-58512 79 days |
| 24583 |
pechersky author:pechersky |
feat(GroupTheory/ArchimedeanDensely): type tag equivs on OrderMonoidIso |
and instantiate Unique using those
to prepare for unique order monoid iso
on mularchimedean discrete ordered groups
---
[](https://gitpod.io/from-referrer/)
|
t-order
t-algebra
label:t-algebra$ |
32/0 |
Mathlib/GroupTheory/ArchimedeanDensely.lean |
1 |
1 |
['github-actions'] |
nobody |
10-51115 10 days ago |
10-60333 10 days ago |
10-60327 10 days |
| 24590 |
smmercuri author:smmercuri |
chore: make `Valuation.Completion` a `def` and refactor more of `AdicValuation.lean` |
The main purpose of this PR is to resolve timeout issues encountered in FLT following the refactor of `HeightOneSpectrum.adicCompletion` to use the `WithVal` type synonym. The proposed fix in this PR is to replace `abbrev` with `def` in `Valuation.Completion`. Tested in FLT and this removes the timeout issue.
Also refactor as much API as possible from `HeightOneSpectrum.adicCompletion` to `Valuation.Completion`.
See #22488 for a previous attempt at fixing the problem.
---
[](https://gitpod.io/from-referrer/)
|
FLT |
162/81 |
Mathlib/NumberTheory/NumberField/FinitePlaces.lean,Mathlib/RingTheory/DedekindDomain/AdicValuation.lean,Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean,Mathlib/RingTheory/LaurentSeries.lean,Mathlib/Topology/Algebra/Valued/WithVal.lean |
5 |
4 |
['github-actions', 'leanprover-bot', 'smmercuri'] |
nobody |
10-24988 10 days ago |
10-25012 10 days ago |
10-24996 10 days |
| 24586 |
kebekus author:kebekus |
feat: introduce and discuss the leading coefficient of a meromorphic function |
Define the leading coefficient of a meromorphic function. If `f` is meromorphic at a point `x`, the leading coefficient is defined as the (unique!) value `g x` for a presentation of `f` in the form `(z - x) ^ order • g z` with `g` analytic at `x`. The lemma `leadCoefficient_eq_limit` expresses the leading coefficient as a limit.
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.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
251/0 |
Mathlib.lean,Mathlib/Analysis/Meromorphic/LeadCoefficient.lean |
2 |
1 |
['github-actions'] |
nobody |
9-46033 9 days ago |
10-46386 10 days ago |
10-46434 10 days |
| 23368 |
b-reinke author:b-reinke |
feat(GroupTheory/FreeGroup/ReducedWords): add theory of reduced words |
Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project.
This PR adds the file `GroupTheory/FreeGroup/ReducedWords.lean`, where the predicate of reduced words is defined. It is shown that `reduce` and `toWord` produce reduced words.
This is done in preparation for the theory of cyclically reduced words.
---
[](https://gitpod.io/from-referrer/)
|
t-geometric-group-theory
t-algebra
label:t-algebra$ |
109/0 |
Mathlib.lean,Mathlib/GroupTheory/FreeGroup/ReducedWords.lean |
2 |
28 |
['b-reinke', 'github-actions', 'vlad902'] |
nobody |
9-43485 9 days ago |
48-22705 1 month ago |
48-30536 48 days |
| 24480 |
mariainesdff author:mariainesdff |
feat(RingTheory/DividedPowers/SubPDIdeal): add SubDPIdeal |
Let `A` be a commutative (semi)ring and let `I` be an ideal of `A` with a divided power
structure `hI`. A subideal `J` of `I` is a *sub-dp-ideal* of `(I, hI)` if, for all `n ∈ ℕ > 0` and
all `x ∈ J`, `hI.dpow n x ∈ J`.
The "TODOs" listed on the file docstring have been formalized by the authors and will be added in subsequent PRs.
Co-authored-by: @AntoineChambert-Loir
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-number-theory
label:t-algebra$ |
387/0 |
Mathlib.lean,Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean |
2 |
1 |
['github-actions'] |
nobody |
9-33148 9 days ago |
14-13297 14 days ago |
14-13292 14 days |
| 23034 |
plp127 author:plp127 |
feat: `AddMonoidWithOne.toCharZero` |
This does not replace `StrictOrderedSemiring.toCharZero` to avoid looping with `NeZero.charZero_one`.
Requested by @vihdzp in [#Is there code for X? > OrderedAddCommGroup has CharZero](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/OrderedAddCommGroup.20has.20CharZero)
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
8/3 |
Mathlib/Algebra/Order/Ring/Defs.lean |
1 |
17 |
['eric-wieser', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-bot-assistant', 'leanprover-community-mathlib4-bot', 'plp127'] |
nobody |
9-29111 9 days ago |
30-5502 1 month ago |
53-81353 53 days |
| 24605 |
urkud author:urkud |
feat(CompactOpen): add basis of nhds of `ContinuousMap.const _ _` |
---
[](https://gitpod.io/from-referrer/) |
t-topology |
24/0 |
Mathlib/Topology/CompactOpen.lean |
1 |
1 |
['github-actions'] |
nobody |
9-16799 9 days ago |
9-16799 9 days ago |
9-16859 9 days |
| 22828 |
joelriou author:joelriou |
feat(CategoryTheory): parametrized adjunctions |
Given bifunctors `F : C₁ ⥤ C₂ ⥤ C₃` and `G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂`, this PR introduces adjunctions with a parameter `F ⊣₂ G`. In the case of closed monoidal categories, we obtain `curriedTensor C ⊣₂ internalHom`.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
152/0 |
Mathlib.lean,Mathlib/CategoryTheory/Adjunction/Parametrized.lean,Mathlib/CategoryTheory/Closed/Monoidal.lean |
3 |
8 |
['emilyriehl', 'erdOne', 'github-actions', 'joelriou', 'mckoen'] |
nobody |
9-8760 9 days ago |
17-6653 17 days ago |
64-12738 64 days |
| 24442 |
D-Thomine author:D-Thomine |
feat(Analysis/Asymptotics): add LinGrowth |
This new file is about the linear growth of sequences of extended real numbers, expressed using liminf and limsups.
The documentation, names, lemmas and their proofs are directly ported from Asymptotics.ExpGrowth. Some auxiliary lemmas in ExpGrowth are moved to LinGrowth.
ExpGrowthInf and ExpGrowthSup can be expressed using LinGrowthInf and LinGrowthSup. Any proof longer than four lines in ExpGrowth, and which has a linear equivalent, uses this strategy.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
687/261 |
Mathlib.lean,Mathlib/Analysis/Asymptotics/ExpGrowth.lean,Mathlib/Analysis/Asymptotics/LinearGrowth.lean,Mathlib/Order/BoundedOrder/Basic.lean |
4 |
4 |
['D-Thomine', 'github-actions', 'sgouezel'] |
nobody |
8-82580 8 days ago |
8-82580 8 days ago |
14-4136 14 days |
| 24139 |
yuanyi-350 author:yuanyi-350 |
feat: add `Fin.cycleIcc` which rotates `range(i, j)` |
In this file, I define permutation `cycleIcc i j hij`, which is the cycle `(i i+1 .... j)` leaving `(0 ... i-1)` and `(j+1 ... n-1)` unchanged. In other words, it rotates elements in `[i, j]` one step to the right. Also I prove some properties of `cycleIcc i j hij` such as it is a cycle and its cycleType is `j - i`
**This definition is used to prove the following result:**
```
theorem succAbove_comp_cycleIcc [NeZero n] (x : Fin (n + 1) → L) (i j : Fin (n + 1)) (eq : x i = x j) (lt : i < j)
x ∘ i.succAbove = x ∘ j.succAbove ∘ (cycleIcc hij)
```
More clearly, `x ∘ i.succAbove` and `x ∘ j.succAbove` are `Fin n → L` types. For example, when `n = 6, i = 2, j = 5` and `x i = x j`
```
x ∘ i.succAbove = (x 0, x 1, x 3, x 4, x 5, x 6)
x ∘ j.succAbove = (x 0, x 1, x 2, x 3, x 4, x 6)
```
We have
```
(x 0, x 1, x 3, x 4, x 5, x 6)
--(cycleIcc)--->(x 0, x 1, x 5, x 3, x 4, x 6) = (x 0, x 1, x 2, x 3, x 4, x 6)
```
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
132/1 |
Mathlib/Algebra/Group/Fin/Basic.lean,Mathlib/Data/Fin/Basic.lean,Mathlib/Data/Nat/SuccPred.lean,Mathlib/GroupTheory/Perm/Fin.lean |
4 |
26 |
['acmepjz', 'faenuccio', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mbkybky', 'yuanyi-350'] |
nobody |
8-58234 8 days ago |
12-66920 12 days ago |
26-81223 26 days |
| 22415 |
pechersky author:pechersky |
feat(Algebra/Order/Hom/Monoid): order iso versions of unitsWithZero and friends |
---
- [x] depends on: #22402
[](https://gitpod.io/from-referrer/)
|
t-order
t-algebra
label:t-algebra$ |
50/36 |
Mathlib/Algebra/GroupWithZero/WithZero.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean |
3 |
7 |
['faenuccio', 'github-actions', 'mathlib4-dependent-issues-bot', 'pechersky'] |
nobody |
8-49795 8 days ago |
10-51137 10 days ago |
37-8940 37 days |
| 23909 |
grunweg author:grunweg |
chore: various fixes for the flexible linter |
---
[](https://gitpod.io/from-referrer/)
|
|
117/83 |
Mathlib/Condensed/Light/Epi.lean,Mathlib/Control/EquivFunctor/Instances.lean,Mathlib/Control/Monad/Cont.lean,Mathlib/Data/FinEnum.lean,Mathlib/Data/Finsupp/MonomialOrder.lean,Mathlib/Data/List/Sigma.lean,Mathlib/Data/List/SplitBy.lean,Mathlib/Data/Matroid/Sum.lean,Mathlib/Data/Ordmap/Invariants.lean,Mathlib/Data/Real/Pi/Irrational.lean,Mathlib/Data/Seq/Parallel.lean,Mathlib/Data/Vector3.lean,Mathlib/Data/WSeq/Relation.lean,Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean,Mathlib/GroupTheory/CoprodI.lean,Mathlib/GroupTheory/Coxeter/Basic.lean,Mathlib/GroupTheory/Coxeter/Inversion.lean,Mathlib/GroupTheory/Goursat.lean,Mathlib/GroupTheory/HNNExtension.lean,Mathlib/GroupTheory/Nilpotent.lean,Mathlib/NumberTheory/Dioph.lean,Mathlib/NumberTheory/FLT/Polynomial.lean,Mathlib/NumberTheory/LSeries/Injectivity.lean,Mathlib/Probability/Kernel/Condexp.lean,Mathlib/RingTheory/Derivation/MapCoeffs.lean,Mathlib/RingTheory/Frobenius.lean,Mathlib/SetTheory/Ordinal/Notation.lean,Mathlib/SetTheory/ZFC/Rank.lean,Mathlib/Tactic/NormNum/NatFactorial.lean |
29 |
11 |
['b-mehta', 'github-actions', 'grunweg', 'jcommelin', 'leanprover-community-bot-assistant'] |
nobody |
8-13904 8 days ago |
8-13923 8 days ago |
33-11059 33 days |
| 21476 |
grunweg author:grunweg |
feat(lint-style): enable running on downstream projects |
Enable lint-style to run on downstream projects, by making the following modifications:
- allow passing an explicit list of libraries to lint: if nothing is passed, it lints `Mathlib`, `Archive` and `Counterexamples` (as before); otherwise, it lints precisely the passed modules
- only check init imports, undocumented scripts and the errors from `lint-style.py` when linting Mathlib
- make the style exceptions file configurable and optional: using the `nolints-file` flag, the exceptions file can be configured. If the flag is omitted, we try to find a file at `scripts/nolints-style.txt` --- and otherwise proceed with no style exceptions.
This means mathlib can continue unchanged, and downstream projects can either add an explicit exceptions file, or proceed without any exceptions.
After this PR, one should be able to run lint-style on a downstream project by `lake exe lint-style ProjectName`.
Prompted by [this zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/lint-style.20for.20downstream.20libraries).
---
(I did not test the last part.)
[](https://gitpod.io/from-referrer/)
|
t-linter |
58/19 |
Mathlib/Tactic/Linter/TextBased.lean,scripts/lint-style.lean |
2 |
17 |
['Vierkantor', 'adomani', 'github-actions', 'grunweg', 'joneugster'] |
joneugster assignee:joneugster |
8-11787 8 days ago |
22-26930 22 days ago |
41-28394 41 days |
| 24627 |
pechersky author:pechersky |
feat(Topology/Algebra/Valued): `IsLinearTopology 𝒪[K] 𝒪[K]` |
as well as
`IsDiscreteValuationRing 𝒪[ℚ_[p]]`
`IsLinearTopology ℤ_[p] ℤ_[p]`
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
129/0 |
Mathlib.lean,Mathlib/Topology/Algebra/Valued/LinearTopology.lean,Mathlib/Topology/Algebra/Valued/PadicLinearTopology.lean,Mathlib/Topology/Algebra/Valued/ValuedField.lean |
4 |
1 |
['github-actions'] |
nobody |
8-8810 8 days ago |
8-50243 8 days ago |
8-50294 8 days |
| 24492 |
Parcly-Taxel author:Parcly-Taxel |
chore: remove some adaptation notes |
|
tech debt |
15/32 |
Mathlib/Algebra/Homology/Single.lean,Mathlib/Combinatorics/Enumerative/DyckWord.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Int/Cast/Basic.lean,Mathlib/NumberTheory/DiophantineApproximation/Basic.lean |
5 |
12 |
['JovanGerb', 'Parcly-Taxel', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] |
nobody |
7-43505 7 days ago |
7-43521 7 days ago |
12-37780 12 days |
| 24361 |
Hagb author:Hagb |
feat(Data/Finsupp/MonomialOrder): `0 ≤ a` where `a : m.syn` |
`simp` would be able to solve it.
---
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
easy
|
3/0 |
Mathlib/Data/Finsupp/MonomialOrder.lean |
1 |
1 |
['github-actions'] |
nobody |
7-39412 7 days ago |
7-39412 7 days ago |
19-41089 19 days |
| 24236 |
YaelDillies author:YaelDillies |
feat: closed submodules |
Define closed `R`-submodules.
The plan is to redefine proper `R`-cones as closed `R≥0`-submodules.
From Toric
---
- [x] depends on: #24230
[](https://gitpod.io/from-referrer/)
|
toric
t-topology
|
180/0 |
Mathlib.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean |
2 |
14 |
['YaelDillies', 'b-mehta', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
7-38070 7 days ago |
7-38144 7 days ago |
19-72086 19 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 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 n H / n.choose 2` as `n` approaches `∞` exists,
- `extremalNumber n H` is asymptotically equivalent to `turanDensity H * n.choose 2` as `n` approaches `∞`.
---
- [x] depends on: #19865
- [x] depends on: #20681
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
182/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/TuranDensity.lean,Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Data/Sym/Sym2.lean |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
7-37448 7 days ago |
7-37492 7 days ago |
7-39487 7 days |
| 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 for `card α ≤ card β` on the vertex type `V` have at most `(card β-1)^(1/(card α))*(card V)^(2-1/(card α))/2 + (card V)*(card α-1)/2` edges.
---
- [x] depends on: #19865
- [x] depends on: #20738
I'd like to make `aux` not private in the `KovariSosTuran` namespace to enable reuse of the double-counting here, but I don't know what to call it.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
289/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/KovariSosTuran.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
7-35652 7 days ago |
15-66223 15 days ago |
15-66758 15 days |
| 22151 |
alreadydone author:alreadydone |
feat(RingTheory): a semiprimary ring is Noetherian/Artinian iff its Jacobson radical is fg |
A key fact used is `Module.FG.smul`: if `I` is a two-sided ideal of `R` that is f.g. as a left ideal and `N` is a f.g. `R`-module, then `I • M` is also a f.g. `R`-module.
Many lemmas about coprimality of ideals are also generalized to the noncommutative, two-sided setting.
---
- [x] depends on: #21904
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
215/155 |
Mathlib/Algebra/Algebra/Operations.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean,Mathlib/RingTheory/Extension.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/Finiteness/Ideal.lean,Mathlib/RingTheory/HopkinsLevitzki.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/Ideal/Operations.lean |
8 |
6 |
['alreadydone', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
7-33234 7 days ago |
7-33234 7 days ago |
71-6901 71 days |
| 24659 |
IvanRenison author:IvanRenison |
feat(Analysis/InnerProductSpace/Projection): add `Submodule.re_inner_orthogonalProjection_nonneg` |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
13/0 |
Mathlib/Analysis/InnerProductSpace/Projection.lean |
1 |
1 |
['github-actions'] |
nobody |
7-25569 7 days ago |
7-25570 7 days ago |
7-25634 7 days |
| 23760 |
xroblot author:xroblot |
feat(NumberField): define the `maximalRealSubfield` of a number field |
Define the `maximalRealSubfield` of a number field. It is a totally real subfield that contains all other totally real subfields.
Add also a couple of instances about the fact that subfields of a totally real field are totally real.
---
- [x] depends on: #24137
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
78/5 |
Mathlib/NumberTheory/NumberField/Basic.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean |
3 |
26 |
['faenuccio', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'xroblot'] |
faenuccio assignee:faenuccio |
7-14498 7 days ago |
8-28641 8 days ago |
15-24814 15 days |
| 24662 |
robin-carlier author:robin-carlier |
chore(CategoryTheory/Opposites): pseudofunctoriality of opposites |
We record lemmas dealing with pseudofunctoriality of the construction `C ↦ Cᵒᵖ`. More precisely, we give isomorphisms of the form `(F ⋙ G).op ≅ F.op ⋙ G.op`, and we study how they interact with constructions such as whiskering, unitors, and associators.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
206/0 |
Mathlib/CategoryTheory/Opposites.lean |
1 |
5 |
['github-actions', 'joelriou', 'robin-carlier'] |
nobody |
7-2481 7 days ago |
7-2481 7 days ago |
7-15398 7 days |
| 23923 |
YaelDillies author:YaelDillies |
feat: a discrete monoid has compact Pontryagin dual |
From LeanAPAP
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
47/10 |
Mathlib/Topology/Algebra/Group/CompactOpen.lean,Mathlib/Topology/Algebra/PontryaginDual.lean,Mathlib/Topology/CompactOpen.lean,Mathlib/Topology/ContinuousMap/Basic.lean,Mathlib/Topology/Separation/NotNormal.lean |
5 |
13 |
['YaelDillies', 'b-mehta', 'github-actions', 'urkud'] |
nobody |
6-67944 6 days ago |
11-5498 11 days ago |
32-42944 32 days |
| 24669 |
qawbecrdtey author:qawbecrdtey |
feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` |
---
[](https://gitpod.io/from-referrer/)
This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it.
```lean
def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E
```
|
t-analysis |
20/1 |
Mathlib/Analysis/Normed/Operator/LinearIsometry.lean |
1 |
1 |
['github-actions'] |
nobody |
6-53365 6 days ago |
6-53381 6 days ago |
6-53435 6 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
---
[](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 |
7 |
['Paul-Lez', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'ocfnash', 'xyzw12345'] |
ocfnash assignee:ocfnash |
6-43858 6 days ago |
42-48439 1 month ago |
43-80227 43 days |
| 22464 |
adomani author:adomani |
feat(CI): declarations diff in Lean |
Rewrites the `declaration_diff` script in Lean.
You can see the effect of the new script in the testing branch #22497.
The new CI step runs in approximately 5mins, but is separate from the `build` step.
---
[](https://gitpod.io/from-referrer/)
|
CI |
151/0 |
.github/workflows/PR_summary_lean.yml,scripts/README.md,scripts/declarations_diff.lean,scripts/declarations_diff_lean_shell_glue.sh |
4 |
6 |
['bryangingechen', 'github-actions', 'grunweg'] |
robertylewis assignee:robertylewis |
6-43682 6 days ago |
71-7927 2 months ago |
71-7917 71 days |
| 24172 |
LessnessRandomness author:LessnessRandomness |
feat: specialize rational root theorem to usual rational numbers and integers |
Rational root theorem and integral root theorem - the special case for usual rational numbers and integers.
--- |
new-contributor
t-algebra
label:t-algebra$ |
123/0 |
Mathlib.lean,Mathlib/RingTheory/Polynomial/OfRationalNumbers/RationalRootTheorem.lean |
2 |
2 |
['github-actions', 'grunweg'] |
mariainesdff assignee:mariainesdff |
6-43415 6 days ago |
26-11098 26 days ago |
26-11152 26 days |
| 23413 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Join): Pseudofunctoriality of joins of categories |
Promote the constructions `C ↦ C ⋆ D` and `D ↦ C ⋆ D` to pseudofunctors from `Cat` to `Cat`. The construction is carried in a new file `CategoryTheory/Join/Pseudofunctor.lean` to reduce imports.
---
- [x] depends on: #23412
The pseudofunctoriality statements here are not the most general. The "right" statements would be
1) "pseudobifunctoriality".
2) pseudofunctoriality with values in slice bicategories.
Unfortunately, the two-categorical machinery in mathlib is not advanced enough yet to even make sense of the statements (first would require at least product bicategories, or 2-categories of pseudofunctors for a curried version, second would require slice bicategories.).
The content of this file should be upgraded once said constructions in bicategories are available, but for now I want at least to have statements that recover what we already have for `WithInitial` and `WithTerminal` rather than conditioning everything on a (probably rather long) bicategorical sidequest.
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
169/0 |
Mathlib.lean,Mathlib/CategoryTheory/Join/Basic.lean,Mathlib/CategoryTheory/Join/Pseudofunctor.lean |
3 |
9 |
['github-actions', 'joelriou', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'robin-carlier'] |
nobody |
6-41853 6 days ago |
6-41853 6 days ago |
25-19326 25 days |
| 22933 |
chrisflav author:chrisflav |
feat(RingTheory/LocalProperties): constructor for `RingHom.OfLocalizationSpan` |
Adds a constructor for `RingHom.OfLocalizationSpan` where `P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))` has to be shown for a covering family. This is convenient in practice, because the base change API is the more generally applicable framework.
-- -
I think the import increase is fine, but if people are not happy with it, I can instead make a new file `Mathlib.RingTheory.LocalizationAway.BaseChange`.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
102/3 |
Mathlib/Algebra/Algebra/Basic.lean,Mathlib/RingTheory/LocalProperties/Basic.lean,Mathlib/RingTheory/Localization/BaseChange.lean |
3 |
8 |
['chrisflav', 'erdOne', 'github-actions'] |
nobody |
6-37030 6 days ago |
6-70771 6 days ago |
61-2990 61 days |
| 22085 |
IvanRenison author:IvanRenison |
feat(Combinatorics/SimpleGraph): introduce `ConnectedComponent.toSimpleGraph` |
---
I don't know if `ConnectedComponent.Graph` is the best name for this
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
72/32 |
Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Path.lean |
2 |
16 |
['IvanRenison', 'github-actions', 'leanprover-community-bot-assistant', 'pimotte'] |
b-mehta assignee:b-mehta |
6-23266 6 days ago |
26-31693 26 days ago |
74-25009 74 days |
| 22792 |
madvorak author:madvorak |
feat(Mathlib/Data/Fin/Pigeonhole): pigeonhole-like results for Fin |
Consider the following settings:
```
import Mathlib
example (X Y : Type) [Fintype X] [Fintype Y] (f : X → Y) (hf : f.Injective) :
Fintype.card X ≤ Fintype.card Y := by
hint
example (m n : ℕ) (f : Fin m → Fin n) (hf : f.Injective) :
m ≤ n := by
hint
example (X Y : Type) [Fintype X] [Fintype Y] (f : X ↪ Y) :
Fintype.card X ≤ Fintype.card Y := by
hint
example (m n : ℕ) (f : Fin m ↪ Fin n) :
m ≤ n := by
hint
```
The 1st and 3rd `hint` succeed, but the 2nd a 4th `hint` fail.
The problem is obviously that `exact?` does not see through `Fintype.card (Fin n) = n` when searching for appropriate lemma.
It may seem to not be a problem, as it will rarely derail experienced Mathlib users — after all, experienced Leaners usually go directly for the `Finset` or `Fintype` version.
However, beginners frequently work with `Fin` and they will expect stuff like
```
theorem le_of_injective (f : Fin m → Fin n) (hf : f.Injective) : m ≤ n
```
to exist; therefore, when `hint` or `exact?` fails, it is a very unpleasant surprise.
This PR addressed this issue; not to provide useful content for advanced users, but to make Mathlib more useful for beginners.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
38/0 |
Mathlib.lean,Mathlib/Data/Fin/Pigeonhole.lean |
2 |
1 |
['github-actions'] |
ericrbg assignee:ericrbg |
6-23232 6 days ago |
65-12983 2 months ago |
65-13034 65 days |
| 23758 |
erdOne author:erdOne |
feat(Topology/Algebra): linearly topologized iff non-archimedian |
...for topological modules over compact rings or `ℤ`-finite rings
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
t-topology
label:t-algebra$ |
138/3 |
Mathlib/LinearAlgebra/Span/Basic.lean,Mathlib/Topology/Algebra/LinearTopology.lean |
2 |
21 |
['ADedecker', 'AntoineChambert-Loir', 'erdOne', 'github-actions', 'grunweg'] |
ADedecker and AntoineChambert-Loir assignee:AntoineChambert-Loir assignee:ADedecker |
6-23154 6 days ago |
26-81998 26 days ago |
37-44416 37 days |
| 23826 |
javra author:javra |
feat(CategoryTheory): linear categories as `ModuleCat R`-enriched categories |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-category-theory
|
195/0 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean,Mathlib/CategoryTheory/Enriched/Linear.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/CategoryTheory/Monoidal/Linear.lean |
5 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
TwoFX assignee:TwoFX |
6-23138 6 days ago |
30-33572 1 month ago |
30-33555 30 days |
| 21103 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialSet): uniqueness of the decomposition involving non-degenerate simplices |
Any simplex `x : X _⦋n⦌` of a simplicial set can be written in a unique way as `X.map f.op y` for an epimorphism `f : ⦋n⦌ ⟶ ⦋m⦌` and a non-degenerate `m`-simplex `y`.
---
- [x] depends on: #21098
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
118/5 |
Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean |
2 |
4 |
['gio256', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
dagurtomas assignee:dagurtomas |
6-20524 6 days ago |
25-80429 25 days ago |
64-25633 64 days |
| 21745 |
robin-carlier author:robin-carlier |
feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_σ`s |
We prove that admissible lists indeed provide a normal form for morphisms of satisfying `P_σ`.
To this end, we introduce `standardσ`, a construction that takes a list and turn it into a composition of `σ i`s in `SimplexCategoryGenRel`. We then prove that, thangs to the fifth simplicial identity, composition on the right corresponds to simplicial insertion in the list. This gives existence of a normal form for every morphism satisfying `P_σ`.
For unicity, we introduce an auxiliary function `simplicialEvalσ : (List ℕ) → ℕ → ℕ` and show that for admissible lists, it lifts to `ℕ` the `orderHom` attached to `toSimplexCategory.map standardσ`, and that we can recover elements of the list only by looking at values of this function.
Part of a series of PR formalising that `SimplexCategoryGenRel` is equivalent to `SimplexCategory`.
---
- [ ] depends on: #21744
[](https://gitpod.io/from-referrer/)
|
large-import
t-topology
t-category-theory
|
286/7 |
Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
dagurtomas assignee:dagurtomas |
6-20511 6 days ago |
23-5791 23 days ago |
23-7314 23 days |
| 23502 |
Timeroot author:Timeroot |
feat(ModelTheory/Semantics): BoundedFormula.realize_foldr_imp |
Two lemmas for `realize`ing a `BoundedFormula`.
---
Pulled out from #19695.
[](https://gitpod.io/from-referrer/)
|
t-logic |
20/0 |
Mathlib/ModelTheory/Semantics.lean,Mathlib/ModelTheory/Syntax.lean |
2 |
1 |
['github-actions'] |
fpvandoorn assignee:fpvandoorn |
6-20323 6 days ago |
44-13496 1 month ago |
44-13548 44 days |
| 23365 |
vasnesterov author:vasnesterov |
feat(Tactic/Simproc): nested quantifiers in `existsAndEq` |
Generalize the `existsAndEq` simproc to nested existential quantifiers.
For example `∃ a, p a ∧ ∃ b, a = f b ∧ q b` now simplifies to `∃ b, p (f b) ∧ q b`.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
440/73 |
Mathlib/Tactic/Simproc/ExistsAndEq.lean,MathlibTest/Simproc/ExistsAndEq.lean |
2 |
40 |
['JovanGerb', 'b-mehta', 'eric-wieser', 'github-actions', 'kim-em', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'vasnesterov'] |
joneugster assignee:joneugster |
6-16860 6 days ago |
41-70964 1 month ago |
47-11206 47 days |
| 24054 |
plp127 author:plp127 |
feat(Topology): R1 spaces are quasisober |
This generalizes `T2Space.quasiSober`
---
- [ ] depends on: #24098
[](https://gitpod.io/from-referrer/)
|
t-topology |
36/8 |
Mathlib/Topology/Separation/Basic.lean,Mathlib/Topology/Separation/Hausdorff.lean,Mathlib/Topology/Sober.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'urkud'] |
urkud assignee:urkud |
6-16645 6 days ago |
21-6808 21 days ago |
22-16858 22 days |
| 24657 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Join): Opposites of joins of categories |
Record the equivalence `(C ⋆ D)ᵒᵖ ≌ Dᵒᵖ ⋆ Cᵒᵖ` and characterize both of its directions with respect to the left/right inclusions.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
152/0 |
Mathlib.lean,Mathlib/CategoryTheory/Join/Opposites.lean |
2 |
8 |
['b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'robin-carlier'] |
nobody |
6-14211 6 days ago |
6-14211 6 days ago |
6-61301 6 days |
| 24690 |
ScottCarnahan author:ScottCarnahan |
feat (Data.Prod): Reverse lexicographic order |
This PR implements the type synonym RevLex as a one-field structure, defines an order on products, and proves an order isomorphism with the Lex product with factors switched.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
141/0 |
Mathlib.lean,Mathlib/Data/Prod/RevLex.lean |
2 |
1 |
['github-actions'] |
nobody |
6-6292 6 days ago |
6-6355 6 days ago |
6-6340 6 days |
| 20704 |
winstonyin author:winstonyin |
feat: existence of local flows of vector fields |
I formalise the existence theorem for local flows of time-dependent vector fields (`IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt`). Currently, if we wish to show the existence of a family of integral curves indexed by their initial conditions, it is necessary to prove the hypotheses of the vector field (Lipschitz continuity within a closed ball, etc.), centred around each of these initial conditions. I have refactored the current proof of the Picard-Lindelöf theorem to allow the initial point to be different from the point about which the hypotheses on the vector field are stated. This way, integral curves and flows are treated on equal footing.
Credits going to the original author @urkud, I have completely rewritten the file to accommodate different design choices. Many of the proof steps are nevertheless inspired by Yury's formalisation.
* The `PicardLindelof` data structure is removed entirely. It merely bundles the non-Prop arguments into itself. Although it simplifies the assumptions in subsequent proofs, it obscures the (in)dependence on the relevant constants in the type description of theorems. Since `IsPicardLindelof` is already a public facing structure, we should also simply use it internally, without any loss.
* In particular, I remove the completely superficial dependence of `FunSpace` on the `PicardLindelof` structure.
* `FunSpace` no longer specifies the initial condition. It only needs the initial point to lie in a closed ball (which will be the domain of the local flow).
* I avoid defining new non-Prop things that are only used in the proof steps, such as the current `vComp` and `tDist`. The proofs are a little longer as a result, but they are also more readable.
* I place all private (i.e. only internally used) theorems under the namespace `FunSpace`, to guide users to the proper theorems in the public API.
This is part of my effort to show that the solution to an ODE depends smoothly on the initial condition, or on parameters of the ODE. This is in turn needed for many results about manifolds, such as the fact that $C^1$ vector fields on compact manifolds always have global integral curves (or global flows).
I especially welcome any suggestions to rename lemmas or define new structures to simplify the statements.
I'm happy to write up the proof in LaTeX as well, if it's going to help reviewers.
- [x] depends on: #20696
- [x] depends on: #20731
---
[](https://gitpod.io/from-referrer/)
|
t-dynamics
t-analysis
|
562/360 |
Mathlib/Algebra/Order/Group/Abs.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/ODE/PicardLindelof.lean,Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean,docs/1000.yaml,docs/undergrad.yaml |
6 |
7 |
['github-actions', 'grunweg', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'michaellee94', 'winstonyin'] |
grunweg assignee:grunweg |
6-3144 6 days ago |
8-7199 8 days ago |
57-51090 57 days |
| 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)
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
28/0 |
Mathlib/LinearAlgebra/Span/Basic.lean |
1 |
21 |
['Paul-Lez', 'Raph-DG', 'github-actions', 'j-loreaux', 'mattrobball'] |
mattrobball assignee:mattrobball |
5-81834 5 days ago |
50-14789 1 month ago |
83-86286 83 days |
| 24691 |
eric-wieser author:eric-wieser |
feat: more `NormSMulClass` instances |
This adds instances for `ProdLp`, `PiLp`, and matrix norms.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
53/1 |
Mathlib/Analysis/Matrix.lean,Mathlib/Analysis/Normed/Lp/PiLp.lean,Mathlib/Analysis/Normed/Lp/ProdLp.lean,Mathlib/Analysis/Normed/MulAction.lean |
4 |
11 |
['copilot-pull-request-reviewer', 'eric-wieser', 'github-actions', 'loefflerd'] |
nobody |
5-81340 5 days ago |
6-5721 6 days ago |
6-5770 6 days |
| 23969 |
grunweg author:grunweg |
feat: add LinearEquiv.ofInjectiveOfFinrankEq |
This is used in #22611.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
20/0 |
Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean |
1 |
7 |
['eric-wieser', 'github-actions', 'grunweg'] |
eric-wieser assignee:eric-wieser |
5-75012 5 days ago |
32-30461 1 month ago |
32-30514 32 days |
| 23678 |
plp127 author:plp127 |
feat: recursor for nonempty lists |
Adds `List.recNeNil` and `List.recOnNeNil` for motives that depend on the list being nonempty. Taken from [Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/accessing.20the.20source.20case.20during.20induction/near/502101211).
---
[](https://gitpod.io/from-referrer/)
|
t-data |
40/0 |
Mathlib/Data/List/Induction.lean |
1 |
6 |
['eric-wieser', 'github-actions', 'plp127'] |
ericrbg assignee:ericrbg |
5-72797 5 days ago |
39-85434 1 month ago |
39-85486 39 days |
| 23930 |
Vtec234 author:Vtec234 |
feat(Tactic): dependent rewriting |
Add dependent rewrite tactics `rw!` and `rewrite!`.
These operate by inserting casts in front of terms that would otherwise become type-incorrect after the rewrite.
In the default mode, only proof terms are casted, so that (by proof irrelevance) no observable complexity is added.
In the most liberal mode, the tactics never encounter the 'motive is not type correct' error,
but may add casts that make the goal or other term very complex.
Co-authored-by: Aaron Liu
---
This has been discussed on Zulip [here](https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/dependent.20rewrite.20tactic/with/504228516). See the included test file for example rewrites that this tactic can do.
[](https://gitpod.io/from-referrer/)
|
t-meta |
706/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/DepRewrite.lean,MathlibTest/depRewrite.lean |
4 |
1 |
['github-actions'] |
adamtopaz assignee:adamtopaz |
5-72666 5 days ago |
33-67237 1 month ago |
33-67286 33 days |
| 24358 |
urkud author:urkud |
feat(BigOperators/Fin): lemmas about summation over intervals |
Add lemmas about sums over `Fin.Icc (Fin.castLE h a) (Fin.castLE h b)` etc.
For `Fin.castAdd`, `Fin.castSucc`, and `Fin.cast`, the set is incomplete,
but the missing lemmas will require additions to other files.
Also fix the RHS in some recently added lemmas about `Finset.map`
and intervals.
---
I'm not sure which of the new lemmas should be `@[simp]`.
- [x] depends on: #24197
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
243/19 |
Mathlib/Algebra/BigOperators/Fin.lean,Mathlib/Order/Interval/Finset/Fin.lean |
2 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
5-65014 5 days ago |
11-43194 11 days ago |
13-24747 13 days |
| 24685 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Limits/Preserves): Preservations of (co)limits by bifunctors |
Introduce a typeclass `PreservesColimit₂` that bundles the assumption that a bifunctor preserves a pair of colimit diagrams in each of its variables. This is stated in terms of a construction `Functor.mapCocone₂` that applies a bifunctor `G` to a pair of cocones to get a cocone over the uncurryfication of `whiskeringLeft₂ _|>.obj _|>.obj _|>.obj G`. The cocone points of this construction is definitionally the evaluation of `G` at the cocone points of the two cocones given as parameters.
We give helper functions to extract isomorphisms with abstract colimits out of this typeclass, and we characterize these isomorphisms with respect to the canonical maps to the colimits.
The dual typeclass for limits is also introduced.
---
The definition of `Functor.mapCocone₂` and of `PreservesColimit₂` is due to @joelriou and was suggested during review of #17781.
This PR only contains basic definitions, but does not give any interesting ways of inferring a `PreservesColimit₂` instance.
This will be the content of a follow-up PR.
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
243/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Preserves/Bifunctor.lean |
2 |
1 |
['github-actions'] |
nobody |
5-51394 5 days ago |
6-12830 6 days ago |
6-12885 6 days |
| 22420 |
pechersky author:pechersky |
feat(Order/Prod/Lex/{Hom,Monoid,GroupWithZero}): ordered inclusions and projections of prod of ordered groups |
---
- [x] depends on: #22402
[](https://gitpod.io/from-referrer/)
|
t-order
t-algebra
label:t-algebra$ |
256/0 |
Mathlib.lean,Mathlib/Order/Prod/Lex/GroupWithZero.lean,Mathlib/Order/Prod/Lex/Hom.lean,Mathlib/Order/Prod/Lex/Monoid.lean |
4 |
15 |
['YaelDillies', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'pechersky'] |
YaelDillies assignee:YaelDillies |
5-43178 5 days ago |
37-8709 1 month ago |
37-10501 37 days |
| 24703 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal): external product of diagrams in monoidal categories |
Given functors `K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C` with values in a monoidal category, define a construction `externalProduct K₁ K₂` (denoted `K₁ ⊠ K₂`) as the bifunctor `(j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂`.
We show that composition of this construction with the diagonal functor to the product recovers the pointwise tensor product of functors, and we show that this construction satisfies a symmetry whenever `C` is braided.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
99/0 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/ExternalProduct.lean |
2 |
1 |
['github-actions'] |
nobody |
5-36408 5 days ago |
5-37006 5 days ago |
5-36991 5 days |
| 8167 |
sebzim4500 author:sebzim4500 |
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₃
```
[](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 |
5-27195 5 days ago |
67-1639 2 months ago |
97-50288 97 days |
| 21182 |
joneugster author:joneugster |
fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace |
Currently the `#count_heartbeat` linter reported the heartbeats until it concluded `error: [declaration] has already been declared` instead of re-elaborating the declaration.
---
[Zulip report](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/count_heartbeats.20for.20all.20declarations.20in.20a.20file.3F/near/496303652)
[](https://gitpod.io/from-referrer/)
|
t-meta |
72/5 |
Mathlib/Util/CountHeartbeats.lean,MathlibTest/CountHeartbeats.lean |
2 |
16 |
['adomani', 'github-actions', 'joneugster', 'mathlib-bors'] |
adomani assignee:adomani |
5-27125 5 days ago |
42-20779 1 month ago |
44-54180 44 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>
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
|
816/2 |
Mathlib.lean,Mathlib/Algebra/Lie/Derivation/AdjointAction.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 |
8 |
16 |
['bryangingechen', 'eric-wieser', 'faenuccio', 'github-actions', 'grunweg', 'ocfnash', 'siddhartha-gadgil', 'xyzw12345'] |
robertylewis assignee:robertylewis |
5-27017 5 days ago |
80-58516 2 months ago |
80-58508 80 days |
| 22794 |
vasnesterov author:vasnesterov |
feat(Tactic/NormNum): `norm_num` extension for `Irrational x^y` |
Add `norm_num` extension for `Irrational x^y`.
---
I don't disprove `Irrational x^y` when `x^y` is, in fact, rational here, because I hope in the future `norm_num` will be able to simplify such expressions to their rational representations (e.g. `(8/27)^(2/3) --> 4/9`), and then apply `Rat.not_irrational`.
[](https://gitpod.io/from-referrer/)
|
t-meta |
446/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/NormNum/Irrational.lean,MathlibTest/norm_num_ext.lean,scripts/noshake.json |
5 |
1 |
['github-actions'] |
dwrensha assignee:dwrensha |
5-26991 5 days ago |
59-70774 1 month ago |
64-71310 64 days |
| 24036 |
Louddy author:Louddy |
feat: add `HeightOneSpectrum.ofPrime` |
Add a definition relating elements of type `HeightOneSpectrum R` with the (nonzero) prime elements of the monoid with zero `Ideal R`. (Note the distinction between `Prime` and `Ideal.IsPrime`).
The documentation string is inspired from [Ideal.prime_iff_isPrime](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/DedekindDomain/Ideal.html#Ideal.prime_iff_isPrime).
This was discussed [#mathlib4 > Placing a definition in `DedekindDomain.Ideal` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Placing.20a.20definition.20in.20.60DedekindDomain.2EIdeal.60/near/511647129).
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
11/1 |
Mathlib/RingTheory/DedekindDomain/Ideal.lean |
1 |
5 |
['Louddy', 'Ruben-VandeVelde', 'github-actions'] |
Ruben-VandeVelde assignee:Ruben-VandeVelde |
5-25144 5 days ago |
30-26414 1 month ago |
30-26468 30 days |
| 11563 |
YaelDillies author:YaelDillies |
feat: `∑ i ∈ s with hi : p i, f i hi` syntax for big operators |
Define new notation for `Finset.sum`/`Finset.prod`. `∑ i ∈ s with hi : p i, f i hi` now is notation for `∑ i : s.filter p, f i.1 (mem_filter.1 i.2).2`.
---
- [x] depends on: #6795
Other notations we could have are
* `∑ hi : i ∈ s, f i hi` as notation for `∑ i : s, f i.1 i.2`
* `∑ hi : i ∈ s with p i, f i hi` as notation for `∑ i : s.filter p, f i.1 (mem_filter.1 i.2).1`
* `∑ hi : i ∈ s with hpi : p i, f i hi hpi` as notation for `∑ i : s.filter p, f i.1 (mem_filter.1 i.2).1 (mem_filter.1 i.2).2`
but Eric seems mildly unhappy about them.
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-meta
label:t-algebra$ |
27/18 |
Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean |
1 |
27 |
['YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'kbuzzard', 'kmill', 'leanprover-community-mathlib4-bot'] |
kmill assignee:kmill |
5-25057 5 days ago |
51-86131 1 month ago |
100-19420 100 days |
| 23849 |
chrisflav author:chrisflav |
feat(Data/Set): add `Set.encard_iUnion` |
---
[](https://gitpod.io/from-referrer/)
|
t-data |
65/0 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Card/Arithmetic.lean,Mathlib/Data/Set/Finite/Lattice.lean |
3 |
11 |
['YaelDillies', 'chrisflav', 'github-actions'] |
YaelDillies assignee:YaelDillies |
5-22708 5 days ago |
5-22708 5 days ago |
35-51500 35 days |
| 22089 |
sgouezel author:sgouezel |
feat: composing a continuous multilinear map with continuous linear maps is analytic in both variables |
Also prove that the composition of continuously polynomial functions is continuously polynomial.
---
- [x] depends on: #22102
- [x] depends on: #22789
[](https://gitpod.io/from-referrer/)
|
t-analysis |
277/80 |
Mathlib/Analysis/Analytic/CPolynomial.lean,Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Data/Multiset/DershowitzManna.lean,Mathlib/Order/KrullDimension.lean |
5 |
9 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'sgouezel', 'urkud'] |
loefflerd assignee:loefflerd |
5-20064 5 days ago |
43-1517 1 month ago |
81-54465 81 days |
| 24712 |
scholzhannah author:scholzhannah |
refactor: change `CWComplex` from `abbrev` to its own `class` |
This PR makes the classical absolute CW complex into its own class. This is done to make typeclass inference behave nicer and to give `CWComplex` a constructor.
Co-authored-by: Floris van Doorn
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
65/30 |
Mathlib/Topology/CWComplex/Classical/Basic.lean,Mathlib/Topology/CWComplex/Classical/Finite.lean |
2 |
1 |
['github-actions'] |
nobody |
5-19185 5 days ago |
5-21167 5 days ago |
5-21217 5 days |
| 24715 |
scholzhannah author:scholzhannah |
refactor: reorder Topology/CWComplex/Classical/Basic.lean |
This PR reorders the file Topology/CWComplex/Classical/Basic.lean. This is to prepare for the addition of the notion of subcomplexes which will require turning `skeleton` and `skeletonLT` into a subcomplex.
Co-authored-by: Floris van Doorn
---
The reordering requires changing the proof of the following lemmas:
- `RelCWComplex.closedCell_subset_complex`
- `RelCWComplex.openCell_subset_complex`
- `RelCWComplex.base_subset_complex`
- `RelCWComplex.union_iUnion_openCell_eq_complex`
- `RelCWComplex.iUnion_openCell_eq_skeletonLT`
And the addition of:
- `RelCWComplex.iUnion_openCell_eq_iUnion_closedCell`
[](https://gitpod.io/from-referrer/)
|
t-topology |
226/214 |
Mathlib/Topology/CWComplex/Classical/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
5-18413 5 days ago |
5-18413 5 days ago |
5-18469 5 days |
| 23320 |
Whysoserioushah author:Whysoserioushah |
feat(Mathlib/RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum |
co-authored by: @jjaassoonn
---
splited from [#23216](https://github.com/leanprover-community/mathlib4/pull/23216) following @eric-wieser advice
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
81/0 |
Mathlib.lean,Mathlib/RingTheory/TwoSidedIdeal/SpanAsSum.lean |
2 |
43 |
['Paul-Lez', 'Whysoserioushah', 'eric-wieser', 'github-actions', 'kbuzzard'] |
eric-wieser assignee:eric-wieser |
5-17942 5 days ago |
49-70386 1 month ago |
49-70431 49 days |
| 24702 |
joneugster author:joneugster |
fix(CI): publish gitpod docker image to ghcr.io |
Fix for workflow introduced in #23844, #24694, and #24698.
The docker images are published at https://github.com/orgs/leanprover-community/packages?repo_name=mathlib4
---
**Notes for reviewer**:
- You can see the action by pushing any commit to this PR or by running it manually at https://github.com/leanprover-community/mathlib4/actions/workflows/docker_build.yml (choose branch `eugster/fix-docker-build`)
- I haven't validated the created images are usable, maybe somebody could download them and create a container?
- [ ] **maintainer**: Could somebody please delete all packages at https://github.com/orgs/leanprover-community/packages?repo_name=mathlib4 which have been created acccidentially during testing
- [ ] **maintainer**: The packages `gitpod`, `lean`, and `gitpod-blueprint` at https://github.com/orgs/leanprover-community/packages?repo_name=mathlib4 should be made public. I think this is done through the github UI
- [ ] revert the `on:` part below to a schedule before merging (see below)
[](https://gitpod.io/from-referrer/)
|
CI |
42/42 |
.github/workflows/docker_build.yml |
1 |
11 |
['YaelDillies', 'bryangingechen', 'github-actions', 'joneugster', 'pechersky'] |
bryangingechen assignee:bryangingechen |
5-15389 5 days ago |
5-26377 5 days ago |
5-26489 5 days |
| 24648 |
Hagb author:Hagb |
feat(LinearAlgebra/Span/Defs): add `subset_span_finite_of_subset_span` |
Given finite subset `t` of span of a set `s`, there exists a finite subset `T` of the `s` such that `t` is a subset of span of `T`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
12/0 |
Mathlib/LinearAlgebra/Span/Defs.lean |
1 |
4 |
['Hagb', 'erdOne', 'github-actions'] |
nobody |
5-9455 5 days ago |
7-42057 7 days ago |
7-42108 7 days |
| 23601 |
YaelDillies author:YaelDillies |
feat(CommAlgCat): the category of commutative algebras |
Define the category of commutative `R`-algebras. This is the same as `Under R` up to two details:
* `A : CommAlg R` contains the data of both `algebraMap R A : R → A` and `Algebra.smul : R → A → A`. `A : Under R` only contains `algebraMap R A`, meaning that going back and forth between `Under R` and unbundled algebras is painful/nigh impossible.
* If `A : Under R`, then `A` must live in the same universe as `R`
From Toric, FLT
Co-authored-by: Andrew Yang
Co-authored-by: Michał Mrugała
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
toric
FLT
t-algebra
label:t-algebra$ |
185/0 |
Mathlib.lean,Mathlib/Algebra/Category/CommAlgCat/Basic.lean |
2 |
27 |
['Kiolt', 'YaelDillies', 'b-mehta', 'erdOne', 'eric-wieser', 'github-actions'] |
nobody |
5-6705 5 days ago |
5-30449 5 days ago |
19-36285 19 days |
| 24213 |
BoltonBailey author:BoltonBailey |
feat: add simp lemmas for trig functions on `π * 2⁻¹` |
This PR adds a number of simp lemmas to reduce trig functions evaluated on `π * 2⁻¹`. This allows `simp` to reduce expressions such as `sin (π * (1 / 2))`
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
45/0 |
Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean |
1 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
5-6160 5 days ago |
5-6182 5 days ago |
23-63574 23 days |
| 24692 |
ScottCarnahan author:ScottCarnahan |
feat (RingTheory/HahnSeries/Basic): isomorphism of Hahn series induced by order isomorphism |
This PR introduces an isomorphism of Hahn series induced by an order isomorphism on the exponent posets.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
29/0 |
Mathlib/RingTheory/HahnSeries/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
5-639 5 days ago |
6-5042 6 days ago |
6-5027 6 days |
| 22651 |
101damnations author:101damnations |
feat(RepresentationTheory/*): subrepresentations, quotients by subrepresentations, and representations of quotient groups |
Given a `G`-representation `(V, ρ)` and a `G`-invariant submodule `W ≤ V`, this PR defines the restriction of `ρ` to `W` as a representation, and the representation on `V / W` induced by `ρ`.
When `S` is a normal subgroup of `G` on which `ρ` is trivial, we also define the `G / S` representation induced by `ρ`.
We use this to define the `G / S` representation on `V^S`.
We also add `Representation.self_inv_apply, Representation.inv_self_apply`, which supercede the following lemmas:
Deletions:
- FDRep.inv_ρ_self_apply
- FDRep.ρ_inv_self_apply
- Rep.inv_ρ_self_apply
- Rep.ρ_inv_self_apply
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
174/5 |
Mathlib/RepresentationTheory/Basic.lean,Mathlib/RepresentationTheory/FDRep.lean,Mathlib/RepresentationTheory/Invariants.lean,Mathlib/RepresentationTheory/Rep.lean |
4 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
4-79579 4 days ago |
6-18343 6 days ago |
58-80196 58 days |
| 23459 |
Timeroot author:Timeroot |
feat: Definition of `Clone` notations and typeclasses |
Definitions and notation typeclasses for #20051
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
100/0 |
Mathlib.lean,Mathlib/Algebra/Clone/Defs.lean |
2 |
22 |
['Timeroot', 'YaelDillies', 'dupuisf', 'eric-wieser', 'github-actions', 'urkud'] |
YaelDillies assignee:YaelDillies |
4-77999 4 days ago |
37-14282 1 month ago |
39-63385 39 days |
| 24597 |
yuma-mizuno author:yuma-mizuno |
feat(CategoryTheory/Monoidal): replace Mon_ lemmas with Mon_Class lemmas |
extracted from #15254
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
165/123 |
Mathlib/CategoryTheory/Monoidal/Mon_.lean |
1 |
5 |
['github-actions', 'joelriou', 'leanprover-community-bot-assistant'] |
nobody |
4-46096 4 days ago |
4-48872 4 days ago |
9-2879 9 days |
| 24337 |
mans0954 author:mans0954 |
feature(Analysis/InnerProductSpace/Basic): Add norm_add_eq_iff_real |
Adds `norm_add_eq_iff_real` - a sufficient and necessary condition for equality in the triangle inequality.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
6/0 |
Mathlib/Analysis/InnerProductSpace/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
4-36533 4 days ago |
20-37529 20 days ago |
20-37589 20 days |
| 23161 |
mans0954 author:mans0954 |
feature(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range |
The distance between two elements of `Finset.range N` (i.e. absolute value of the difference as integers) is less than `N`.
A lemma I found useful for something I was working on, so sharing here in case it's of wider interest.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
30/0 |
Mathlib.lean,Mathlib/Algebra/Order/Group/Unbundled/Abs.lean,Mathlib/Data/Finset/RangeDistance.lean |
3 |
3 |
['fbarroero', 'github-actions'] |
nobody |
4-36474 4 days ago |
54-86068 1 month ago |
54-86059 54 days |
| 24735 |
joelriou author:joelriou |
chore(CategoryTheory/Monoidal): define tensorLeft/Right as abbrev for curriedTensor |
In the study of commutation of tensor products with colimits, we may not be completely sure about phrasing the assumptions (as instances) in terms of `tensorLeft X` (resp. `tensorRight Y`) or in terms of `(curriedTensor C).obj X` (resp. `(curriedTensor C).flip.obj Y`), even though they are defeq, and we could have to introduce lemmas/instances to deduce properties of `tensorLeft X` from that of `(curriedTensor C).obj` and vice versa. By making `tensorLeft` and `tensorRight` abbreviations, this PR makes such issues disappear.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
20/21 |
Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean,Mathlib/CategoryTheory/Closed/Functor.lean,Mathlib/CategoryTheory/Closed/Monoidal.lean,Mathlib/CategoryTheory/Monoidal/Bimod.lean,Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean,Mathlib/CategoryTheory/Monoidal/Category.lean |
6 |
6 |
['fivemeyestore', 'fivemhostingserver', 'fivemserverhostings', 'fivemtebex', 'github-actions', 'scriptforfivem'] |
nobody |
4-33837 4 days ago |
4-37345 4 days ago |
4-37330 4 days |
| 24530 |
chrisflav author:chrisflav |
feat(RingTheory): faithfully flat ring maps |
Co-authored by: Joël Riou
---
- [ ] depends on: #24375
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
159/15 |
Mathlib.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean,Mathlib/RingTheory/LocalProperties/Basic.lean,Mathlib/RingTheory/RingHom/FaithfullyFlat.lean,Mathlib/RingTheory/RingHom/Finite.lean,Mathlib/RingTheory/RingHom/Flat.lean,Mathlib/RingTheory/RingHom/Integral.lean,Mathlib/RingTheory/RingHom/Locally.lean,Mathlib/RingTheory/RingHom/Surjective.lean,Mathlib/RingTheory/RingHom/Unramified.lean,Mathlib/RingTheory/RingHomProperties.lean |
12 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
4-33143 4 days ago |
4-33144 4 days ago |
4-34211 4 days |
| 24711 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal/Limits): miscellany about preservation of (co)limits by tensor products |
Register some instances regarding preservations of (co)limits for the tensor product of a monoidal category. More precisely, we register the fact that if the category is braided and `tensorLeft c` preserves colimits (this can be inferred e.g via `MonoidalClosed C`), then so does `tensorRight c` for every `c`.
We also rephrase preservation of (co)limits for `curriedTensor C` in terms of preservations of (co)limits for `tensorRight c`.
The PR introduces also introduces a directory `CategoryTheory.Monoidal.Limits` and moves the existing file `CategoryTheory.Monoidal.Limits.lean` to `CategoryTheory.Monoidal.Limits.Basic`.
---
The instances registered here are tailored so that for a braided monoidal closed category, `PreservesColimit₂` instances from #24685 can be inferred with the results of #24686 for the external product of diagrams defined in #24703
[](https://gitpod.io/from-referrer/)
|
file-removed
t-category-theory
|
72/2 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean,Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean,Mathlib/CategoryTheory/Monoidal/Limits/Preserves.lean |
4 |
8 |
['github-actions', 'joelriou', 'robin-carlier'] |
nobody |
4-31626 4 days ago |
4-31626 4 days ago |
5-14917 5 days |
| 23197 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Equivalences): category structure on equivalences |
We put a category structure on `(C ≌ D)`. The morphisms are simply natural transformations between the underlying functor. We also provide various API for this structure.
---
While this PR contains functoriality of the operation that maps an equivalence to its underlying functor, functoriality of inverses will be in a different PR and recorded in a different file : I feel the most natural way to do this is to bring in the results from `Adjunction.Mates`, but this imports quite a lot of stuff.
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
69/0 |
Mathlib/CategoryTheory/Equivalence.lean |
1 |
11 |
['github-actions', 'joelriou', 'robin-carlier'] |
joelriou assignee:joelriou |
4-31323 4 days ago |
4-31323 4 days ago |
53-67469 53 days |
| 24441 |
MrSumato author:MrSumato |
feat(Data/List): add Lyndon-Schutzenberger theorem on list commutativity |
Add Lyndon-Schutzenberger theorem on list commutativity. Included definition for List.repeatSelf that returns list repeated n times.
---
This is my first mathlib PR, so any comments are highly appreciated.
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
|
129/1 |
Mathlib.lean,Mathlib/Data/List/Commutativity.lean,Mathlib/Data/List/Defs.lean,Mathlib/Data/List/Lemmas.lean |
4 |
23 |
['MrSumato', 'github-actions', 'grunweg', 'plp127'] |
nobody |
4-15764 4 days ago |
6-80687 6 days ago |
6-81716 6 days |
| 23748 |
vasnesterov author:vasnesterov |
feat(Analysis/Analytic): `HasFPowerSeriesOnBall.comp_sub` variations |
Prove `HasFPowerSeriesOnBall.comp_sub` variations for `HasFPowerSeriesOnBall`'s friend structures.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
57/0 |
Mathlib/Analysis/Analytic/Basic.lean |
1 |
5 |
['github-actions', 'j-loreaux', 'urkud', 'vasnesterov'] |
nobody |
4-14238 4 days ago |
4-14239 4 days ago |
37-5337 37 days |
| 23681 |
Timeroot author:Timeroot |
feat(Algebra/Polynomial): Descartes' Rule of signs |
Proof of Descartes' Rule of Signs. Last PR from https://github.com/Timeroot/lean-descartes-signs , now that #9085 is merged. Defines `Polynomial.SignVariations` as the relevant quantity, and `descartes_rule_of_signs` as the headline theorem.
---
I tried to clean it up + golf it down and did shrink it a good deal. The lemma `signvar_mul_eraseLead_le_of_nextCoeff` is still 142 lines, and `succ_sign_lin_mul` is ~140 lines of code as well. Those are the ugly ones. I welcome ideas if someone wants to try to clean them up more! But the proof really does require an annoying bit of case-splitting, as far as I can tell.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
616/3 |
Mathlib.lean,Mathlib/Algebra/Polynomial/CoeffList.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Algebra/Polynomial/EraseLead.lean,Mathlib/Algebra/Polynomial/RuleOfSigns.lean |
5 |
5 |
['BoltonBailey', 'Timeroot', 'github-actions'] |
nobody |
4-6000 4 days ago |
39-79449 1 month ago |
39-79497 39 days |
| 24689 |
chrisflav author:chrisflav |
feat(Topology): compact open covered sets |
This is used to define the fpqc topology for schemes.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
t-topology
|
219/0 |
Mathlib.lean,Mathlib/Data/Set/Sigma.lean,Mathlib/Topology/Compactness/Compact.lean,Mathlib/Topology/Sets/CompactOpenCovered.lean,Mathlib/Topology/Sets/Opens.lean,Mathlib/Topology/Spectral/Prespectral.lean |
6 |
3 |
['erdOne', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
4-4566 4 days ago |
4-4583 4 days ago |
5-62065 5 days |
| 22341 |
chrisflav author:chrisflav |
feat(RingTheory): formulas for `Module.rankAtStalk` for various constructions |
Compute `Module.rankAtStalk` for base change and products. Relate it to being trivial and to the dimension of the fiber.
---
- [x] depends on: #22339
- [x] depends on: #22336
- [x] depends on: #22328
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
179/3 |
Mathlib/RingTheory/LocalRing/Module.lean,Mathlib/RingTheory/Spectrum/Prime/Basic.lean,Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean |
4 |
12 |
['chrisflav', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
4-1845 4 days ago |
4-7818 4 days ago |
18-78258 18 days |
| 24756 |
urkud author:urkud |
chore(Calculus): add `Function.const` versions of some lemmas |
Rename `fun _ ↦ c` versions to `fun_const`.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
25/9 |
Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/Deriv/Basic.lean,Mathlib/Analysis/Calculus/FDeriv/Analytic.lean,Mathlib/Analysis/Calculus/FDeriv/Basic.lean,Mathlib/Analysis/Calculus/Gradient/Basic.lean |
5 |
3 |
['eric-wieser', 'github-actions', 'urkud'] |
nobody |
3-74294 3 days ago |
3-81740 3 days ago |
3-81790 3 days |
| 24498 |
ScottCarnahan author:ScottCarnahan |
refactor (RingTheory/HahnSeries/HEval): remove positive order condition from definition |
This PR removes the positive order condition for substitution (or Hahn evaluation) of a Hahn series into a power series. When the order is not positive, the function substitutes zero. We also add short lemmas for substitution into `PowerSeries.X` and `PowerSeries.C`.
---
Is there a better way to express `eq_toFun`?
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
37/13 |
Mathlib/RingTheory/HahnSeries/HEval.lean,Mathlib/RingTheory/HahnSeries/Summable.lean |
2 |
1 |
['github-actions'] |
nobody |
3-67634 3 days ago |
13-34202 13 days ago |
13-34186 13 days |
| 24351 |
eric-wieser author:eric-wieser |
feat: fderiv lemmas for `pow` |
This generalizes the lemmas about `fderiv fun x => f x ^ n` to work over arbitrary normed modules and algebras.
Following the convention set by the lemmas about `fderiv` and `*`, we use `'`d names for the non-commutative variants.
Moves:
- `deriv_pow''` -> `deriv_pow`
- `deriv_pow` -> `deriv_pow_field`
- `derivWithin_pow'` -> `derivWithin_pow_field'`
Deletions:
- `deriv_pow'`
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
282/82 |
Mathlib.lean,Mathlib/Analysis/Calculus/Deriv/Polynomial.lean,Mathlib/Analysis/Calculus/Deriv/Pow.lean,Mathlib/Analysis/Calculus/FDeriv/Mul.lean,Mathlib/Analysis/Calculus/FDeriv/Pow.lean,Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Complex/Angle.lean,Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean,Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean |
9 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
3-65446 3 days ago |
3-65446 3 days ago |
4-12493 4 days |
| 23963 |
alreadydone author:alreadydone |
feat(RingTheory): isotypic API and simple Wedderburn–Artin existence |
A replacement of #23583 with more meaningful intermediate results.
Co-authored-by: Edison Xie @Whysoserioushah
Co-authored-by: Jujian Zhang [jujian.zhang19@imperial.ac.uk](mailto:jujian.zhang19@imperial.ac.uk)
---
- [x] depends on: #24119
Module docstrings are added in #24192, specifically [f5b94a2](https://github.com/leanprover-community/mathlib4/pull/24192/commits/f5b94a2bf5a85422b7349157a454b0d4e3a7e0ae)
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
417/20 |
Mathlib.lean,Mathlib/RingTheory/SimpleModule/Basic.lean,Mathlib/RingTheory/SimpleModule/IsAlgClosed.lean,Mathlib/RingTheory/SimpleModule/Isotypic.lean,Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean |
5 |
35 |
['Whysoserioushah', 'alreadydone', 'eric-wieser', 'github-actions', 'jcommelin', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
3-62975 3 days ago |
13-35565 13 days ago |
18-11727 18 days |
| 22966 |
alreadydone author:alreadydone |
feat(RingTheory): degree 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
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
272/49 |
Mathlib/RingTheory/AdjoinRoot.lean,Mathlib/RingTheory/Algebraic/Basic.lean,Mathlib/RingTheory/Algebraic/Integral.lean,Mathlib/RingTheory/AlgebraicIndependent/AlgebraicClosure.lean,Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean,Mathlib/RingTheory/TensorProduct/Basic.lean |
6 |
11 |
['Louddy', 'alreadydone', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
3-60929 3 days ago |
3-61898 3 days ago |
21-32759 21 days |
| 24734 |
mbkybky author:mbkybky |
feat(Algebra/Homology/DerivedCategory): `Ext` commutes with finite coproducts |
Prove that `Ext` commutes with finite coproducts and products.
Co-authored-by: Nailin Guan @Thmoas-Guan
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-category-theory
label:t-algebra$ |
83/5 |
Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean,Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean,Mathlib/CategoryTheory/Preadditive/Biproducts.lean |
3 |
6 |
['github-actions', 'joelriou', 'mbkybky'] |
nobody |
3-53668 3 days ago |
3-53668 3 days ago |
3-59379 3 days |
| 24261 |
Paul-Lez author:Paul-Lez |
chore: replace `WithLp.equiv` with a new pair `WithLp.toLp`/`WithLp.ofLp` |
This PR does the following:
- deprecate `WithLp.equiv`
- Add `WithLp.toLp` and `WithLp.ofLp` (for consistency with other equivalences to type synonyms)
See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/defeq.20abuse.20in.20.60WithLp.60)
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
750/361 |
Mathlib/Algebra/Module/ZLattice/Covolume.lean,Mathlib/Analysis/CStarAlgebra/Matrix.lean,Mathlib/Analysis/Calculus/ContDiff/WithLp.lean,Mathlib/Analysis/Calculus/FDeriv/WithLp.lean,Mathlib/Analysis/InnerProductSpace/PiL2.lean,Mathlib/Analysis/InnerProductSpace/ProdL2.lean,Mathlib/Analysis/Matrix.lean,Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean,Mathlib/Analysis/Normed/Lp/PiLp.lean,Mathlib/Analysis/Normed/Lp/ProdLp.lean,Mathlib/Analysis/Normed/Lp/WithLp.lean,Mathlib/Analysis/Quaternion.lean,Mathlib/Analysis/RCLike/Inner.lean,Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean,Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean,Mathlib/LinearAlgebra/Matrix/Hermitian.lean,Mathlib/LinearAlgebra/Matrix/LDL.lean,Mathlib/LinearAlgebra/Matrix/Spectrum.lean,Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean,Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean,Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean,MathlibTest/EuclideanSpace.lean |
24 |
48 |
['Paul-Lez', 'YaelDillies', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
3-53118 3 days ago |
3-53512 3 days ago |
7-80839 7 days |
| 24450 |
justus-springer author:justus-springer |
feat(Algebra/Order/Nonneg): A finite module is finite over the nonnegative scalars |
From Toric
---
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
new-contributor
t-algebra
label:t-algebra$ |
21/3 |
Mathlib/Algebra/Order/Nonneg/Module.lean |
1 |
3 |
['YaelDillies', 'github-actions'] |
nobody |
3-42602 3 days ago |
3-42602 3 days ago |
15-19166 15 days |
| 23940 |
YaelDillies author:YaelDillies |
feat: polytopes |
From Toric
Co-authored-by: Matthew Johnson
---
[](https://gitpod.io/from-referrer/)
|
toric
t-analysis
|
74/0 |
Mathlib.lean,Mathlib/Geometry/Convex/Polytope.lean,Mathlib/Geometry/Convex/README.md |
3 |
6 |
['Parcly-Taxel', 'YaelDillies', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
3-34653 3 days ago |
3-39631 3 days ago |
33-43226 33 days |
| 24205 |
meithecatte author:meithecatte |
chore(RegularExpressions): clarify that TODO has pending PRs |
The TODO on equivalence between regular expressions and DFAs seems to be particularly appealing to new contributors, having spawned multiple competing PRs working towards that goal.
It is also one where a new contributor is quite likely to produce a design that is not inline with mathlib's API design philosophy and will require a lot of guidance, which causes the PRs to languish in review.
Reword the TODO to make it less likely that the situation gets worse.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-computability
new-contributor
easy
|
2/1 |
Mathlib/Computability/RegularExpressions.lean |
1 |
7 |
['YaelDillies', 'github-actions', 'meithecatte', 'urkud'] |
nobody |
3-34481 3 days ago |
3-34481 3 days ago |
25-1885 25 days |
| 24758 |
erdOne author:erdOne |
feat(AlgebraicGeometry): Inverse limit of nonempty schemes is nonemtpy |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
121/0 |
Mathlib.lean,Mathlib/Algebra/Category/Ring/FilteredColimits.lean,Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean,Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean,Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean |
5 |
1 |
['github-actions'] |
nobody |
3-29741 3 days ago |
3-29741 3 days ago |
3-76573 3 days |
| 24774 |
chrisflav author:chrisflav |
chore(RingTheory/Ideal): `Ideal.Quotient.factor` as an `AlgHom` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
29/0 |
Mathlib/RingTheory/Ideal/Quotient/Operations.lean |
1 |
1 |
['github-actions'] |
nobody |
3-26554 3 days ago |
3-26618 3 days ago |
3-26603 3 days |
| 24697 |
mbkybky author:mbkybky |
refactor(Algebra/Module/Projective): generalize universes |
Generalize `(P : Type max u v)` to `(P : Type v) [Small.{v} R]` in [Module.Projective.of_lifting_property](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/Projective.html#Module.Projective.of_lifting_property) and [IsProjective.iff_projective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/ModuleCat/Projective.html#IsProjective.iff_projective). Also generalize universes in [Module.Projective.iff_split](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/Projective.html#Module.Projective.iff_split).
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
82/47 |
Mathlib/Algebra/Category/ModuleCat/Projective.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Module/Projective.lean,Mathlib/LinearAlgebra/Finsupp/Defs.lean |
4 |
1 |
['github-actions'] |
nobody |
3-24600 3 days ago |
3-24649 3 days ago |
3-24634 3 days |
| 24528 |
chrisflav author:chrisflav |
feat(AlgebraicGeometry): directed covers |
Directed covers are covers, where every intersection can be covered by a component of the cover. For open covers this is equivalent to the images forming a basis of the topology.
If a cover is directed, the compatibility conditions for gluing become easier, because only compatibility with the transition maps needs to be checked.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
233/0 |
Mathlib.lean,Mathlib/AlgebraicGeometry/Cover/Directed.lean |
2 |
5 |
['chrisflav', 'erdOne', 'github-actions', 'joelriou'] |
nobody |
3-22054 3 days ago |
7-84124 7 days ago |
12-72696 12 days |
| 24493 |
urkud author:urkud |
chore(*): review `simp` lemmas for `piCongr*` equivs |
- remove `@[simp]` from lemmas with `Eq.rec` in the RHS;
- add missing `@[simp]` lemmas;
---
[](https://gitpod.io/from-referrer/)
|
tech debt |
55/12 |
Mathlib/Logic/Equiv/Basic.lean,Mathlib/Topology/Homeomorph/Lemmas.lean,Mathlib/Topology/UniformSpace/Equiv.lean |
3 |
3 |
['eric-wieser', 'github-actions', 'urkud'] |
nobody |
3-19176 3 days ago |
7-18765 7 days ago |
13-53185 13 days |
| 24769 |
YaelDillies author:YaelDillies |
feat: `M ⟶ N` is a commutative monoid if `N` is a commutative monoid object |
From Toric
Co-authored-by: Andrew Yang
Co-authored-by: Michał Mrugała
---
[](https://gitpod.io/from-referrer/)
|
toric
t-category-theory
|
151/11 |
Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean |
3 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
3-17099 3 days ago |
3-17119 3 days ago |
3-30306 3 days |
| 24593 |
Multramate author:Multramate |
refactor(AlgebraicGeometry/EllipticCurve/*): replace Fin 3 with products |
This allows the removal of all instances of `erw` in `Jacobian` and `Projective` files.
---
- [ ] depends on: #21356
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
938/1017 |
Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Basic.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Point.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Basic.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Point.lean |
8 |
n/a |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
3-11475 3 days ago |
unknown |
unknown |
| 24602 |
xyzw12345 author:xyzw12345 |
feat(LinearAlgebra/SymmetricAlgebra): IsSymmetricAlgebra |
This PR is a part of #21539, which separates out the part about `IsSymmetricAlgebra`.
Co-authored-by: Raphael Douglas Giles @Raph-DG
Co-authored-by: Zhixuan Dai <22300180006@m.fudan.edu.cn>
Co-authored-by: Zhenyan Fu
Co-authored-by: Yiming Fu
- [ ] depends on: #21539
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
78/0 |
Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/Basis.lean |
2 |
5 |
['eric-wieser', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
3-8910 3 days ago |
3-9162 3 days ago |
3-11104 3 days |
| 24673 |
adomani author:adomani |
fix(docstring linter): inspect also internal docstrings |
This omission was pointed out in #24532.
---
[](https://gitpod.io/from-referrer/)
|
t-linter
maintainer-merge
|
81/32 |
Mathlib/Algebra/Homology/ShortComplex/Homology.lean,Mathlib/CategoryTheory/EpiMono.lean,Mathlib/Tactic/FunProp/Types.lean,Mathlib/Tactic/Linter/DocString.lean,Mathlib/Tactic/MkIffOfInductiveProp.lean,Mathlib/Topology/CWComplex/Classical/Finite.lean,MathlibTest/DocString.lean |
7 |
12 |
['adomani', 'github-actions', 'grunweg'] |
grunweg assignee:grunweg |
3-4388 3 days ago |
3-4389 3 days ago |
6-14169 6 days |
| 24785 |
chrisflav author:chrisflav |
feat(Algebra/MvPolynomial): add `MvPolynomial.mem_range_map_of_coeffs_subset` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
60/0 |
Mathlib/Algebra/MvPolynomial/Basic.lean,Mathlib/Algebra/MvPolynomial/Eval.lean |
2 |
1 |
['github-actions'] |
nobody |
3-1646 3 days ago |
3-1708 3 days ago |
3-1693 3 days |
| 23238 |
YaelDillies author:YaelDillies |
feat: extended floor and ceil |
My motivation for this is to prove `ENat.toENNReal (⨆ i, f i) = ⨆ i, ENat.toENNReal (f i)` and `ENat.toENNReal (⨅ i, f i) = ⨅ i, ENat.toENNReal (f i)`. Kalle Kytölä independently needs this for his formalisation of statistical physics.
From MiscYD
---
- [x] depends on: #24781
- [x] depends on: #24782
See #15269 for a past attempt.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
235/0 |
Mathlib.lean,Mathlib/Algebra/Order/Floor/Extended.lean |
2 |
24 |
['YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'kkytola', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
2-84718 2 days ago |
3-4269 3 days ago |
50-56491 50 days |
| 23721 |
YaelDillies author:YaelDillies |
chore: rename `AlgebraCat` to `AlgCat` |
and its friends too.
The new names:
* are shorter
* match `MonCat`, `CommMonCat` and (almost) match `Grp`, `CommGrp`
* are what people would write on paper
The existing name is too much of a mouthful to be usefully included in declaration names. For example, [`BialgebraCat.hasForgetToAlgebra`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/BialgebraCat/Basic.html#BialgebraCat.hasForgetToAlgebra) wasn't named `BialgebraCat.hasForgetToAlgebraCat`.
---
[](https://gitpod.io/from-referrer/)
|
file-removed
t-algebra
label:t-algebra$ |
438/431 |
Mathlib.lean,Mathlib/Algebra/Algebra/Defs.lean,Mathlib/Algebra/BrauerGroup/Defs.lean,Mathlib/Algebra/Category/AlgCat/Basic.lean,Mathlib/Algebra/Category/AlgCat/Limits.lean,Mathlib/Algebra/Category/AlgCat/Monoidal.lean,Mathlib/Algebra/Category/AlgCat/Symmetric.lean,Mathlib/Algebra/Category/AlgebraCat/Symmetric.lean,Mathlib/Algebra/Category/BialgCat/Basic.lean,Mathlib/Algebra/Category/BialgCat/Monoidal.lean,Mathlib/Algebra/Category/CoalgCat/Basic.lean,Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean,Mathlib/Algebra/Category/CoalgCat/Monoidal.lean,Mathlib/Algebra/Category/HopfAlgCat/Basic.lean,Mathlib/Algebra/Category/HopfAlgCat/Monoidal.lean,Mathlib/Algebra/Category/Ring/Under/Basic.lean,Mathlib/CategoryTheory/Monoidal/Hopf_.lean,Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean,Mathlib/CategoryTheory/Monoidal/Internal/Module.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/LinearAlgebra/CliffordAlgebra/CategoryTheory.lean,Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean,Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Symmetric.lean,Mathlib/RingTheory/Coalgebra/TensorProduct.lean,Mathlib/RingTheory/HopfAlgebra/Basic.lean,MathlibTest/CategoryTheory/ConcreteCategory/Alg.lean,docs/overview.yaml |
27 |
19 |
['Kiolt', 'YaelDillies', 'b-mehta', 'erdOne', 'github-actions', 'leanprover-community-bot-assistant', 'urkud'] |
nobody |
2-84084 2 days ago |
2-84132 2 days ago |
13-72541 13 days |
| 24788 |
chrisflav author:chrisflav |
chore(RingTheory/Extension): move into folders |
We move
- `Mathlib.RingTheory.Extension` -> `Mathlib.RingTheory.Extension.Basic`
- `Mathlib.RingTheory.Generators` -> `Mathlib.RingTheory.Extension.Generators`
- `Mathlib.RingTheory.Presentation` -> `Mathlib.RingTheory.Extension.Presentation.Basic`
- `Mathlib.RingTheory.Kaehler.CotangentComplex` -> `Mathlib.RingTheory.Extension.Cotangent.Basic`
- `Mathlib.RingTheory.CotangentLocalizationAway` -> `Mathlib.RingTheory.Extension.Cotangent.LocalizationAway`
---
See https://github.com/leanprover-community/mathlib4/pull/24788/files/74bc7316cbca51f556f78b4debcc5edba411c170 for a meaningfull diff.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
2253/2233 |
Mathlib.lean,Mathlib/Algebra/Module/Presentation/Differentials.lean,Mathlib/RingTheory/CotangentLocalizationAway.lean,Mathlib/RingTheory/Extension.lean,Mathlib/RingTheory/Extension/Basic.lean,Mathlib/RingTheory/Extension/Cotangent/Basic.lean,Mathlib/RingTheory/Extension/Cotangent/LocalizationAway.lean,Mathlib/RingTheory/Extension/Generators.lean,Mathlib/RingTheory/Extension/Presentation/Basic.lean,Mathlib/RingTheory/Generators.lean,Mathlib/RingTheory/Kaehler/CotangentComplex.lean,Mathlib/RingTheory/Kaehler/JacobiZariski.lean,Mathlib/RingTheory/Presentation.lean,Mathlib/RingTheory/Smooth/Kaehler.lean,Mathlib/RingTheory/Smooth/StandardSmooth.lean,Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean |
16 |
1 |
['github-actions'] |
nobody |
2-81496 2 days ago |
2-81711 2 days ago |
2-83755 2 days |
| 21838 |
joneugster author:joneugster |
feat(Cache): Allow arguments of the form `Mathlib.Data` which correspond to a folder but not a file |
---
- [x] depends on: #21834
[](https://gitpod.io/from-referrer/)
|
CI
t-meta
|
34/11 |
Cache/IO.lean,Cache/Main.lean |
2 |
10 |
['eric-wieser', 'github-actions', 'joneugster', 'mathlib4-dependent-issues-bot', 'mergify'] |
nobody |
2-80072 2 days ago |
40-18861 1 month ago |
43-2249 43 days |
| 24382 |
joelriou author:joelriou |
feat(CategoryTheory): pseudofunctors from strict bicategories |
This PR provides an API for pseudofunctors `F` from a strict bicategory `B`. In particular, this shall apply to pseudofunctors from locally discrete bicategories.
We first introduce more flexible variants of `mapId` and `mapComp`: for example, if `f` and `g` are composable morphisms and `fg` is such that `h : fg = f ≫ f`, we provide an isomorphism `F.mapComp' f g fg h : F.map fg ≅ F.map f ≫ F.map g`. We study the compatibilities of these isomorphisms with respect to composition with identities and associativity.
Secondly, given a commutative square `t ≫ r = l ≫ b` in `B`, we construct an isomorphism `F.map t ≫ F.map r ≅ F.map l ≫ F.map b`.
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
168/0 |
Mathlib.lean,Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean,Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean |
3 |
13 |
['callesonne', 'erdOne', 'github-actions', 'joelriou'] |
nobody |
2-72235 2 days ago |
3-17400 3 days ago |
18-2835 18 days |
| 22662 |
plp127 author:plp127 |
feat: Localization.Away.lift (computably) |
This PR adds `Localization.Away.lift'` and `Localization.Away.lift`, computable alternatives to `Localization.awayLift`.
---
- [x] depends on: #24791
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
74/0 |
Mathlib/RingTheory/Localization/Away/Basic.lean |
1 |
11 |
['eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'plp127', 'vihdzp'] |
nobody |
2-69117 2 days ago |
2-70049 2 days ago |
68-70035 68 days |
| 24795 |
DavidLedvinka author:DavidLedvinka |
feat(MeasureTheory/Group): add quasiMeasurePreserving group operation theorems |
Add theorems that proves group multiplication is quasi-measure preserving and tag them with `fun_prop`. Also tags a few other theorems with `fun_prop`.
|
t-measure-probability |
32/4 |
Mathlib/MeasureTheory/Group/Prod.lean |
1 |
1 |
['github-actions'] |
nobody |
2-63588 2 days ago |
2-63588 2 days ago |
2-63645 2 days |
| 24184 |
YaelDillies author:YaelDillies |
feat: `[G : H]` notation for the index of `H : Subgroup G` |
This is a cute notation which I wrote for FLT. Not sure whether we want it in mathlib nor how to include `relindex` in the picture.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
RFC
label:t-algebra$ |
5/0 |
Mathlib/GroupTheory/Index.lean |
1 |
7 |
['YaelDillies', 'erdOne', 'github-actions', 'j-loreaux', 'kbuzzard'] |
nobody |
2-54711 2 days ago |
2-54711 2 days ago |
25-78831 25 days |
| 24539 |
Parcly-Taxel author:Parcly-Taxel |
feat: restore positivity extensions for `EReal` |
|
t-data
t-meta
|
27/41 |
Mathlib/Data/EReal/Basic.lean |
1 |
5 |
['Parcly-Taxel', 'eric-wieser', 'github-actions', 'urkud'] |
nobody |
2-53484 2 days ago |
2-71609 2 days ago |
12-54084 12 days |
| 23935 |
Thmoas-Guan author:Thmoas-Guan |
feat(RingTheory/IsSMulRegular): categorical constructions for IsSMulRegular |
The categorical constructions for `IsSMulRegular` for later use related to `Ext` in a separate file.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-category-theory
label:t-algebra$ |
62/0 |
Mathlib.lean,Mathlib/Algebra/Homology/ExactSequence.lean,Mathlib/RingTheory/Regular/Category.lean |
3 |
28 |
['Thmoas-Guan', 'erdOne', 'github-actions', 'joelriou', 'riccardobrasca'] |
joelriou assignee:joelriou |
2-42035 2 days ago |
21-7948 21 days ago |
29-67444 29 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`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
50/0 |
Mathlib/Algebra/Module/FinitePresentation.lean |
1 |
4 |
['Thmoas-Guan', 'acmepjz', 'github-actions'] |
nobody |
2-41996 2 days ago |
38-43875 1 month ago |
38-43870 38 days |
| 21966 |
vasnesterov author:vasnesterov |
feat(Tactic/Order): support `⊤`, `⊥`, and lattice operations |
Support `⊤`, `⊥`, and lattice operations in the `order` tactic.
---
- [x] depends on: #21877
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
248/68 |
Mathlib/Tactic/Order.lean,Mathlib/Tactic/Order/CollectFacts.lean,Mathlib/Tactic/Order/Graph/Basic.lean,Mathlib/Tactic/Order/Preprocessing.lean,MathlibTest/order.lean,scripts/noshake.json |
6 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
2-41086 2 days ago |
41-35507 1 month ago |
75-32002 75 days |
| 17914 |
xroblot author:xroblot |
feat(NumberTheory/NumberField): proof of the Analytic Class Number Formula |
Let `K` be a number field. Define
```lean
def dedekindZeta (s : ℂ) :=
LSeries (fun n ↦ Nat.card {I : Ideal (𝓞 K) // absNorm I = n}) s
```
and
```lean
def residue : ℝ :=
(2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * classNumber K) /
(torsionOrder K * Real.sqrt |discr K|)
```
We prove:
```lean
theorem dedekindZeta_residue :
Tendsto (fun s : ℝ ↦ (s - 1) * dedekindZeta K s) (𝓝[>] 1) (𝓝 (residue K))
```
---
- [x] depends on: #16675
- [x] depends on: #16822
- [x] depends on: #12488
- [x] depends on: #12405
- [x] depends on: #17943
- [x] depends on: #17944
- [x] depends on: #18130
- [x] depends on: #18166
- [x] depends on: #18231
- [x] depends on: #18246
- [x] depends on: #18245
- [x] depends on: #18248
- [x] depends on: #18400
- [x] depends on: #20660
- [x] depends on: #22115
- [x] depends on: #22397
- [x] depends on: #22779
- [x] depends on: #22866
- [x] depends on: #23440
- [x] depends on: #24713
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
81/0 |
Mathlib.lean,Mathlib/NumberTheory/NumberField/ClassNumber.lean,Mathlib/NumberTheory/NumberField/DedekindZeta.lean |
3 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'riccardobrasca', 'xroblot'] |
riccardobrasca assignee:riccardobrasca |
2-27238 2 days ago |
2-39579 2 days ago |
2-52889 2 days |
| 22919 |
plp127 author:plp127 |
feat(Data/Fintype/Pi): Make `Fintype` instance for `RelHom`s computable |
Makes the `Fintype` instance for rel homs computable.
See this [Zulip](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Classical.20vs.20constructive.20logic.20in.20computation/near/496220816) message.
---
- [x] depends on: #24748
[](https://gitpod.io/from-referrer/)
|
t-data |
178/44 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Coloring.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean,Mathlib/Data/Fintype/CardEmbedding.lean,Mathlib/Data/Fintype/Pi.lean |
5 |
29 |
['IvanRenison', 'b-mehta', 'eric-wieser', 'fpvandoorn', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'plp127'] |
b-mehta assignee:b-mehta |
2-21212 2 days ago |
2-26846 2 days ago |
59-41868 59 days |
| 24584 |
acmepjz author:acmepjz |
feat(RingTheory/PowerSeries/WeierstrassPreparation): Weierstrass preparation theorem over complete local ring |
We define Weierstrass division, Weierstrass factorization, and prove
Weierstrass preparation theorem.
We assume that a ring is adic complete with respect to some ideal.
If such ideal is a maximal ideal, then by `isLocalRing_of_isAdicComplete_maximal`,
such ring has only on maximal ideal, and hence such ring is a complete local ring.
## Main definitions
- `PowerSeries.IsWeierstrassDivisionAt f g q r I`: a `Prop` which asserts that a power series
`q` and a polynomial `r` of degree `< n` satisfy `f = g * q + r`, where `n` is the order of the
image of `g` in `(A / I)⟦X⟧` (defined to be zero if such image is zero, in which case
it's mathematically not considered).
- `PowerSeries.IsWeierstrassDivision`: version of `PowerSeries.IsWeierstrassDivisionAt`
for local rings with respect to its maximal ideal.
- `PowerSeries.IsWeierstrassFactorizationAt g f h I`: a `Prop` which asserts that `f` is a
distingushed polynomial at `I`, `h` is a formal power series over `A` which a unit, such that
the formal power series `g` satisfies `g = f * h`.
- `PowerSeries.IsWeierstrassFactorization`: version of `PowerSeries.IsWeierstrassFactorizationAt`
for local rings with respect to its maximal ideal.
## Main results
- `PowerSeries.exists_isWeierstrassDivision`: **Weierstrass division**: let `f`, `g` be power
series over a complete local ring, such that the image of `g` in the residue field is not zero.
Let `n` be the order of the image of `g` in the residue field. Then there exists a power series
`q` and a polynomial `r` of degree `< n`, such that `f = g * q + r`.
- `PowerSeries.IsWeierstrassDivision.elim`: The `q` and `r` in the Weierstrass division is unique.
- `PowerSeries.exists_isWeierstrassFactorization`: **Weierstrass preparation theorem**: let `g` be
a power series over a complete local ring, such that the image of `g` in the residue field is
not zero. Then there exists a distinguished polynomial `f` and a power series `h`
which is a unit, such that `g = f * h`.
- `PowerSeries.IsWeierstrassFactorization.elim`: The `f` and `h` in Werierstrass preparation
theorem is unique.
Co-authored-by: Nailin Guan <150537269+Thmoas-Guan@users.noreply.github.com>
---
[](https://gitpod.io/from-referrer/)
Supersedes #21944.
Part of Iwasawa project https://github.com/acmepjz/lean-iwasawa/blob/master/Iwasawalib/RingTheory/PowerSeries/WeierstrassPreparation.lean
- [x] depends on: #24678
|
t-algebra label:t-algebra$ |
618/0 |
Mathlib.lean,Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean |
2 |
16 |
['acmepjz', 'github-actions', 'mathlib4-dependent-issues-bot', 'riccardobrasca'] |
nobody |
2-18829 2 days ago |
2-22364 2 days ago |
6-41045 6 days |
| 23673 |
erdOne author:erdOne |
feat(AlgebraicGeometry): delaborator for coercing schemes to types |
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
t-meta
|
46/0 |
Mathlib/AlgebraicGeometry/Scheme.lean,MathlibTest/Delab/Scheme.lean |
2 |
2 |
['github-actions', 'jcommelin'] |
jcommelin assignee:jcommelin |
2-15137 2 days ago |
22-20380 22 days ago |
40-11373 40 days |
| 24771 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra/Module): lemmas for support dimension |
Add some lemma about support dimension over local ring and dimension 0.
---
- [x] depends on: #24494
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
39/3 |
Mathlib/RingTheory/KrullDimension/Module.lean |
1 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
2-13508 2 days ago |
2-42069 2 days ago |
2-45166 2 days |
| 24654 |
grunweg author:grunweg |
feat(lint-style): enforce modules are named in UpperCamelCase |
except for a handful of explicit exceptions
In passing, refactor the other two checks in `lint-style` to return the number of their errors (which is both meaningful and semantically clear), as opposed to a boolean (which can be accidentally inverted).
---
- [x] depends on: #23974 (right now, the linter complains about the two violations fixed in that PR)
[](https://gitpod.io/from-referrer/)
|
t-linter |
58/14 |
scripts/lint-style.lean |
1 |
17 |
['adomani', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] |
nobody |
2-13478 2 days ago |
2-19852 2 days ago |
2-24980 2 days |
| 22531 |
vasnesterov author:vasnesterov |
feat(Analysis): radius of convergence for `FormalMultilinearSeries.compContinuousLinearMap` |
- Add basic lemmas `compContinuousLinearMap_id` and `compContinuousLinearMap_comp`.
- Prove lower and upper bounds for the convergence radius of `f.compContinuousLinearMap`.
- Prove `radius_compNeg`: the convergence radii of `f(x)` and `f(-x)` are equal.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
137/11 |
Mathlib/Analysis/Analytic/Basic.lean,Mathlib/Analysis/Analytic/CPolynomial.lean,Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean,scripts/noshake.json |
5 |
7 |
['github-actions', 'j-loreaux', 'vasnesterov'] |
nobody |
2-3967 2 days ago |
4-11241 4 days ago |
69-6917 69 days |
| 23727 |
faenuccio author:faenuccio |
chore(RingTheory/Valuation/Discrete/Basic): refactor the definition of discrete valuation to allow for more general targets |
Co-authored by @mariainesdff
The two `ToDo` mentioned in the docstring are WIP by María Inés de Frutos-Fernández and Filippo A. E. Nuccio.
---
- [x] depends on: #23725
- [x] depends on: #23726
|
large-import
t-algebra
label:t-algebra$ |
68/26 |
Mathlib/RingTheory/Valuation/Discrete/Basic.lean |
1 |
28 |
['faenuccio', 'github-actions', 'kbuzzard', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'pechersky'] |
nobody |
2-3203 2 days ago |
2-3232 2 days ago |
16-7382 16 days |
| 24819 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(RingTheory/MvPolynomial/Groebner): add docstring and a particular case |
* add a new division theorem when one divides by a single polynomial
* add docstrings to the three division theorems
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
27/3 |
Mathlib/RingTheory/MvPolynomial/Groebner.lean |
1 |
1 |
['github-actions'] |
nobody |
2-3016 2 days ago |
2-3016 2 days ago |
2-3069 2 days |
| 24191 |
joelriou author:joelriou |
refactor(CategoryTheory): redefine triangulated subcategories using ObjectProperty |
---
- [x] depends on: #22574
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
279/191 |
Mathlib/Algebra/Homology/DerivedCategory/Basic.lean,Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean,Mathlib/CategoryTheory/ObjectProperty/Shift.lean,Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean,Mathlib/CategoryTheory/Triangulated/Subcategory.lean |
5 |
5 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
2-405 2 days ago |
2-420 2 days ago |
20-64610 20 days |
| 18254 |
callesonne author:callesonne |
feat(Bicategory/Modification/Pseudo): define modifications between strong natural transformations of pseudofunctors |
This PR adds modifications between strong natural transformations of pseudofunctors. At the same time, it improves the existing code on modifications between oplax natural tranformations of oplax functors (by removing some simp lemmas).
---
- [x] depends on: #18250
- [x] depends on: #18252
- [x] depends on: #18253
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
277/58 |
Mathlib.lean,Mathlib/CategoryTheory/Bicategory/Modification/Oplax.lean,Mathlib/CategoryTheory/Bicategory/Modification/Pseudo.lean,Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Pseudo.lean |
4 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
1-83464 1 day ago |
2-12373 2 days ago |
2-13956 2 days |
| 18285 |
callesonne author:callesonne |
feat(Bicategory/Grothendieck): functoriality of the grothendieck construction |
This PR is the start towards proving functoriality of the Grothendieck construction.
---
- [x] depends on: #18252
- [x] depends on: #18253
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
182/13 |
Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean,Mathlib/CategoryTheory/Bicategory/Grothendieck.lean,Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Pseudo.lean,Mathlib/CategoryTheory/Category/Cat.lean |
4 |
n/a |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
1-83358 1 day ago |
unknown |
unknown |
| 13611 |
callesonne author:callesonne |
feat(FiberedCategory/HasFibers): define HasFibers class |
We define a class `HasFibers p` for a given functor `p : 𝒳 ⥤ 𝒮`. The point of this is to give the user the option to supply their own fiber categories, as often the standard fibers will not be definitionally the same as the (equivalent) categories one is interested in.
Co-authored-by: Paul Lezeau
---
This is the final PR in a sequence of PRs developing the theory of fibered categories that I will make for now. I will wait for the reviewing to catch up before I start working on more of these again, so as to not create too big of a backlog.
- [x] depends on: #13603
- [x] depends on: #12982
- [x] depends on: #13416
- [x] depends on: #13410
- [x] depends on: #13393
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
283/21 |
Mathlib.lean,Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean,Mathlib/CategoryTheory/FiberedCategory/HasFibers.lean,Mathlib/CategoryTheory/FiberedCategory/HomLift.lean |
4 |
22 |
['callesonne', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot'] |
Paul-Lez assignee:Paul-Lez |
1-82848 1 day ago |
207-18681 6 months ago* |
0-571 9 minutes* |
| 17627 |
hrmacbeth author:hrmacbeth |
feat: universal properties of vector bundle constructions |
Characterizations for the smoothness of maps into the total spaces of (1) the direct sum of two vector bundles; (2) the pullback of a vector bundle.
This gap in the library was exposed by #17358.
---
- [x] depends on: #22804
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry |
311/9 |
Mathlib/Data/Bundle.lean,Mathlib/Geometry/Manifold/VectorBundle/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/Pullback.lean,Mathlib/Topology/FiberBundle/Constructions.lean |
4 |
14 |
['github-actions', 'grunweg', 'hrmacbeth', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'sgouezel'] |
grunweg assignee:grunweg |
1-79486 1 day ago |
55-27542 1 month ago |
56-11998 56 days |
| 21965 |
JovanGerb author:JovanGerb |
feat: extensible `push`(_neg) tactic - part 1 |
This is the first part of #21769, namely defining the new tactic, and only tagging the lemmas that have to be tagged to match the old behaviour.
This includes
- The `push_neg` tactic, which is a macro for `push Not`
- The `push` tactic
- The `↓pushNeg` simproc that can be used as `simp [↓pushNeg]`
- The `push` and `push_neg` tactics in `conv` mode.
- The `#push_discr_tree` command to help see what lemmas the tactic is using for a given constant.
There are two new files: `Mathlib.Tactic.Push` and `Mathlib.Tactic.Push.Attr`. The latter only introduces the `@[push]` attribute, so that it can be used by early Mathlib files without having to import `Mathlib.Tactic.Push`.
Zulip conversation: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/I.20made.20an.20extensible.20.60push.60.20tactic.20generalizing.20.60push_neg.60/near/499492535
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
311/182 |
Mathlib.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Push.lean,Mathlib/Tactic/Push/Attr.lean,MathlibTest/push_neg.lean,scripts/noshake.json |
9 |
7 |
['JovanGerb', 'github-actions', 'grunweg', 'leanprover-bot'] |
robertylewis assignee:robertylewis |
1-79023 1 day ago |
83-25448 2 months ago |
85-74611 85 days |
| 22655 |
YaelDillies author:YaelDillies |
refactor: make use of `FunLike` for `Submonoid.LocalizationMap` |
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
156/140 |
Mathlib/GroupTheory/MonoidLocalization/Away.lean,Mathlib/GroupTheory/MonoidLocalization/Basic.lean,Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean,Mathlib/RingTheory/Localization/Defs.lean |
4 |
1 |
['github-actions'] |
ericrbg assignee:ericrbg |
1-78973 1 day ago |
48-32800 1 month ago |
65-58956 65 days |
| 24762 |
erdOne author:erdOne |
chore(AlgebraicGeometry): golf file with ideal sheaf API |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
60/94 |
Mathlib/AlgebraicGeometry/AffineScheme.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean,Mathlib/AlgebraicGeometry/Morphisms/Proper.lean,Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean,Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean |
6 |
6 |
['chrisflav', 'github-actions'] |
nobody |
1-78823 1 day ago |
1-78823 1 day ago |
2-31324 2 days |
| 24333 |
xcloudyunx author:xcloudyunx |
feat(Combinatorics/SimpleGraph): cycle graph implementation for generic vertex types |
The existing `cycleGraph` implementation under Combinatorics/SimpleGraph/Circulant.lean only operates over `Fin n`. This PR implements a cycle graph implementation over any generic vertex type.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
182/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Cycle.lean |
2 |
29 |
['IvanRenison', 'github-actions'] |
kmill assignee:kmill |
1-78822 1 day ago |
20-62753 20 days ago |
20-62807 20 days |
| 24372 |
Hagb author:Hagb |
feat(Tactic/SimpIntro): add support for introducing non-propositions |
`simp_intro` would be able to introduce non-propositions.
The previous `simp_intro` tactic cannot solve some statement that can be solved by applying `intro` and `simp` like `simp_intro`. For example, the following one can be solved like this
```lean
example (r : Nat → Prop) : (∀ x, x > 0 → r x) → ∀ y z, y = 0 → z > y → r z := by
simp
intro hr
try simp at hr -- does nothing
try simp [hr] -- does nothing
intro y z
try simp [hr] -- does nothing
intro hy
try simp [hr] at hy -- does nothing
simp [hr, hy]
intro hyz
try simp [hr, hy] at hyz
simp [hr, hy, hyz] -- accomplish the goal successfully
```
while the previous `simp_intro` cannot introduce `y` and `z` here.
```lean
example (r : Nat → Prop) : (∀ x, x > 0 → r x) → ∀ y z, y = 0 → z > y → r z := by
/- the previous `simp_intro` fails with message:
invalid 'simp', proposition expected
Nat -/
simp_intro .. -- or `simp_intro hr y`
example (r : Nat → Prop) : (∀ x, x > 0 → r x) → ∀ y z, y = 0 → z > y → r z := by
-- unsolved
simp_intro hr
example (r : Nat → Prop) : (∀ x, x > 0 → r x) → ∀ y z, y = 0 → z > y → r z := by
-- successfully solve the goal with the `simp_intro` in thie commit
simp_intro .. -- or `simp_intro hr y z hy hz`
```
This commit makes it be able to introduce these kinds of hypotheses.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
|
13/2 |
Mathlib/Tactic/SimpIntro.lean,MathlibTest/simp_intro.lean |
2 |
1 |
['github-actions'] |
kmill assignee:kmill |
1-78784 1 day ago |
19-2316 19 days ago |
19-2367 19 days |
| 24395 |
rudynicolop author:rudynicolop |
feat(Data/List): list splitting definitions and lemmas |
Adds definitions and lemmas for obtaining all prefixes and suffixes of lists.
---
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
|
143/2 |
Mathlib/Data/List/Perm/Lattice.lean,Mathlib/Data/List/TakeDrop.lean |
2 |
1 |
['github-actions'] |
ericrbg assignee:ericrbg |
1-78766 1 day ago |
17-86193 17 days ago |
17-86255 17 days |
| 8691 |
urkud author:urkud |
feat(Analysis/NormedSpace): add `NormedSpace.Alternating` |
---
- [x] depends on: #19445
- [x] depends on: #19422
- [x] depends on: #24159
[](https://gitpod.io/from-referrer/) |
t-analysis |
607/4 |
Mathlib.lean,Mathlib/Analysis/NormedSpace/Alternating/Basic.lean,Mathlib/Topology/Algebra/Module/Alternating/Basic.lean,Mathlib/Topology/Algebra/Module/Alternating/Topology.lean |
4 |
68 |
['eric-wieser', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'urkud'] |
grunweg assignee:grunweg |
1-78463 1 day ago |
15-13656 15 days ago |
16-24487 16 days |
| 20160 |
vasnesterov author:vasnesterov |
feat(Data/Seq): `modify` and `set` operations for `Seq` |
Introduce `modify` and `set` operations for sequences, along with a few lemmas about them.
---
- [ ] depends on: #20071
[](https://gitpod.io/from-referrer/)
|
t-data |
92/0 |
Mathlib/Data/Seq/Seq.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
1-78067 1 day ago |
1-78085 1 day ago |
1-78235 1 day |
| 24674 |
kbuzzard author:kbuzzard |
doc: give examples of various uses of our Action classes. |
---
[](https://gitpod.io/from-referrer/)
I'm just writing the things which I wish were there every time I read these confusingly-named classes and can't immediately remember what the axioms are. |
t-algebra
documentation
label:t-algebra$ |
37/6 |
Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/Defs.lean,Mathlib/Algebra/Ring/Action/Basic.lean |
3 |
7 |
['eric-wieser', 'github-actions', 'kbuzzard'] |
nobody |
1-77782 1 day ago |
5-78355 5 days ago |
6-37313 6 days |
| 24796 |
erdOne author:erdOne |
feat(AlgebraicGeometry): locally directed gluing |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
433/133 |
Mathlib/AlgebraicGeometry/Gluing.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean,Mathlib/AlgebraicGeometry/Restrict.lean,Mathlib/AlgebraicGeometry/Scheme.lean |
6 |
1 |
['github-actions'] |
nobody |
1-76335 1 day ago |
2-60602 2 days ago |
2-60635 2 days |
| 23339 |
joelriou author:joelriou |
feat(CategoryTheory): the colimit type of a functor to types |
Given a category `J` (with `J : Type u` and `[Category.{v} J]`) and a functor `F : J ⥤ Type w`, we introduce a type `F.ColimitType : Type (max u w)`, which satisfies a certain universal property of the colimit: it is defined as a suitable quotient of `Σ j, F.obj j`. This universal property is not expressed in a categorical way (as in general `Type (max u w)` is not the same as `Type u`).
(This type `F.ColimitType` is basically the same as `CategoryTheory.Limits.Types.Quot` that is defined in `CategoryTheory.Limits.Types`, but we expand the API (with minimal imports to category theory) so that it may be used in future PRs to refactor both `DirectedSystem` and the construction of colimits in `Type`.)
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
272/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Types/ColimitType.lean |
2 |
5 |
['AntoineChambert-Loir', 'erdOne', 'github-actions', 'joelriou'] |
adamtopaz assignee:adamtopaz |
1-75704 1 day ago |
42-7587 1 month ago |
48-77124 48 days |
| 23497 |
chrisflav author:chrisflav |
chore(RingTheory/AdicCompletion/AsTensorProduct): golf using five lemma for modules |
---
- [x] depends on: #23496
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
30/81 |
Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
1-72449 1 day ago |
22-30406 22 days ago |
22-31232 22 days |
| 22767 |
robin-carlier author:robin-carlier |
feat(AlgebraicTopology/SimplexCategory): the augmented simplex category |
This PR defines `AugmentedSimplexCategory` as `WithInitial SimplexCategory`. Using the API in `CategoryTheory.WithTerminal`, we check that functors out of this category (resp. out of its opposite) corresponds to cosimplicial (resp. simplicial) objects, and we link various construction about simplicial objects in terms of this category.
---
- [x] depends on : #22658
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
118/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplexCategory/Augmented.lean |
2 |
4 |
['github-actions', 'joelriou', 'robin-carlier'] |
joelriou assignee:joelriou |
1-51537 1 day ago |
1-51537 1 day ago |
65-2926 65 days |
| 24828 |
mans0954 author:mans0954 |
feature(Algebra/Polynomial/Roots) : nthRoots_two_unit_of_char_ne_two |
Compute the second roots of the unit for rings of characteristic not 2.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
12/0 |
Mathlib/Algebra/Polynomial/Roots.lean,Mathlib/Data/Multiset/ZeroCons.lean |
2 |
1 |
['github-actions'] |
nobody |
1-50655 1 day ago |
1-50655 1 day ago |
1-56790 1 day |
| 24809 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Functor/KanExtension): preservations of Kan extensions |
Introduce a typeclass `G.PreservesLeftKanExtension F L` that asserts that a functor `G` preserves the left Kan extension of `F` along a functor `L`. Introduce a pointwise variant, and relate it to the non-pointwise version when pointwise extensions exist.
Show that a functor that preserves the relevant colimits preserve pointwise left Kan extensions. Construct isomorphisms `L.leftKanExtension F ⋙ G ≅ L.leftKanExtension (F ⋙ G)` when `G.PreservesLeftKanExtension F L` holds. Also construct a functorial version, as an isomorphism `L.lan ⋙ (whiskeringRight _ _ _).obj G ≅ (whiskeringRight _ _ _).obj G ⋙ L.lan`.
All results are dualised to right Kan extensions.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
523/0 |
Mathlib.lean,Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean,Mathlib/CategoryTheory/Functor/KanExtension/Preserves.lean |
3 |
5 |
['TwoFX', 'github-actions', 'joelriou', 'robin-carlier'] |
nobody |
1-49724 1 day ago |
2-25258 2 days ago |
2-25308 2 days |
| 24829 |
urkud author:urkud |
fix(Topology/Homotopy): fix name&args order of `comp` |
`ContinuousMap.Homotopy.hcomp` used name & arguments order
that matches Mathlib's category theory conventions,
not topology conventions.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
30/19 |
Mathlib/Topology/Homotopy/Basic.lean,Mathlib/Topology/Homotopy/Contractible.lean,Mathlib/Topology/Homotopy/Equiv.lean,Mathlib/Topology/Homotopy/Lifting.lean |
4 |
5 |
['github-actions', 'grunweg', 'urkud'] |
nobody |
1-44826 1 day ago |
1-53466 1 day ago |
1-53521 1 day |
| 24644 |
matthewjasper author:matthewjasper |
chore(RingTheory/DedekindDomain/AdicValuation): Use intValuation over intValuationDef |
`intValuationDef` exists so that we can prove its basic properties before defining `intValuation`, but it shouldn't be used afterwards. Change theorems which use `intValuation` in their names to actually use `intValution` and update usages.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
t-topology
label:t-algebra$ |
108/77 |
Mathlib/NumberTheory/NumberField/FinitePlaces.lean,Mathlib/RingTheory/DedekindDomain/AdicValuation.lean,Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean,Mathlib/RingTheory/LaurentSeries.lean |
4 |
4 |
['github-actions', 'kbuzzard', 'matthewjasper'] |
nobody |
1-44367 1 day ago |
1-44367 1 day ago |
5-49200 5 days |
| 22881 |
Champitoad author:Champitoad |
feat(CategoryTheory/Topos): add representability results for subobject classifier |
We add a section `Representability` at the end of `Mathlib.CategoryTheory.Topos.Classifier` where we formalize the necessary lemmas and definitions that lead to the proof of `CategoryTheory.isRepresentable_hasClassifier_iff`, which states that a category `C` has a subobject classifier if and only if the subobjects presheaf `CategoryTheory.Subobject.presheaf C` is representable (Proposition 1 in Section I.3 of Sheaves in Geometry and Logic [MM92]). The toughest part is found in definition `CategoryTheory.Classifier.fromRepresentation`, which formalizes as closely as possible the argument given in [MM92, pp. 33-34].
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-category-theory
|
251/22 |
Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/Presheaf.lean,Mathlib/CategoryTheory/Topos/Classifier.lean |
3 |
21 |
['Champitoad', 'github-actions', 'joelriou'] |
joelriou assignee:joelriou |
1-43805 1 day ago |
42-14701 1 month ago |
56-34703 56 days |
| 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
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-topology
|
59/4 |
Mathlib/Analysis/Calculus/ContDiff/RCLike.lean,Mathlib/Topology/EMetricSpace/Lipschitz.lean |
2 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
PatrickMassot assignee:PatrickMassot |
1-43767 1 day ago |
22-29899 22 days ago |
22-36658 22 days |
| 23367 |
b-reinke author:b-reinke |
feat(GroupTheory/FreeGroup/Reduce): add lemmas for toWord and reduce |
Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project.
This PR adds some simple helper lemmas for the interaction of `toWord` and `reduce` and basic list / group operations.
The RHS of the lemmas often contains more appearances of `reduce`, so they are not marked as `simp` lemmas.
---
[](https://gitpod.io/from-referrer/)
|
t-geometric-group-theory
t-algebra
label:t-algebra$ |
23/0 |
Mathlib/GroupTheory/FreeGroup/Reduce.lean |
1 |
9 |
['github-actions', 'grunweg', 'vlad902'] |
tb65536 assignee:tb65536 |
1-43535 1 day ago |
48-22725 1 month ago |
48-31401 48 days |
| 24015 |
alreadydone author:alreadydone |
feat(RingTheory): lemmas on finiteness of `LinearMap` and `Module.End` |
---
One less lemma than #24012, but with the advantage of not depending on #23963.
- [x] depends on: #24115
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
91/32 |
Mathlib/Algebra/Module/LinearMap/End.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean,Mathlib/LinearAlgebra/BilinearMap.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/Projection.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/SimpleModule/Basic.lean |
7 |
9 |
['alreadydone', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-dependent-issues-bot'] |
erdOne assignee:erdOne |
1-43467 1 day ago |
27-24847 27 days ago |
30-31968 30 days |
| 24835 |
RemyDegenne author:RemyDegenne |
feat(Probability): lemmas about variance |
- `Var[fun ω ↦ X ω + c; μ] = Var[X; μ]`. Same for `c + X`, `-X`, `X - c` and `c - X`.
- The variance of a Dirac measure is 0
- `Var[X; μ.map Y] = Var[X ∘ Y; μ]`
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
54/0 |
Mathlib/Probability/Variance.lean |
1 |
1 |
['github-actions'] |
nobody |
1-40807 1 day ago |
1-41100 1 day ago |
1-41085 1 day |
| 24719 |
madvorak author:madvorak |
feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv` |
---
Discussion:
https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2324719.20cannot.20find.20home/with/517142655
|
t-algebra label:t-algebra$ |
10/0 |
Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean |
1 |
8 |
['eric-wieser', 'github-actions', 'madvorak'] |
nobody |
1-38031 1 day ago |
3-21921 3 days ago |
4-58151 4 days |
| 24105 |
urkud author:urkud |
feat(Topology/UniformSpace/Path): new file |
---
- [ ] depends on: #24066
[](https://gitpod.io/from-referrer/)
|
t-topology |
112/5 |
Mathlib.lean,Mathlib/Topology/ContinuousMap/Defs.lean,Mathlib/Topology/Order/ProjIcc.lean,Mathlib/Topology/Path.lean,Mathlib/Topology/UniformSpace/CompactConvergence.lean,Mathlib/Topology/UniformSpace/Path.lean |
6 |
4 |
['ADedecker', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
1-35389 1 day ago |
7-77892 7 days ago |
7-78802 7 days |
| 24838 |
RemyDegenne author:RemyDegenne |
feat(MeasureTheory): tightness of the range of a sequence |
* `isTightMeasureSet_range_iff_tendsto_limsup_measure_norm_gt`: in a proper normed group,
the range of a sequence of measures `μ : ℕ → Measure E` is tight if and only if the function
`r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖x‖}) atTop` tends to `0` at infinity.
* `isTightMeasureSet_range_iff_tendsto_limsup_inner`: in a finite-dimensional inner product space,
the range of a sequence of measures `μ : ℕ → Measure E` is tight if and only if the function
`r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖⟪y, x⟫_𝕜‖}) atTop` tends to `0` at infinity for all `y`.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
133/2 |
Mathlib/MeasureTheory/Measure/TightNormed.lean |
1 |
2 |
['RemyDegenne', 'github-actions'] |
nobody |
1-35281 1 day ago |
1-35354 1 day ago |
1-35339 1 day |
| 7596 |
alreadydone author:alreadydone |
feat: covering maps from properly discontinuous actions and discrete subgroups |
---
- [x] depends on: #23236
[](https://gitpod.io/from-referrer/)
|
file-removed
t-topology
|
351/21 |
Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Topology/Algebra/ConstMulAction.lean,Mathlib/Topology/Algebra/Group/Pointwise.lean,Mathlib/Topology/Covering/AddCircle.lean,Mathlib/Topology/Covering/Basic.lean,Mathlib/Topology/Covering/Galois.lean,Mathlib/Topology/Homotopy/Lifting.lean,Mathlib/Topology/Instances/AddCircle.lean |
9 |
16 |
['ADedecker', 'alreadydone', 'digama0', 'github-actions', 'mathlib4-dependent-issues-bot', 'tb65536'] |
nobody |
1-35077 1 day ago |
2-13059 2 days ago |
26-18457 26 days |
| 24814 |
grunweg author:grunweg |
chore(LpSeminorm/Basic): golf a norm lemma using its enorm equivalent |
Follow-up to #24640: prove norm lemmas using their enorm counterpart.
---
[](https://gitpod.io/from-referrer/)
|
carleson
t-measure-probability
|
21/22 |
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean |
1 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
1-34162 1 day ago |
1-40585 1 day ago |
2-12475 2 days |
| 24792 |
eric-wieser author:eric-wieser |
feat: add `Matrix.vec` |
The module docstring explains the choice to make this diverge from `Function.uncurry`, as "row major" vectorization seems to be in the minority.
From eric-wieser/lean-matrix-cookbook
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
150/0 |
Mathlib.lean,Mathlib/Data/Matrix/Vec.lean |
2 |
22 |
['b-mehta', 'eric-wieser', 'github-actions'] |
nobody |
1-32614 1 day ago |
1-85120 1 day ago |
2-67137 2 days |
| 24661 |
edegeltje author:edegeltje |
feat(Tactic/Algebraize): Allow the `algebraize` tactic to use lemmas which don't (directly) mention RingHom |
This PR allows the `algebraize` tactic to be applied in more cases. Specifically, in cases where the assumption is not (directly) about RingHom, it should still be able to apply lemmas.
Written at the suggestion of @chrisflav , with the following example usecase:
```lean
import Mathlib
open AlgebraicGeometry
attribute [algebraize flat_of_flat] Flat -- pretend this is added where `AlgebraicGeometry.Flat` is defined
lemma flat_of_flat {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (h : Flat (Spec.map (CommRingCat.ofHom f))) : @Module.Flat R S _ _ f.toAlgebra.toModule := by
have : f.Flat := sorry -- supposedly, this is true. ask christian.
algebraize [f]
assumption
set_option tactic.hygienic false -- allow the tactic to produce accessible names for testing
example {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (h : Flat (Spec.map (CommRingCat.ofHom f))) : True := by
algebraize [f]
guard_hyp algebraizeInst : Module.Flat R S -- used to fail, succeeds now
trivial
```
---
[](https://gitpod.io/from-referrer/)
|
t-meta
enhancement
|
123/25 |
Mathlib/Tactic/Algebraize.lean,MathlibTest/algebraize.lean |
2 |
10 |
['chrisflav', 'edegeltje', 'github-actions'] |
nobody |
1-29497 1 day ago |
2-33917 2 days ago |
3-11021 3 days |
| 24830 |
loefflerd author:loefflerd |
feat(Analysis/UpperHalfPlane, ModularForms): extend actions from GLPos to GL |
This extends the action of `GL(2, ℝ)⁺` on the upper half-plane, and the slash actions on modular forms, to actions of all of `GL (Fin 2) ℝ` (with elements of negative determinant acting as anti-holomorphic maps).
This is mathematically extra information which we didn't have before; but the goal is also to make the modular forms code (hopefully) easier to work with, by avoiding the extra layer of coercions required by working with the subtype `GL(2, ℝ)⁺`.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
366/336 |
Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean,Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean,Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean,Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean,Mathlib/NumberTheory/Modular.lean,Mathlib/NumberTheory/ModularForms/Basic.lean,Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean,Mathlib/NumberTheory/ModularForms/LevelOne.lean,Mathlib/NumberTheory/ModularForms/SlashActions.lean,Mathlib/NumberTheory/ModularForms/SlashInvariantForms.lean |
13 |
1 |
['github-actions'] |
nobody |
1-23551 1 day ago |
1-46419 1 day ago |
1-46404 1 day |
| 21162 |
smmercuri author:smmercuri |
feat: add `Valued.WithZeroMulInt.tendsto_zero_pow_of_le_neg_one` |
If `K` is a valued ring taking values in the multiplicative integers wth a zero adjoined, then `Valued.WithZeroMulInt.tendsto_zero_pow_of_le_neg_one` is the result that `x ^ n` tends to zero in this ring if `v x` is at most `-1` valued.
---
- [x] depends on: #21160
- [x] depends on: #22055
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
89/5 |
Mathlib.lean,Mathlib/Algebra/GroupWithZero/Int.lean,Mathlib/Algebra/GroupWithZero/WithZero.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Topology/Algebra/Valued/WithZeroMulInt.lean |
5 |
14 |
['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'smmercuri'] |
nobody |
1-17330 1 day ago |
1-17330 1 day ago |
61-44331 61 days |
| 24833 |
jcommelin author:jcommelin |
chore: swap the sides of the argument to `subtypePerm` |
This way the argument will not loop, when used with `simp`.
The argument also appears in many lemmas.
This change is a workaround for the extended simpNF linter, which runs `simp [h]` with `h` of that type.
Zulip: [#mathlib4 > simpNF lint with hyps @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/simpNF.20lint.20with.20hyps/near/517741799)
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
47/47 |
Mathlib/Algebra/Group/End.lean,Mathlib/GroupTheory/Perm/Centralizer.lean,Mathlib/GroupTheory/Perm/Cycle/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Factors.lean,Mathlib/GroupTheory/Perm/Finite.lean,Mathlib/GroupTheory/Perm/Sign.lean,Mathlib/GroupTheory/Perm/Support.lean |
7 |
10 |
['JovanGerb', 'eric-wieser', 'github-actions', 'jcommelin'] |
nobody |
1-14878 1 day ago |
1-43219 1 day ago |
1-43270 1 day |
| 24842 |
grunweg author:grunweg |
feat(LpSeminorm/Trim): generalise to enorms |
---
- [x] depends on: #24841
[](https://gitpod.io/from-referrer/)
|
carleson
t-measure-probability
|
8/11 |
Mathlib/MeasureTheory/Function/LpSeminorm/Trim.lean |
1 |
3 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] |
nobody |
1-9958 1 day ago |
1-15183 1 day ago |
1-15168 1 day |
| 21283 |
erdOne author:erdOne |
feat: topology on Hom(R, S) in `CommRingCat` |
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-topology
label:t-algebra$ |
227/0 |
Mathlib.lean,Mathlib/Algebra/Category/Ring/Constructions.lean,Mathlib/Algebra/Category/Ring/Topology.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/Homeomorph/Lemmas.lean,scripts/noshake.json |
6 |
6 |
['dagurtomas', 'erdOne', 'github-actions'] |
nobody |
1-9426 1 day ago |
1-9488 1 day ago |
83-37404 83 days |
| 21950 |
erdOne author:erdOne |
feat(NumberTheory/Padics): the completion of `ℚ` at a finite place is `ℚ_[p]` |
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
253/1 |
Mathlib.lean,Mathlib/Algebra/GroupWithZero/WithZero.lean,Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/Topology/Algebra/Valued/WithVal.lean,Mathlib/Topology/Algebra/WithZeroMulInt.lean,Mathlib/Topology/Algebra/WithZeroTopology.lean |
7 |
18 |
['Ruben-VandeVelde', 'erdOne', 'github-actions', 'leanprover-community-bot-assistant', 'xroblot'] |
nobody |
1-6981 1 day ago |
6-83802 6 days ago |
31-46612 31 days |
| 24730 |
YaelDillies author:YaelDillies |
feat(Bialgebra): group-like elements |
Define group-like elements in a bialgebra, ie units `a` such that `Δ a = a ⊗ₜ a`.
We prove that group-like elements always form a group, and are linearly independent if the base ring is a domain.
From Toric
Co-authored-by: Michał Mrugała
---
- [x] depends on: #24747
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
168/0 |
Mathlib.lean,Mathlib/RingTheory/Bialgebra/GroupLike.lean |
2 |
4 |
['YaelDillies', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
1-6784 1 day ago |
3-76388 3 days ago |
3-77945 3 days |
| 24578 |
b-mehta author:b-mehta |
feat(Pointwise): cardinality of product set in GroupWithZero |
This PR:
* generalises the assumptions to `card_le_card_image₂_left` and `card_le_card_image₂_right` and golf these: they previously required injectivity everywhere despite using it in only one place. (These lemmas were also used in exactly one place each in mathlib)
* adds `card_le_card_mul_left_of_injective` and `card_le_card_mul_right_of_injective` which generalise the typeclass assumptions on the existing `card_le_card_mul_left` and `card_le_card_mul_right`
* uses the above to add versions of `card_le_card_mul_left` and `card_le_card_mul_right` in groups with zero. This is useful for applying the pointwise constructions to fields
In fact, the first versions of all the above lemmas were written in this generality, but that was seemingly lost during an upstream.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
54/16 |
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean,Mathlib/Data/Finset/NAry.lean |
3 |
1 |
['github-actions'] |
nobody |
1-5366 1 day ago |
6-30292 6 days ago |
10-67896 10 days |
| 24418 |
upobir author:upobir |
feat(Algebra/Order/Ring/Unbundled/Basic): add (x - a) * (x - b) inequalities |
---
The pr introduces inequalities that represent relation between (x - a) * (x - b) and 0. Quadratic expression inequalities generally use these lemmas. I was not sure where to put the lemmas, the LinearOrderedRing section felt like best
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
20/0 |
Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean |
1 |
10 |
['github-actions', 'j-loreaux', 'upobir'] |
adomani assignee:adomani |
1-5348 1 day ago |
1-5348 1 day ago |
16-20764 16 days |
| 24752 |
MichaelStollBayreuth author:MichaelStollBayreuth |
perf(Data.Real.Sqrt): make Real.sqrt irreducible |
We try to see what happens if we make `Real.sqrt` irreducible.
There are cases where this makes unification *very* significantly faster, compare [#mathlib4 > Coercion triggers timeout @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Coercion.20triggers.20timeout/near/517177117).
---
[](https://gitpod.io/from-referrer/)
|
t-data |
1/0 |
Mathlib/Data/Real/Sqrt.lean |
1 |
18 |
['MichaelStollBayreuth', 'eric-wieser', 'github-actions', 'leanprover-bot'] |
nobody |
1-753 1 day ago |
3-14075 3 days ago |
3-19553 3 days |
| 21237 |
scholzhannah author:scholzhannah |
feat: a weaker definition of compactly generated spaces |
This PR defines compactly coherent spaces as a topological space where a set is open iff its intersection with every compact set is open in that compact set. This notion is typically called compactly generated in the literature. There is a different [definition of compactly generated spaces already in mathlib](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Compactness/CompactlyGeneratedSpace.html#CompactlyGeneratedSpace) but that definition is stronger than the one presented here. They do however agree on Hausdorff spaces. See [this wikipedia page](https://en.wikipedia.org/wiki/Compactly_generated_space) for an explanation for the three different definitions of compactly generated spaces used in literature.
Co-authored-by: Floris van Doorn
---
See also [this discussion on Zulip](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Compactly.20generated.20spaces) about compactly generated spaces.
- [x] depends on: #21134
[](https://gitpod.io/from-referrer/)
|
t-topology |
347/0 |
Mathlib.lean,Mathlib/Topology/Compactness/CompactlyCoherentSpace.lean,docs/references.bib |
3 |
22 |
['ADedecker', 'StevenClontz', 'github-actions', 'jzxia', 'mathlib4-dependent-issues-bot', 'scholzhannah', 'urkud'] |
nobody |
0-79987 22 hours ago |
1-8831 1 day ago |
72-53888 72 days |
| 23490 |
erdOne author:erdOne |
feat(Algebra/Category): the category of topological modules |
Co-authored-by: Richard Hill
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
541/0 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean,Mathlib/Topology/Algebra/Module/ModuleTopology.lean,MathlibTest/CategoryTheory/ConcreteCategory/TopModuleCat.lean |
4 |
22 |
['chrisflav', 'erdOne', 'github-actions', 'kbuzzard'] |
nobody |
0-79002 21 hours ago |
1-8757 1 day ago |
12-2500 12 days |
| 24850 |
pechersky author:pechersky |
feat(Topology/UniformSpace/Ultra): uniform spaces induced by pseudometrics are ultra if system is ultra |
Any uniform space has a natural system of pseudometrics definable on it,
comprised of those pseudometrics constructed from a descending chain of
equivalence relation entourages. In a nonarchimedean uniformity, this pseudometric system
induces the uniformity.
---
[](https://gitpod.io/from-referrer/)
- [ ] depends on: #23111 |
t-topology |
693/0 |
Mathlib.lean,Mathlib/Topology/MetricSpace/BundledFun.lean,Mathlib/Topology/UniformSpace/Ultra/Pseudometrizable.lean |
3 |
7 |
['ADedecker', 'fpvandoorn', 'github-actions', 'mathlib4-dependent-issues-bot', 'pechersky'] |
nobody |
0-75775 21 hours ago |
1-8704 1 day ago |
1-10221 1 day |
| 24465 |
adomani author:adomani |
feat: a linter to enforce formatting |
This linter enforces that the hypotheses of every declaration are correctly formatted.
This already required multiple PRs to make mathlib compliant. Ideally, little by little the linter can be extended to format more of mathlib.
---
The default linter option is `false`, but the lakefile enforces it to be `true`.
This means that the linter does not run on `MathlibTest`. However, the tests should still be compliant, since the default option was `true` in development and the tests were fixed.
[](https://gitpod.io/from-referrer/)
|
large-import
t-linter
|
624/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter.lean,Mathlib/Tactic/Linter/CommandStart.lean,MathlibTest/CommandStart.lean,MathlibTest/EuclideanSpace.lean,MathlibTest/Simps.lean,MathlibTest/Traversable.lean,MathlibTest/antidiagonal.lean,MathlibTest/delabLinearIndependent.lean,MathlibTest/matrix.lean,MathlibTest/norm_num.lean,MathlibTest/set_like.lean,MathlibTest/vec_notation.lean,lakefile.lean |
15 |
20 |
['Parcly-Taxel', 'adomani', 'github-actions', 'grunweg'] |
grunweg assignee:grunweg |
0-73214 20 hours ago |
11-42426 11 days ago* |
14-44028 14 days* |
| 24868 |
plp127 author:plp127 |
feat(Tactic/Positivity): Support nonnegativity for non-strictly ordered rings. |
Change the positivity extension for multiplication to work on `IsOrderedRing` when proving nonnegativity instead of needing `IsStrictOrderedRing`.
Motivated by [#mathlib4 > `positivity` can't apply `mul_nonneg`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60positivity.60.20can't.20apply.20.60mul_nonneg.60/with/516270014).
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
29/37 |
Mathlib/Tactic/Positivity/Basic.lean,Mathlib/Tactic/Positivity/Core.lean |
2 |
4 |
['github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
nobody |
0-61613 17 hours ago |
0-61614 17 hours ago |
0-64920 18 hours |
| 24591 |
mans0954 author:mans0954 |
feature(RingTheory/RootsOfUnity/AlgebraicallyClosed): HasEnoughRootsOfUnity Circle n |
Construct an isomorphism `rootsOfUnity n Circle ≃* rootsOfUnity n ℂ` and use that fact that `rootsOfUnity n ℂ` has enough roots of unity to deduce that `rootsOfUnity n Circle` does as well.
This resolves a [TODO](https://github.com/leanprover-community/mathlib4/blob/529c13b5da1ff47aef41dbebd4d004fdf353aaf7/Mathlib/RingTheory/RootsOfUnity/AlgebraicallyClosed.lean#L16)
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
47/6 |
Mathlib/RingTheory/RootsOfUnity/AlgebraicallyClosed.lean,Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean |
2 |
7 |
['github-actions', 'loefflerd', 'mans0954'] |
nobody |
0-57273 15 hours ago |
4-36745 4 days ago |
9-64157 9 days |
| 24859 |
j-loreaux author:j-loreaux |
feat: `CFC.sqrt a = cfcₙ Real.sqrt a` |
Since `CFC.sqrt` is defined in terms of the `ℝ≥0` continuous functional calculus, this is slightly non-obvious, but follows from the uniqueness of the square root.
---
from [LeanOA](https://github.com/j-loreaux/LeanOA)
[](https://gitpod.io/from-referrer/)
|
t-analysis
easy
|
11/1 |
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean |
1 |
5 |
['eric-wieser', 'github-actions', 'j-loreaux'] |
nobody |
0-52525 14 hours ago |
1-906 1 day ago |
1-923 1 day |
| 24870 |
smmercuri author:smmercuri |
feat: `Field`, `FiniteDimensional` and `Algebra.IsSeparable` instances for `WithAbs` |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-analysis
|
14/1 |
Mathlib/Analysis/Normed/Field/WithAbs.lean |
1 |
1 |
['github-actions'] |
nobody |
0-46208 12 hours ago |
0-46215 12 hours ago |
0-46360 12 hours |
| 24872 |
smmercuri author:smmercuri |
feat: `apply` and `coe` results for `UniformSpace.Completion.mapRingHom` |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
9/0 |
Mathlib/Topology/Algebra/UniformRing.lean |
1 |
1 |
['github-actions'] |
nobody |
0-45987 12 hours ago |
0-45987 12 hours ago |
0-46036 12 hours |
| 24520 |
chrisflav author:chrisflav |
feat(Algebra/Pi): add `AlgEquiv.prodCongr` |
and related `AlgEquiv`s.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
125/41 |
Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/Algebra/Pi.lean,Mathlib/Algebra/Algebra/Prod.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Topology/LocallyConstant/Algebra.lean |
5 |
9 |
['Ruben-VandeVelde', 'chrisflav', 'eric-wieser', 'github-actions', 'mistarro'] |
nobody |
0-45720 12 hours ago |
12-84234 12 days ago |
13-10161 13 days |
| 24873 |
smmercuri author:smmercuri |
feat: `Subtype.map_ne` |
The restrictions to subtypes of two functions that never agree, also never agree.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
7/0 |
Mathlib/Data/Subtype.lean |
1 |
1 |
['github-actions'] |
nobody |
0-45647 12 hours ago |
0-45649 12 hours ago |
0-45699 12 hours |
| 24875 |
smmercuri author:smmercuri |
feat: injectivity of `InfinitePlace.embedding` |
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
15/0 |
Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-45512 12 hours ago |
0-45512 12 hours ago |
0-45567 12 hours |
| 24877 |
smmercuri author:smmercuri |
feat: predicates for extensions of complex embeddings |
If `L/K`, `ψ : K →+* ℂ`, `φ : L →+* ℂ` we define three predicates asserting ways that `φ` can extend `ψ`.
- `IsExtension ψ φ` : the restriction of `φ` to `K` is `ψ`.
- `IsMixedExtension ψ φ` : the restriction of `φ` to `K` is `ψ`, `ψ` has real image while `φ` has complex image.
- `IsUnmixedExtension ψ φ`: the restriction of `φ` to `K` is `ψ`, `ψ` has real image if and only if `φ` has real image.
`IsMixedExtension` and `IsUnmixedExtension` are the `ComplexEmbedding` analogues to ramified and unramified infinite places.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
91/0 |
Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean |
1 |
1 |
['github-actions'] |
nobody |
0-44863 12 hours ago |
0-44866 12 hours ago |
0-44920 12 hours |
| 24880 |
smmercuri author:smmercuri |
feat: predicate for ramified infinite places |
Adds `InfinitePlace.IsRamified` as a shorthand for `¬InfinitePlace.IsUnramified` plus basic API.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
16/0 |
Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean |
1 |
1 |
['github-actions'] |
nobody |
0-44273 12 hours ago |
0-44291 12 hours ago |
0-44337 12 hours |
| 24705 |
grunweg author:grunweg |
feat(workflows): automatically assign reviewers |
Once per day, automatically assign all proposed reviewers from the automatic assignment algorithm.
---
See [the github documentation](https://docs.github.com/en/rest/issues/assignees?apiVersion=2022-11-28#add-assignees-to-an-issue) for the assignment syntax.
[](https://gitpod.io/from-referrer/)
|
CI |
41/0 |
.github/workflows/auto_assign_reviewers.yaml |
1 |
3 |
['adomani', 'github-actions'] |
bryangingechen assignee:bryangingechen |
0-43372 12 hours ago |
2-15557 2 days ago |
2-15542 2 days |
| 22882 |
xroblot author:xroblot |
feat(NumberField/Units): add `regOfFamily` and refactor `regulator` |
This is a refactor of `NumberField.regulator`.
We introduce `regOfFamily` which is the regulator of a family of units indexed by `Fin (Units.rank K)`. It is equal to `0` if the family is not `isMaxRank`. This a `Prop` that says that the image of the family in the `logSpace K` is linearly independent and thus generates a full lattice. All the results about computing the `regulator` by some matrix determinant computation are now proved more generally for `regOfFamily`.
The `regulator` of a number field is still defined as the covolume of the `unitLattice` and we prove that is is also equal to `regOfFamily` of the system of fundamental units `fundSystem K`. Together with the results about computing `regOfFamily`, we recover that way the results about computing the regulator.
---
- [x] depends on: #22868
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
183/53 |
Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean,Mathlib/NumberTheory/NumberField/Units/Regulator.lean |
3 |
5 |
['alreadydone', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
0-42387 11 hours ago |
0-42407 11 hours ago |
56-63087 56 days |
| 24883 |
madvorak author:madvorak |
chore(Data/Matrix): `Matrix.submatrix` naming convention |
I'm suggesting this change for the following reasons:
(1) managing expectations — `r_reindex` looks more like a propositional argument at first glance
(2) the original naming does not do justice to its motivation — there is nothing called `r` and `c` here — it would need to be `row_reindex` and `col_reindex` or something like that (if we wanted to use the convention for naming constants even tho we are naming a variable here)
---
Old version:
https://github.com/leanprover-community/mathlib4/pull/24135 |
t-data |
11/11 |
Mathlib/Data/Matrix/ConjTranspose.lean,Mathlib/Data/Matrix/Defs.lean |
2 |
1 |
['github-actions'] |
nobody |
0-42282 11 hours ago |
0-42282 11 hours ago |
0-42273 11 hours |
| 23955 |
Louddy author:Louddy |
feat: Ideal.count_associates_eq |
Add variant of `UniqueFactorizationMonoid.count_normalizedFactors_eq` for associated Ideals.
This is convenient when you need to talk about an element as `a₀ = x ^ n * a`.
Note the file is slightly over the 1500 lines limit, I hope that is ok.
Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)>
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
35/1 |
Mathlib/RingTheory/DedekindDomain/Ideal.lean |
1 |
7 |
['Louddy', 'Ruben-VandeVelde', 'alreadydone', 'github-actions', 'grunweg'] |
kbuzzard assignee:kbuzzard |
0-41548 11 hours ago |
0-41548 11 hours ago |
27-42308 27 days |
| 22100 |
smmercuri author:smmercuri |
feat: two inequivalent absolute values have a `< 1` and `> 1` value |
- Two absolute values `v` and `w` are equivalent if and only if `v x < 1` exactly when `w x < 1`
- Two inequivalent absolute values `v` and `w` have a point `x` at which `1 < v x` and `w x < 1`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-analysis
label:t-algebra$ |
176/0 |
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Analysis/AbsoluteValue/Equivalence.lean |
2 |
6 |
['Paul-Lez', 'github-actions', 'smmercuri'] |
faenuccio assignee:faenuccio |
0-39274 10 hours ago |
26-77790 26 days ago |
57-65136 57 days |
| 24878 |
grunweg author:grunweg |
chore: add more deprecations |
Continuation of #24871; all commits were generated semi-automatically using the script in #24681.
---
Commits can be reviewed individually; I updated mk_all in a separate commit.
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
59/0 |
Mathlib.lean,Mathlib/CategoryTheory/FullSubcategory.lean,Mathlib/RingTheory/EisensteinCriterion.lean,Mathlib/RingTheory/Polynomial/Eisenstein/Generalized.lean,Mathlib/Tactic.lean,Mathlib/Tactic/ExtractLets.lean,Mathlib/Tactic/LiftLets.lean |
7 |
2 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
0-38583 10 hours ago |
0-38719 10 hours ago |
0-44755 12 hours |
| 24885 |
xroblot author:xroblot |
chore(NumberField): minor clean up and golf |
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
22/23 |
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean,Mathlib/NumberTheory/NumberField/Units/Basic.lean,Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean |
3 |
4 |
['Ruben-VandeVelde', 'github-actions', 'xroblot'] |
nobody |
0-37741 10 hours ago |
0-37741 10 hours ago |
0-41992 11 hours |
| 24887 |
Ruben-VandeVelde author:Ruben-VandeVelde |
chore: avoid Coe.coe in PowerSeries |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
4/6 |
Mathlib/RingTheory/PowerSeries/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-37546 10 hours ago |
0-37548 10 hours ago |
0-37605 10 hours |
| 24616 |
bwehlin author:bwehlin |
feat(MeasureTheory/Measure/Dirac): Dirac measure applied to a measurable set is either 0 or 1 |
The Dirac measure at a point `a`, applied to a set `s`, is either 0 or 1. This feature provides two if and only ifs that can be used to turn statements in terms of `\ne` into statements in terms of `=`, as well as a "0 or 1 theorem".
(The reason for adding these is to avoid having to simplify in terms of `Set.indicator` over and over while working with Dirac) |
new-contributor
t-measure-probability
|
15/0 |
Mathlib/MeasureTheory/Measure/Dirac.lean |
1 |
2 |
['bwehlin', 'github-actions'] |
nobody |
0-36448 10 hours ago |
9-4655 9 days ago |
9-4710 9 days |
| 22078 |
Louddy author:Louddy |
feat(SkewMonoidAlgebra): multiplication and algebraic instances |
# Multiplication and Algebraic Instances
In this PR, we introduce the definition of the skewed convolution product on `SkewMonoidAlgebra k G`. 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`.
We also introduce the associated algebraic instances.
## Context
This is the third part of a planned series of PRs aiming to formalise skew monoid algebras.
The PRs are split to ease the review process. The moral sum of these planned PRs is #10541.
The first and second part were #15878 and #19084.
Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)>
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-algebra
label:t-algebra$ |
453/45 |
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean |
1 |
57 |
['AntoineChambert-Loir', 'Louddy', 'github-actions', 'kbuzzard'] |
nobody |
0-36290 10 hours ago |
0-36290 10 hours ago |
72-56821 72 days |
| 24121 |
smorel394 author:smorel394 |
feat(RingTheory/Coalgebra/Equiv, RingTheory/Bialgebra/Equiv): constructors for coalgebra and bialgebra equivalences |
Add constructors for equivalences of coalgebras and bialgebras, similar to what already exists for equivalences of algebras:
- `CoalgEquiv.ofCoalgHom` constructs a `CoalgEquiv` from a `CoalgHom` that has an inverse;
- `CoalgEquiv.ofBijective` constructs a `CoalgEquiv` from a bijective `CoalgHom`;
- `BialgEquiv.ofBialgHom` constructs a `BialgEquiv` from a `CoalgHom` that has an inverse;
- `BialgEquiv.ofBijective` constructs a `BialgEquiv` from a bijective `BialgHom`.
Also add some `apply` and `coe` lemmas, following the same model as for `AlgEquiv`s.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
73/0 |
Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Coalgebra/Equiv.lean |
2 |
14 |
['github-actions', 'riccardobrasca', 'smorel394'] |
riccardobrasca assignee:riccardobrasca |
0-33846 9 hours ago |
28-5882 28 days ago |
28-5950 28 days |
| 24892 |
Ruben-VandeVelde author:Ruben-VandeVelde |
fix: add missing simps projections for ContinuousAddEquiv |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
1/0 |
Mathlib/Topology/Algebra/ContinuousMonoidHom.lean |
1 |
1 |
['github-actions'] |
nobody |
0-33609 9 hours ago |
0-33611 9 hours ago |
0-33661 9 hours |
| 24816 |
ciskiko author:ciskiko |
feat(GroupTheory): add Regular Wreath Product |
feat: add regular wreath product and some results; add iterated wreath product; add the isomorphism of iterated wreath product of Z_p to sylow p subgroup of S_{p^n}.
Needs some work simplifying final result.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
294/0 |
Mathlib.lean,Mathlib/GroupTheory/RegularWreathProduct.lean |
2 |
17 |
['ciskiko', 'github-actions', 'tb65536'] |
tb65536 assignee:tb65536 |
0-31547 8 hours ago |
1-29709 1 day ago |
1-54139 1 day |
| 24778 |
YaelDillies author:YaelDillies |
feat: `CommGrp`-valued Yoneda embedding |
From Toric
Co-authored-by: Andrew Yang
---
[](https://gitpod.io/from-referrer/)
|
toric
large-import
t-category-theory
|
60/6 |
Mathlib/Algebra/Category/Grp/Basic.lean,Mathlib/Algebra/Category/Grp/ForgetCorepresentable.lean,Mathlib/Algebra/Category/MonCat/Basic.lean,Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean |
4 |
3 |
['TwoFX', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
0-31525 8 hours ago |
0-31543 8 hours ago |
1-13230 1 day |
| 24876 |
kebekus author:kebekus |
feat: introduce the Proximity Function of Value Distribution Theory |
Define the "proximity function" attached to a meromorphic function defined on the complex plane. Also known as the "Nevanlinna Proximity Function", this is one of the three main functions used in Value Distribution Theory.
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.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
131/4 |
Mathlib.lean,Mathlib/Analysis/Complex/ValueDistribution/CountingFunction.lean,Mathlib/Analysis/Complex/ValueDistribution/ProximityFunction.lean,docs/references.bib |
4 |
3 |
['github-actions', 'jcommelin', 'kebekus'] |
nobody |
0-31279 8 hours ago |
0-45128 12 hours ago |
0-45179 12 hours |
| 24731 |
101damnations author:101damnations |
feat(Algebra/Category/ModuleCat/Monoidal/Basic): create simp set for unfolding the monoidal category structure on `ModuleCat` |
Occasionally it's useful to unfold the monoidal category structure on `ModuleCat` to the underlying `TensorProduct` definitions, and this involves multiple non-simp lemmas with long names. This PR creates a simp set `moduleCat_simps` comprising these lemmas.
---
I've also applied this simp set where relevant in mathlib - it doesn't have many use cases yet but I have subsequent PRs where it would be handy, e.g. #21732. I didn't reference monoidal stuff in the name in case it could include other `ModuleCat` lemmas later.
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-category-theory
label:t-algebra$ |
19/10 |
Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean,Mathlib/RepresentationTheory/Rep.lean,Mathlib/RingTheory/Coalgebra/TensorProduct.lean,Mathlib/Tactic/Attr/Register.lean |
5 |
10 |
['101damnations', 'YaelDillies', 'eric-wieser', 'fpvandoorn', 'github-actions', 'joelriou', 'leanprover-community-bot-assistant'] |
nobody |
0-29633 8 hours ago |
1-40235 1 day ago |
3-9862 3 days |
| 24167 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(Data/Fin/Tuple/Embedding): create embeddings of Fin Nat to types |
Define
* `Fin.Embedding.cons`, `Fin.Embedding.tail`
* `Fin.Embedding.snoc`, `Fin.Embedding.init`
* `Fin.Embedding.append`
analogously to `Fin.cons`, `Fin.snoc`, `Fin.append`.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
155/1 |
Mathlib.lean,Mathlib/Data/Fin/Tuple/Basic.lean,Mathlib/Data/Fin/Tuple/Embedding.lean,Mathlib/Order/Fin/Basic.lean |
4 |
22 |
['AntoineChambert-Loir', 'eric-wieser', 'github-actions'] |
riccardobrasca assignee:riccardobrasca |
0-29149 8 hours ago |
0-41644 11 hours ago |
26-3487 26 days |
| 24849 |
jano-wol author:jano-wol |
feat: simple lie algebras have irreducible root systems |
Simple lie algebras have irreducible root systems
---
PR shows that simple lie algebras have irreducible root systems.
This work is part of the framework: https://github.com/orgs/leanprover-community/projects/17
Issue link: https://github.com/leanprover-community/mathlib4/issues/22831
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
176/0 |
Mathlib/Algebra/Lie/Weights/RootSystem.lean |
1 |
1 |
['github-actions'] |
ocfnash assignee:ocfnash |
0-29146 8 hours ago |
1-14327 1 day ago |
1-14377 1 day |
| 24904 |
kim-em author:kim-em |
chore: use TreeMap in MLList/BestFirst and rw_search |
|
t-data |
14/13 |
Mathlib/Data/MLList/BestFirst.lean |
1 |
1 |
['github-actions'] |
nobody |
0-27454 7 hours ago |
0-27462 7 hours ago |
0-27513 7 hours |
| 24304 |
YaelDillies author:YaelDillies |
feat: continuous perfect pairings |
Andrew and I do not know what a continuous perfect pairing should be. It's certainly at least a map `M →ₗ[R] N →ₗ[R] R`, but we probably want it to be continuous in both arguments simultaneously, ie as a map `M × N → R`, otherwise it wouldn't induce a map `N → M →L[R] R`. We probably also want the fact that a continuous perfect pairing between `M` and `N` implies that `M` is the dual of `N` and vice-versa. That means we would need the two maps `M → N →[L] R` and `N → M →L[R] R` to be homeorphisms. We are currently only assuming that they are bijective, which is enough to show that the double dual of a proper cone is itself.
From Toric
Co-authored-by: Andrew Yang
---
[](https://gitpod.io/from-referrer/)
|
toric
t-topology
|
92/0 |
Mathlib.lean,Mathlib/Topology/Algebra/Module/PerfectPairing.lean |
2 |
5 |
['ADedecker', 'YaelDillies', 'erdOne', 'github-actions'] |
ADedecker assignee:ADedecker |
0-26979 7 hours ago |
21-39577 21 days ago |
21-39631 21 days |
| 24889 |
Kha author:Kha |
chore: do not include cache requests in build benchmark |
|
|
5/2 |
scripts/bench/temci-config.run.yml |
1 |
4 |
['Kha', 'github-actions', 'leanprover-bot'] |
nobody |
0-26201 7 hours ago |
0-36036 10 hours ago |
0-36020 10 hours |
| 24352 |
grunweg author:grunweg |
feat(L1Space/IntegrableOn): generalise more lemmas to enorm |
Future possibilities include generalising norm_le_pi_norm to enorm, and generalising HasFiniteIntegral.of_finite.
---
- [x] depends on: #24343
- [x] depends on: #24355 (generalising remaining theorems in LpSeminorm/Basic, part 1)
- [x] depends on: #24356 (generalising remaining theorems in LpSeminorm/Basic, part 2)
- [x] depends on: #24640 (LpSeminorm/Basic and LpSpace/Basic)
- [x] depends on: #24481
- [x] depends on: #24482
- [x] depends on: #24818
- [x] depends on: #24820
[](https://gitpod.io/from-referrer/)
|
carleson
t-measure-probability
|
135/107 |
Counterexamples/Phillips.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/SpecialFunctions/Integrals.lean,Mathlib/MeasureTheory/Covering/Differentiation.lean,Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean,Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean,Mathlib/MeasureTheory/Function/L1Space/Integrable.lean,Mathlib/MeasureTheory/Integral/Average.lean,Mathlib/MeasureTheory/Integral/Bochner/FundThmCalculus.lean,Mathlib/MeasureTheory/Integral/Bochner/Set.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean,Mathlib/MeasureTheory/Integral/PeakFunction.lean,Mathlib/Probability/ConditionalExpectation.lean |
16 |
10 |
['github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-bot-assistant', 'leanprover-community-mathlib4-bot', 'mathlib4-dependent-issues-bot'] |
nobody |
0-24702 6 hours ago |
0-24702 6 hours ago |
1-10427 1 day |
| 21522 |
riccardobrasca author:riccardobrasca |
feat: add Mathlib.RingTheory.DedekindDomain.Instances |
We add a new file `Mathlib.RingTheory.DedekindDomain.Instances` containing various instances that are useful to work with the localization a prime of an extension of Dedekind domains. As a practical example we golf a tedious proof in `Mathlib.RingTheory.Ideal/Norm.RelNorm`
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
253/71 |
Mathlib.lean,Mathlib/RingTheory/DedekindDomain/Different.lean,Mathlib/RingTheory/DedekindDomain/Instances.lean,Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean,Mathlib/RingTheory/Ideal/Norm/RelNorm.lean,Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean,Mathlib/RingTheory/Localization/AtPrime.lean,Mathlib/RingTheory/Localization/Basic.lean,Mathlib/RingTheory/Localization/LocalizationLocalization.lean,Mathlib/RingTheory/RingHom/Finite.lean,Mathlib/RingTheory/Trace/Quotient.lean |
11 |
34 |
['YaelDillies', 'erdOne', 'fpvandoorn', 'github-actions', 'riccardobrasca'] |
nobody |
0-23213 6 hours ago |
0-23221 6 hours ago |
66-55794 66 days |
| 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
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-analysis
t-number-theory
label:t-algebra$ |
543/2 |
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Analysis/AbsoluteValue/Equivalence.lean,Mathlib/Analysis/Normed/Ring/WithAbs.lean,Mathlib/NumberTheory/NumberField/AdeleRing.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean |
5 |
1 |
['github-actions'] |
nobody |
0-22829 6 hours ago |
0-40132 11 hours ago |
11-63715 11 days |
| 24706 |
riccardobrasca author:riccardobrasca |
feat: add RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_le_pow_inertiaDeg_of_mem_primesOver_of_mem_Icc |
We improve the statement of `RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_mem_primesOver_of_le` to `RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_le_pow_inertiaDeg_of_mem_primesOver_of_mem_Icc`: it is enough to only test primes `p` and ideals `P` such that `p ^ ((span {p}).inertiaDeg P` is less than Minkowski's bound.
We also improve the structure of the file.
---
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
t-algebra
t-number-theory
label:t-algebra$ |
88/50 |
Mathlib/NumberTheory/NumberField/ClassNumber.lean,Mathlib/NumberTheory/RamificationInertia/Basic.lean |
2 |
15 |
['faenuccio', 'github-actions', 'riccardobrasca'] |
faenuccio assignee:faenuccio |
0-22144 6 hours ago |
0-22144 6 hours ago |
4-3740 4 days |
| 24836 |
RemyDegenne author:RemyDegenne |
feat(MeasureTheory): characteristic function in a Banach space |
Define `charFunCLM μ L`, the characteristic function of a measure `μ` at `L : E →L[ℝ] ℝ` in a normed space `E`. This is the integral `∫ v, exp (L v * I) ∂μ`.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
118/6 |
Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean,Mathlib/MeasureTheory/Measure/CharacteristicFunction.lean,Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean |
3 |
1 |
['github-actions'] |
nobody |
0-21995 6 hours ago |
1-38550 1 day ago |
1-38535 1 day |
| 24856 |
FMLJohn author:FMLJohn |
feat(Topology/Subbasis): prove Alexander Subbasis Theorem |
Prove the Alexander Subbasis Theorem: if `X` has a topology `T` and `T = generateFrom S`, then `X` is compact if any open cover of `X` with elements in `S` has a finite subcover.
---
[](https://gitpod.io/from-referrer/) |
maintainer-merge
t-topology
|
39/0 |
Mathlib/Topology/Compactness/Compact.lean |
1 |
25 |
['FMLJohn', 'YaelDillies', 'alreadydone', 'erdOne', 'github-actions', 'jcommelin'] |
nobody |
0-21371 5 hours ago |
0-21371 5 hours ago |
0-74743 20 hours |
| 24311 |
YaelDillies author:YaelDillies |
chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` |
From Toric
---
- [x] depends on: #24312
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
63/29 |
Mathlib/Algebra/Group/Torsion.lean,Mathlib/Combinatorics/Additive/CauchyDavenport.lean,Mathlib/GroupTheory/Order/Min.lean,Mathlib/GroupTheory/Torsion.lean,Mathlib/Topology/Instances/ZMultiples.lean |
5 |
5 |
['YaelDillies', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
0-21356 5 hours ago |
0-21356 5 hours ago |
0-34686 9 hours |
| 22043 |
YaelDillies author:YaelDillies |
chore: shortcut instance for `Neg ℤˣ` |
This lets us avoid importing `Ring` in downstream files (most of the effect is to come).
---
[](https://gitpod.io/from-referrer/)
|
file-removed
t-algebra
label:t-algebra$ |
20/47 |
Mathlib.lean,Mathlib/Algebra/GCDMonoid/Nat.lean,Mathlib/Algebra/Group/Int/Units.lean,Mathlib/Algebra/Order/Ring/Abs.lean,Mathlib/Algebra/Ring/Int/Units.lean,Mathlib/Algebra/Ring/NegOnePow.lean,Mathlib/Data/Fintype/Units.lean,Mathlib/Data/Int/AbsoluteValue.lean,Mathlib/Data/Int/Associated.lean,Mathlib/GroupTheory/HNNExtension.lean,Mathlib/NumberTheory/NumberField/Basic.lean,MathlibTest/Zify.lean |
12 |
15 |
['YaelDillies', 'eric-wieser', 'github-actions', 'j-loreaux', 'leanprover-community-bot-assistant', 'mathlib-bors'] |
nobody |
0-21099 5 hours ago |
0-21099 5 hours ago |
84-80535 84 days |
| 24905 |
grunweg author:grunweg |
chore(LocallyIntegrable): reorder hypotheses to enable dot notation |
In general, an explicit argument `MonotoneOn` to a lemma in the `MonotoneOn` namespace should come first, similarly for AntitoneOn. If there's a reason to deviate here, I'd love to be enlightened (and a comment to be added).
---
Split out of #24862.
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
11/11 |
Mathlib/Analysis/SumIntegralComparisons.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean |
2 |
3 |
['fpvandoorn', 'github-actions', 'grunweg'] |
nobody |
0-20190 5 hours ago |
0-21792 6 hours ago |
0-21783 6 hours |
| 24804 |
Moises-Herradon-Cueto author:Moises-Herradon-Cueto |
feat(CategoryTheory/Limits/Preserves/Shapes): show that if a functor preserves limits, so does `Over.post` |
If a functor `F` preserves limits (of a certain shape, finite, or of a certain size), then so does the induced functor on `Over` categories.
From Toric
Co-authored-by: Yaël Dillies
---
[](https://gitpod.io/from-referrer/)
|
toric
new-contributor
t-category-theory
|
146/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Preserves/Shapes/Over.lean,Mathlib/CategoryTheory/WithTerminal/Basic.lean |
3 |
4 |
['Moises-Herradon-Cueto', 'erdOne', 'github-actions'] |
nobody |
0-18450 5 hours ago |
2-32551 2 days ago |
2-32566 2 days |
| 24861 |
adomani author:adomani |
feat(deprecated module): automate the generation of deprecated modules |
This PR takes a step further in automating deprecated modules.
The command `#create_deprecated_modules (n)? (comment)? (write)?` generates deprecated modules.
Writing
```lean
#create_deprecated_modules 5 "These files are no longer relevant"
```
looks at the `lean` files in `Mathlib` that existed `4` commits ago
(i.e. the commit that you see with `git log -5`) and that are no longer present.
It shows how the corresponding deprecated modules should look like, using
`"These files are no longer relevant"` as the (optional) comment.
If the number of commits is not explicitly used, `#create_deprecated_modules` defaults to `2`,
namely, the commit just prior to the current one.
If the message is not explicitly used, `#create_deprecated_modules` defaults to
`"Auto-generated deprecation"`.
If you wish there to be no comment, use `#create_deprecated_modules 5 ""`.
Note that the command applies the *same* comment to all the files that it generates.
Finally, if everything looks correct, adding a final `write` actually generates the files:
```lean
#create_deprecated_modules 5 "These files are no longer relevant" write
```
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
181/0 |
scripts/README.md,scripts/create_deprecated_modules.lean |
2 |
31 |
['adomani', 'github-actions', 'grunweg'] |
grunweg assignee:grunweg |
0-17088 4 hours ago |
0-19825 5 hours ago |
0-75506 20 hours |
| 24891 |
YaelDillies author:YaelDillies |
feat: `M ≃ₗ[R] (Fin (Module.finrank R M) → R)` for `M` a finite `R`-module |
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
13/3 |
Mathlib/LinearAlgebra/Dimension/Free.lean,Mathlib/LinearAlgebra/FreeModule/Basic.lean,Mathlib/LinearAlgebra/FreeModule/Finite/Basic.lean |
3 |
7 |
['YaelDillies', 'eric-wieser', 'github-actions'] |
nobody |
0-16079 4 hours ago |
0-18034 5 hours ago |
0-34957 9 hours |
| 24869 |
urkud author:urkud |
feat(Deriv/Shift): add `derivWithin_comp_neg` etc |
I'm using `derivWithin_comp_const_sub` in #24754.
It increases imports of 1 file by 35 and adds 1 file to imports of ~200 files.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-analysis
|
34/12 |
Mathlib/Analysis/Calculus/Deriv/CompMul.lean,Mathlib/Analysis/Calculus/Deriv/Shift.lean,Mathlib/Analysis/Calculus/FDeriv/Equiv.lean |
3 |
1 |
['github-actions'] |
nobody |
0-8736 2 hours ago |
0-46879 13 hours ago |
0-46936 13 hours |
| 24344 |
erdOne author:erdOne |
feat: miscellaneous lemmas about transcedence bases |
---
- [x] depends on: #24806
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
199/11 |
Mathlib/Algebra/Algebra/Basic.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean,Mathlib/FieldTheory/PrimitiveElement.lean,Mathlib/FieldTheory/PurelyInseparable/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableClosure.lean,Mathlib/LinearAlgebra/Dimension/Basic.lean,Mathlib/LinearAlgebra/Dimension/Free.lean,Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean,Mathlib/RingTheory/AlgebraicIndependent/Basic.lean,Mathlib/RingTheory/AlgebraicIndependent/Defs.lean,Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean,Mathlib/RingTheory/Norm/Basic.lean |
14 |
33 |
['acmepjz', 'alreadydone', 'erdOne', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
alreadydone assignee:alreadydone |
0-8460 2 hours ago |
0-78796 21 hours ago |
18-75935 18 days |
| 24696 |
101damnations author:101damnations |
refactor(Algebra/Homology/ShortComplex/ModuleCat, RepresentationTheory/GroupCohomology/*): unfold `CategoryTheory.ShortComplex.moduleCatLeftHomologyData` less eagerly |
`ShortComplex.moduleCatLeftHomologyData` represents the homology of a short complex in `ModuleCat` as a concrete quotient of a `LinearMap.ker` by a `LinearMap.range`. When working on the level of linear maps - i.e. `ModuleCat.Hom.hom` of a morphism in `ModuleCat` - simp lemmas unfolding this concrete definition are useful. But when reasoning about morphisms in `ModuleCat` it seems handy not to unfold the definition, so that `simp` can apply the general `LeftHomologyData` API.
To that end, this PR replaces simp lemmas `ShortComplex.moduleCatLeftHomologyData_i, ShortComplex.moduleCatLeftHomologyData_π` with their linear map versions, `ShortComplex.moduleCatLeftHomologyData_i_hom, ShortComplex.moduleCatLeftHomologyData_π_hom`.
It also rephrases declarations about `ModuleCat` morphisms in the group cohomology folder in terms of `ShortComplex.moduleCatLeftHomologyData` rather than unfolding.
Deletions:
- CategoryTheory.ShortComplex.moduleCatHomology
- CategoryTheory.ShortComplex.moduleCatHomologyπ
- CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i
- CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π
- CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'
---
I hope this seems reasonable - I've found it handy personally.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
111/78 |
Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean,Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean,Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean |
3 |
10 |
['101damnations', 'erdOne', 'github-actions', 'kbuzzard'] |
nobody |
0-7461 2 hours ago |
0-11748 3 hours ago |
2-83187 2 days |
| 24254 |
Louddy author:Louddy |
feat: valuation on RatFunc which is trivial on constants |
Given a valuation `v` on `RatFunc K` that is trivial on the constants `K`, the valuation on `RatFunc.X` determines to some degree the valuation on any `p : Polynomial K`.
These are important in the context of Ostrowski's theorem for `RatFunc K`.
Note that the condition that the valuation is trivial on constants is automatically fulfilled when `K` is finite.
Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)>
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
73/0 |
Mathlib/FieldTheory/RatFunc/AsPolynomial.lean |
1 |
24 |
['Louddy', 'faenuccio', 'github-actions', 'mariainesdff'] |
nobody |
0-7057 1 hour ago |
0-39443 10 hours ago |
1-32946 1 day |
| 24390 |
YaelDillies author:YaelDillies |
chore: rename `ChosenFiniteProducts` to `CartesianMonoidalCategory` |
Now that `ChosenFiniteProducts` extends `MonoidalCategory`, the name `ChosenFiniteProducts` is less relevant. `CartesianMonoidalCategory` is a better name for this class.
From Toric
---
- [x] depends on: #24399
- [x] depends on: #24592
- [x] depends on: #24679
- [x] depends on: #24680
[](https://gitpod.io/from-referrer/)
|
file-removed
toric
t-category-theory
|
321/355 |
Mathlib.lean,Mathlib/Algebra/Category/Grp/CartesianMonoidal.lean,Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/Pullbacks.lean,Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean,Mathlib/CategoryTheory/Closed/Cartesian.lean,Mathlib/CategoryTheory/Closed/Functor.lean,Mathlib/CategoryTheory/Closed/Ideal.lean,Mathlib/CategoryTheory/Closed/Types.lean,Mathlib/CategoryTheory/Closed/Zero.lean,Mathlib/CategoryTheory/Distributive/Cartesian.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Cat.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/CommGrp_.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/CommMon_.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Comon_.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/FunctorCategory.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/InfSemilattice.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Mod_.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Over.lean,Mathlib/CategoryTheory/Monoidal/CommGrp_.lean,Mathlib/CategoryTheory/Monoidal/Grp_.lean,Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean,Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean,Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean,Mathlib/CategoryTheory/Monoidal/Types/Basic.lean,Mathlib/CategoryTheory/Preadditive/CommGrp_.lean,Mathlib/CategoryTheory/Sites/CartesianClosed.lean,Mathlib/CategoryTheory/Sites/CartesianMonoidal.lean,Mathlib/CategoryTheory/Sites/ChosenFiniteProducts.lean,Mathlib/Condensed/CartesianClosed.lean,Mathlib/Condensed/Light/CartesianClosed.lean |
35 |
9 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
0-4926 1 hour ago |
0-11517 3 hours ago |
0-11512 3 hours |
| 24823 |
eric-wieser author:eric-wieser |
refactor: add `hom` lemmas for the `MonoidalCategory` structure on `ModuleCat` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
153/141 |
Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean,Mathlib/Algebra/Category/FGModuleCat/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean,Mathlib/CategoryTheory/Monoidal/Internal/Module.lean,Mathlib/CategoryTheory/Monoidal/Types/Basic.lean,Mathlib/RepresentationTheory/Rep.lean,Mathlib/RingTheory/Coalgebra/TensorProduct.lean |
13 |
4 |
['YaelDillies', 'eric-wieser', 'github-actions', 'joelriou'] |
101damnations assignee:101damnations |
0-4404 1 hour ago |
0-4404 1 hour ago |
0-4389 1 hour |
| 24909 |
Komyyy author:Komyyy |
feat: tychonoff space ↔ the inclusion map to Stone-Čech compactification is embedding |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
63/5 |
Mathlib/Topology/Separation/CompletelyRegular.lean,Mathlib/Topology/StoneCech.lean |
2 |
1 |
['github-actions'] |
nobody |
0-3054 50 minutes ago |
0-3054 50 minutes ago |
0-3039 50 minutes |
| 22457 |
Komyyy author:Komyyy |
feat: the Ackermann function is computable |
It had been proved that Ackermann function is not primitive recursive, but not been proved that it's computable.
I proved that.
---
- [x] depends on: #24811
[](https://gitpod.io/from-referrer/)
|
t-computability |
96/23 |
Mathlib/Computability/Ackermann.lean,Mathlib/Computability/Halting.lean,Mathlib/Computability/PartrecCode.lean |
3 |
18 |
['Komyyy', 'YaelDillies', 'bryangingechen', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp'] |
bryangingechen assignee:bryangingechen |
0-3039 50 minutes ago |
0-4545 1 hour ago |
69-70698 69 days |
| 24911 |
Komyyy author:Komyyy |
style: rename `t2Quotient` to `T2Quotient` |
`t2Quotient X` is a type so should be capitalized.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
52/32 |
Mathlib/Topology/Separation/Hausdorff.lean,Mathlib/Topology/StoneCech.lean |
2 |
1 |
['github-actions'] |
nobody |
0-777 12 minutes ago |
0-777 12 minutes ago |
0-762 12 minutes |
| 22884 |
tannerduve author:tannerduve |
feat(Computability/TuringDegree): define oracle computability and Turing degrees |
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.
Co-authored-by: Elan Roth
---
### Breaking Changes
None.
### Dependencies
None. |
maintainer-merge
t-computability
new-contributor
|
216/0 |
Mathlib.lean,Mathlib/Computability/TuringDegree.lean,docs/references.bib |
3 |
61 |
['YaelDillies', 'b-mehta', 'github-actions', 'tannerduve', 'tristan-f-r'] |
nobody |
0-727 12 minutes ago |
0-925 15 minutes ago |
59-57646 59 days |