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 |
63-73768 2 months ago |
97-76229 3 months ago |
106-57532 106 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-28901 1 month ago |
43-28901 1 month ago |
47-17076 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 |
38-78888 1 month ago |
39-23886 1 month ago |
39-23906 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 |
35-55707 1 month ago |
37-50775 1 month ago |
84-37600 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 |
34-77477 1 month ago |
70-81340 2 months ago |
72-25211 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 |
29-56487 29 days ago |
29-57788 29 days ago |
29-57842 29 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-28939 29 days ago |
29-32751 29 days ago |
29-32733 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 |
28-84268 28 days ago |
29-8906 29 days ago |
29-8888 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-34766 28 days ago |
28-65416 28 days ago |
40-32337 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-11660 28 days ago |
28-11660 28 days ago |
36-43912 36 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 |
27-73520 27 days ago |
27-73538 27 days ago |
83-34260 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-36803 26 days ago |
26-36803 26 days ago |
69-17734 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-31324 26 days ago |
37-29227 1 month ago |
211-53988 211 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-29571 25 days ago |
35-3172 1 month ago |
47-37444 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 |
24-54937 24 days ago |
29-36951 29 days ago |
29-37002 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-19685 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 |
23-83740 23 days ago |
31-38183 1 month ago |
32-14800 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 |
23-50258 23 days ago |
23-65318 23 days ago |
23-65308 23 days |
| 23338 |
WilliamCoram author:WilliamCoram |
feat: restricted power series form a ring |
We define restricted powerseries over a normed ring R, and show they form a ring when R has the ultrametric property.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-number-theory
|
186/0 |
Mathlib.lean,Mathlib/RingTheory/PowerSeries/Restricted.lean |
2 |
17 |
['Paul-Lez', 'WilliamCoram', 'github-actions', 'grunweg'] |
nobody |
23-33944 23 days ago |
48-62071 1 month ago |
48-62192 48 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-25539 22 days ago |
55-73560 1 month ago |
55-75454 55 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-39040 21 days ago |
21-39105 21 days ago |
21-39088 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 |
20-47977 20 days ago |
20-47980 20 days ago |
20-49571 20 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-18749 20 days ago |
20-18749 20 days ago |
20-40229 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-4120 20 days ago |
20-38502 20 days ago |
22-22727 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 |
19-80854 19 days ago |
19-82646 19 days ago |
32-83168 32 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 |
19-46104 19 days ago |
19-83867 19 days ago |
81-65612 81 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-32115 18 days ago |
18-32115 18 days ago |
39-19930 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 |
17-41403 17 days ago |
17-41403 17 days ago |
17-41462 17 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 |
16-71919 16 days ago |
16-73903 16 days ago |
20-61334 20 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 |
16-70617 16 days ago |
28-42682 28 days ago |
68-36289 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 |
16-64705 16 days ago |
20-54943 20 days ago |
20-80183 20 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 |
16-54929 16 days ago |
16-55085 16 days ago |
16-55078 16 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-40695 16 days ago |
69-72598 2 months ago |
69-72579 69 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-17530 16 days ago |
16-26223 16 days ago |
16-26206 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 |
15-79157 15 days ago |
15-79173 15 days ago |
52-35333 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 |
14-65918 14 days ago |
14-65918 14 days ago |
15-53275 15 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 |
14-62792 14 days ago |
14-62792 14 days ago |
14-68175 14 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 |
14-59978 14 days ago |
14-59979 14 days ago |
39-80563 39 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 |
14-55506 14 days ago |
14-65497 14 days ago |
14-65550 14 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-33428 14 days ago |
33-49318 1 month ago |
33-50115 33 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-33355 14 days ago |
14-33355 14 days ago |
30-52799 30 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-19253 14 days ago |
16-40443 16 days ago |
21-30044 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 |
13-67295 13 days ago |
13-68373 13 days ago |
13-68439 13 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 |
12-75819 12 days ago |
12-75882 12 days ago |
12-75865 12 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 |
12-67378 12 days ago |
12-67378 12 days ago |
14-25338 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 |
12-64683 12 days ago |
12-66812 12 days ago |
12-74950 12 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 |
12-54746 12 days ago |
12-54746 12 days ago |
12-54798 12 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 |
12-47838 12 days ago |
12-48039 12 days ago |
12-48094 12 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 |
12-45267 12 days ago |
12-47908 12 days ago |
21-33049 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-26667 12 days ago |
12-58758 12 days ago |
36-75603 36 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 |
11-81377 11 days ago |
11-81377 11 days ago |
23-11549 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 |
11-76584 11 days ago |
11-76584 11 days ago |
11-84499 11 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 |
11-66543 11 days ago |
12-66824 12 days ago |
13-16361 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-27020 11 days ago |
11-32082 11 days ago |
47-77237 47 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-14750 11 days ago |
22-26131 22 days ago |
22-26115 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-13389 11 days ago |
12-57526 12 days ago |
12-57578 12 days |
| 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/)
|
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 |
14 |
['YaelDillies', 'eric-wieser', 'github-actions', 'j-loreaux', 'leanprover-community-bot-assistant', 'mathlib-bors'] |
nobody |
11-76 11 days ago |
11-93 11 days ago |
84-36773 84 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 |
10-84287 10 days ago |
10-84287 10 days ago |
43-64010 43 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 |
10-84275 10 days ago |
10-84275 10 days ago |
48-9342 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 |
10-81739 10 days ago |
10-82782 10 days ago |
38-57101 38 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 |
10-54338 10 days ago |
10-83295 10 days ago |
26-70937 26 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 |
10-51410 10 days ago |
10-68480 10 days ago |
12-36779 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 |
10-47256 10 days ago |
10-47272 10 days ago |
21-29873 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 |
10-44873 10 days ago |
11-62940 11 days ago |
11-78450 11 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-36687 10 days ago |
10-36695 10 days ago |
10-36678 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-15584 10 days ago |
10-15639 10 days ago |
10-15633 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-11509 10 days ago |
79-13151 2 months ago |
79-13276 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-5880 10 days ago |
10-15098 10 days ago |
10-15091 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 |
9-66153 9 days ago |
9-66177 9 days ago |
9-66160 9 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-798 9 days ago |
10-1151 10 days ago |
10-1198 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 |
8-84650 8 days ago |
47-63870 1 month ago |
47-71700 47 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 |
8-74313 8 days ago |
13-54462 13 days ago |
13-54456 13 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 |
8-70276 8 days ago |
29-46667 29 days ago |
53-36118 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 |
8-57964 8 days ago |
8-57964 8 days ago |
8-58023 8 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 |
8-49925 8 days ago |
16-47818 16 days ago |
63-53902 63 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-37345 8 days ago |
8-37345 8 days ago |
13-45300 13 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-12999 8 days ago |
12-21685 12 days ago |
26-35988 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-4560 8 days ago |
10-5902 10 days ago |
36-50104 36 days |
| 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 |
1 |
['github-actions'] |
nobody |
7-70323 7 days ago |
8-45820 8 days ago |
8-45874 8 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 |
7-55069 7 days ago |
7-55088 7 days ago |
32-52223 32 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 |
7-52952 7 days ago |
21-68095 21 days ago |
40-69558 40 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 |
7-49975 7 days ago |
8-5008 8 days ago |
8-5058 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 |
6-84670 6 days ago |
6-84686 6 days ago |
11-78944 11 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 |
6-80577 6 days ago |
6-80577 6 days ago |
18-82254 18 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 |
6-79235 6 days ago |
6-79309 6 days ago |
19-26851 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 |
6-78613 6 days ago |
6-78657 6 days ago |
6-80651 6 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 |
6-76817 6 days ago |
15-20988 15 days ago |
15-21522 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 |
6-74399 6 days ago |
6-74399 6 days ago |
70-48065 70 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 |
6-66734 6 days ago |
6-66735 6 days ago |
6-66798 6 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 |
6-55663 6 days ago |
7-69806 7 days ago |
14-65978 14 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$ |
443/42 |
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean |
1 |
52 |
['AntoineChambert-Loir', 'Louddy', 'github-actions', 'kbuzzard'] |
nobody |
6-52657 6 days ago |
35-53394 1 month ago |
72-17106 72 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 |
6-43646 6 days ago |
6-43646 6 days ago |
6-56562 6 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-22709 6 days ago |
10-46663 10 days ago |
31-84108 31 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-8130 6 days ago |
6-8146 6 days ago |
6-8199 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 |
5-85023 5 days ago |
42-3204 1 month ago |
43-34991 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 |
5-84847 5 days ago |
70-49092 2 months ago |
70-49081 70 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 |
5-84580 5 days ago |
25-52263 25 days ago |
25-52317 25 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 |
5-83018 5 days ago |
5-83018 5 days ago |
24-60490 24 days |
| 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/)
|
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 |
31 |
['YaelDillies', 'erdOne', 'github-actions', 'riccardobrasca'] |
nobody |
5-78694 5 days ago |
6-69775 6 days ago |
66-10558 66 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 |
5-78195 5 days ago |
6-25536 6 days ago |
60-44155 60 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 |
5-64431 5 days ago |
25-72858 25 days ago |
73-66173 73 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 |
5-64397 5 days ago |
64-54148 2 months ago |
64-54198 64 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 |
5-64319 5 days ago |
26-36763 26 days ago |
36-85580 36 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 |
5-64303 5 days ago |
29-74737 29 days ago |
29-74719 29 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 |
5-61689 5 days ago |
25-35194 25 days ago |
63-66797 63 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 |
5-61676 5 days ago |
22-46956 22 days ago |
22-48478 22 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 |
5-61488 5 days ago |
43-54661 1 month ago |
43-54712 43 days |
| 23184 |
mariainesdff author:mariainesdff |
feat(Analysis/Normed/Unbundled/AlgNormOfAut): add algNormOfAut |
Let `K` be a nonarchimedean normed field and `L/K` be a finite extension. We show that the function `L → ℝ` sending `x : L` to the maximum of `‖ σ x ‖` over all `σ : L ≃ₐ[K] L` is an algebra norm on `L`. We also prove that this algebra norm is power multiplicative, nonarchimedean, and extends the norm on `K`.
---
- [x] depends on: #23178
[](https://gitpod.io/from-referrer/)
|
t-analysis
t-number-theory
|
145/0 |
Mathlib.lean,Mathlib/Analysis/Normed/Unbundled/AlgNormOfAut.lean |
2 |
14 |
['erdOne', 'github-actions', 'kbuzzard', 'mariainesdff', 'mathlib4-dependent-issues-bot', 'pechersky'] |
nobody |
5-60563 5 days ago |
15-56589 15 days ago |
15-57270 15 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 |
5-58025 5 days ago |
41-25729 1 month ago |
46-52370 46 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 |
5-57810 5 days ago |
20-47973 20 days ago |
21-58022 21 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 |
5-55376 5 days ago |
5-55376 5 days ago |
6-16065 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 |
5-47457 5 days ago |
5-47520 5 days ago |
5-47504 5 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 |
5-44309 5 days ago |
7-48364 7 days ago |
57-5854 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-36599 5 days ago |
49-55954 1 month ago |
83-41051 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-36105 5 days ago |
5-46886 5 days ago |
5-46934 5 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-29777 5 days ago |
31-71626 1 month ago |
31-71678 31 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$ |
174/0 |
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Analysis/AbsoluteValue/Equivalence.lean |
2 |
6 |
['Paul-Lez', 'github-actions', 'smmercuri'] |
faenuccio assignee:faenuccio |
5-27645 5 days ago |
26-32555 26 days ago |
57-19900 57 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-27562 5 days ago |
39-40199 1 month ago |
39-40250 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-27431 5 days ago |
33-22002 1 month ago |
33-22050 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-19779 5 days ago |
10-84359 10 days ago |
12-65912 12 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-6159 5 days ago |
5-53995 5 days ago |
5-54049 5 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 |
4-84343 4 days ago |
36-49874 1 month ago |
36-51665 36 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 |
4-77573 4 days ago |
4-78171 4 days ago |
4-78155 4 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 |
4-68360 4 days ago |
66-42804 2 months ago |
97-5052 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 |
4-68290 4 days ago |
41-61944 1 month ago |
44-8944 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 |
4-68182 4 days ago |
80-13281 2 months ago |
80-13272 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 |
4-68156 4 days ago |
59-25539 1 month ago |
64-26074 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 |
4-66309 4 days ago |
29-67579 29 days ago |
29-67632 29 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 |
4-66222 4 days ago |
51-40896 1 month ago |
99-60584 99 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 |
4-63873 4 days ago |
4-63873 4 days ago |
35-6264 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 |
4-61229 4 days ago |
42-42682 1 month ago |
81-9229 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 |
4-60350 4 days ago |
4-62332 4 days ago |
4-62381 4 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 |
4-59578 4 days ago |
4-59578 4 days ago |
4-59633 4 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 |
4-59107 4 days ago |
49-25151 1 month ago |
49-25195 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 |
4-56554 4 days ago |
4-67542 4 days ago |
4-67653 4 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 |
4-50620 4 days ago |
6-83222 6 days ago |
6-83272 6 days |
| 24679 |
YaelDillies author:YaelDillies |
refactor: move the construction of `ChosenFiniteProducts` from finite products with `ChosenFiniteProducts` |
Now that `ChosenFiniteProducts` extends `MonoidalCategory`, there is no point having the `MonoidalCategory` version separate from the `ChosenFiniteProducts` one.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-category-theory
|
125/296 |
Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean,Mathlib/CategoryTheory/ChosenFiniteProducts.lean,Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean,Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean |
4 |
2 |
['erdOne', 'github-actions'] |
nobody |
4-49976 4 days ago |
5-59552 5 days ago |
5-59551 5 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 |
4-47870 4 days ago |
4-71614 4 days ago |
18-77449 18 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 |
4-47325 4 days ago |
4-47347 4 days ago |
23-18339 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 |
4-41804 4 days ago |
5-46207 5 days ago |
5-46191 5 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-34344 4 days ago |
5-59508 5 days ago |
58-34960 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-32764 4 days ago |
36-55447 1 month ago |
39-18149 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-861 4 days ago |
4-3637 4 days ago |
8-44043 8 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 |
3-77698 3 days ago |
19-78694 19 days ago |
19-78754 19 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 |
3-77639 3 days ago |
54-40833 1 month ago |
54-40824 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 |
3-75002 3 days ago |
3-78510 3 days ago |
3-78494 3 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 |
3-74308 3 days ago |
3-74309 3 days ago |
3-75375 3 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 |
3-72791 3 days ago |
3-72791 3 days ago |
4-56081 4 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 |
3-72488 3 days ago |
3-72488 3 days ago |
53-22234 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 |
3-56929 3 days ago |
6-35452 6 days ago |
6-36480 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 |
3-55403 3 days ago |
3-55404 3 days ago |
36-46501 36 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 |
3-47165 3 days ago |
39-34214 1 month ago |
39-34261 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 |
3-45731 3 days ago |
3-45748 3 days ago |
5-16829 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 |
3-43010 3 days ago |
3-48983 3 days ago |
18-33022 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-29059 3 days ago |
3-36505 3 days ago |
3-36554 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-22399 3 days ago |
12-75367 12 days ago |
12-75350 12 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-20211 3 days ago |
3-20211 3 days ago |
3-53658 3 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-17740 3 days ago |
12-76730 12 days ago |
17-52891 17 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-15694 3 days ago |
3-16663 3 days ago |
20-73924 20 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-8433 3 days ago |
3-8433 3 days ago |
3-14143 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-7883 3 days ago |
3-8277 3 days ago |
7-35604 7 days |
| 24766 |
YaelDillies author:YaelDillies |
feat: minimal elements exist in well-founded orders |
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-order
|
19/0 |
Mathlib/Order/Minimal.lean |
1 |
1 |
['github-actions'] |
nobody |
3-349 3 days ago |
3-395 3 days ago |
3-395 3 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 |
2-83767 2 days ago |
2-83767 2 days ago |
14-60330 14 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 |
2-75818 2 days ago |
2-80796 2 days ago |
32-84390 32 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 |
2-75646 2 days ago |
2-75646 2 days ago |
24-43050 24 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 |
2-70906 2 days ago |
2-70906 2 days ago |
3-31337 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 |
2-67719 2 days ago |
2-67783 2 days ago |
2-67767 2 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 |
2-65765 2 days ago |
2-65814 2 days ago |
2-65798 2 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 |
2-63219 2 days ago |
7-38889 7 days ago |
12-27460 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 |
2-60341 2 days ago |
6-59930 6 days ago |
13-7949 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 |
2-58264 2 days ago |
2-58284 2 days ago |
2-71470 2 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 |
2-52640 2 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 |
2-50075 2 days ago |
2-50327 2 days ago |
2-52268 2 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 |
2-45553 2 days ago |
2-45554 2 days ago |
5-55333 5 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 |
2-42811 2 days ago |
2-42873 2 days ago |
2-42857 2 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-39483 2 days ago |
2-45434 2 days ago |
50-11255 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-38849 2 days ago |
2-38897 2 days ago |
13-27305 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-36261 2 days ago |
2-36476 2 days ago |
2-38519 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-34837 2 days ago |
39-60026 1 month ago |
42-43414 42 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-27000 2 days ago |
2-58565 2 days ago |
17-44000 17 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-23882 2 days ago |
2-24814 2 days ago |
68-24799 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-18353 2 days ago |
2-18353 2 days ago |
2-18409 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-9476 2 days ago |
2-9476 2 days ago |
25-33596 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-8249 2 days ago |
2-26374 2 days ago |
12-8848 12 days |
| 22915 |
pimotte author:pimotte |
feat(Combinatorics/SimpleGraph): Tutte's theorem |
Proves Tutte's theorem.
---
- [x] depends on: #22242
- [x] depends on: #22119
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
260/30 |
Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Operations.lean,Mathlib/Combinatorics/SimpleGraph/Tutte.lean,docs/1000.yaml |
5 |
45 |
['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'pimotte'] |
nobody |
2-1475 2 days ago |
2-1475 2 days ago |
8-49564 8 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 |
1-83200 1 day ago |
20-49113 20 days ago |
29-22208 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 |
1-83161 1 day ago |
37-85040 1 month ago |
37-85034 37 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 |
1-82251 1 day ago |
40-76672 1 month ago |
74-73167 74 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 |
1-68403 1 day ago |
1-80744 1 day ago |
2-7653 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 |
1-62377 1 day ago |
1-68011 1 day ago |
58-83032 58 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
t-algebra
t-number-theory
label:t-algebra$ |
84/50 |
Mathlib/NumberTheory/NumberField/ClassNumber.lean,Mathlib/NumberTheory/RamificationInertia/Basic.lean |
2 |
1 |
['github-actions'] |
nobody |
1-61182 1 day ago |
1-62181 1 day ago |
3-46255 3 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 |
1-59994 1 day ago |
1-63529 1 day ago |
5-82209 5 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 |
1-56302 1 day ago |
21-61545 21 days ago |
39-52537 39 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 |
1-54673 1 day ago |
1-83234 1 day ago |
1-86330 1 day |
| 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 |
1-54643 1 day ago |
1-61017 1 day ago |
1-66144 1 day |
| 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 |
1-45132 1 day ago |
3-52406 3 days ago |
68-48081 68 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 |
1-44368 1 day ago |
1-44397 1 day ago |
15-48546 15 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 |
1-44181 1 day ago |
1-44181 1 day ago |
1-44233 1 day |
| 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 |
1-41570 1 day ago |
1-41585 1 day ago |
20-19375 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-38229 1 day ago |
1-53538 1 day ago |
1-55120 1 day |
| 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-38123 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-37613 1 day ago |
206-59846 6 months ago* |
0-571 9 minutes* |
| 24693 |
101damnations author:101damnations |
refactor(RepresentationTheory/GroupCohomology/*): replace `nCochainsLequiv` with isomorphisms in `ModuleCat` for `n = 0, 1, 2` |
These are more useful as `ModuleCat` isos in practice.
---
I've also replaced the remaining `Lequiv`s in the group cohomology folder with `LEquiv`s since that spelling is more frequent in mathlib....
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
116/77 |
Mathlib/RepresentationTheory/GroupCohomology/Basic.lean,Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean,Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean |
3 |
6 |
['101damnations', 'erdOne', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
1-36854 1 day ago |
1-43487 1 day ago |
5-41351 5 days |
| 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-34251 1 day ago |
54-68707 1 month ago |
55-53163 55 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-33788 1 day ago |
82-66613 2 months ago |
85-29376 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-33738 1 day ago |
47-73965 1 month ago |
65-13720 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-33588 1 day ago |
1-33588 1 day ago |
1-72488 1 day |
| 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-33587 1 day ago |
20-17518 20 days ago |
20-17572 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-33549 1 day ago |
18-43481 18 days ago |
18-43532 18 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-33531 1 day ago |
17-40958 17 days ago |
17-41020 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-33228 1 day ago |
14-54821 14 days ago |
15-65651 15 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-32832 1 day ago |
1-32850 1 day ago |
1-32999 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-32547 1 day ago |
5-33120 5 days ago |
5-78477 5 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-31100 1 day ago |
2-15367 2 days ago |
2-15399 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-30469 1 day ago |
41-48752 1 month ago |
48-31888 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-27214 1 day ago |
21-71571 21 days ago |
21-72396 21 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-6302 1 day ago |
1-6302 1 day ago |
64-44090 64 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-5420 1 day ago |
1-5420 1 day ago |
1-11554 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-4489 1 day ago |
1-66423 1 day ago |
1-66472 1 day |
| 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 |
0-85991 23 hours ago |
1-8231 1 day ago |
1-8285 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 |
0-85532 23 hours ago |
0-85532 23 hours ago |
5-3964 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 |
0-84970 23 hours ago |
41-55866 1 month ago |
55-75867 55 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 |
0-84932 23 hours ago |
21-71064 21 days ago |
21-77822 21 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 |
0-84700 23 hours ago |
47-63890 1 month ago |
47-72565 47 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 |
0-84632 23 hours ago |
26-66012 26 days ago |
29-73132 29 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$ |
72/0 |
Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Coalgebra/Equiv.lean |
2 |
1 |
['github-actions'] |
riccardobrasca assignee:riccardobrasca |
0-82622 22 hours ago |
27-47047 27 days ago |
27-47115 27 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 |
0-81972 22 hours ago |
0-82265 22 hours ago |
0-82249 22 hours |
| 24775 |
JovanGerb author:JovanGerb |
chore(Order): use new `ge`/`gt` naming convention - Part 1 |
This is the first PR in a sequence of PRs to apply the new naming convention for order lemmas.
This PR changes all lemmas that have multiple occurences of `lt` or `le` in their name, and where `<` and `≤` have their arguments swapped in some places. Then those occurrences of `<` and `≤` are referred to as `gt` and `ge`.
The first commit is an automatic replacement of lemma names. The second commit adds deprecations for the renamed lemmas. Later commits are manual fixes. This should make it easy to review.
---
The naming convention is described at https://github.com/leanprover-community/leanprover-community.github.io/pull/626
[](https://gitpod.io/from-referrer/)
|
t-order |
969/944 |
Archive/Imo/Imo1959Q2.lean,Archive/Imo/Imo1960Q2.lean,Archive/Imo/Imo1986Q5.lean,Archive/Imo/Imo1988Q6.lean,Archive/Imo/Imo2015Q6.lean,Archive/Imo/Imo2024Q6.lean,Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean,Archive/Wiedijk100Theorems/CubingACube.lean,Archive/Wiedijk100Theorems/FriendshipGraphs.lean,Counterexamples/AharoniKorman.lean,Counterexamples/SeminormLatticeNotDistrib.lean,Mathlib/Algebra/BigOperators/Group/List/Basic.lean,Mathlib/Algebra/BigOperators/Intervals.lean,Mathlib/Algebra/BigOperators/Ring/Finset.lean,Mathlib/Algebra/CharP/Basic.lean,Mathlib/Algebra/CubicDiscriminant.lean,Mathlib/Algebra/GCDMonoid/Nat.lean,Mathlib/Algebra/GeomSum.lean,Mathlib/Algebra/Group/Subgroup/Finite.lean,Mathlib/Algebra/Group/Subgroup/Ker.lean,Mathlib/Algebra/Group/UniqueProds/Basic.lean,Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean,Mathlib/Algebra/Lie/Nilpotent.lean,Mathlib/Algebra/LinearRecurrence.lean,Mathlib/Algebra/Module/PID.lean,Mathlib/Algebra/Module/Submodule/Map.lean,Mathlib/Algebra/Order/AddTorsor.lean,Mathlib/Algebra/Order/Archimedean/Basic.lean,Mathlib/Algebra/Order/Archimedean/IndicatorCard.lean,Mathlib/Algebra/Order/BigOperators/Group/List.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/CompleteField.lean,Mathlib/Algebra/Order/Field/Basic.lean,Mathlib/Algebra/Order/Floor/Div.lean,Mathlib/Algebra/Order/Floor/Semiring.lean,Mathlib/Algebra/Order/Group/Abs.lean,Mathlib/Algebra/Order/Group/Unbundled/Basic.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean,Mathlib/Algebra/Order/Interval/Set/Group.lean,Mathlib/Algebra/Order/Ring/Basic.lean,Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean,Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean,Mathlib/Algebra/Order/Round.lean,Mathlib/Algebra/Order/ToIntervalMod.lean,Mathlib/Algebra/Polynomial/CoeffList.lean,Mathlib/Algebra/Polynomial/Degree/Domain.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Algebra/Polynomial/Div.lean,Mathlib/Algebra/Polynomial/HasseDeriv.lean,Mathlib/Algebra/Ring/Divisibility/Lemmas.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/Analysis/Analytic/Basic.lean,Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Asymptotics/ExpGrowth.lean,Mathlib/Analysis/BoxIntegral/Partition/Filter.lean,Mathlib/Analysis/BoxIntegral/Partition/Split.lean,Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean,Mathlib/Analysis/Calculus/Darboux.lean,Mathlib/Analysis/Calculus/Deriv/ZPow.lean,Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean,Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean,Mathlib/Analysis/Complex/AbelLimit.lean,Mathlib/Analysis/Complex/PhragmenLindelof.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean,Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Analysis/Convex/Cone/InnerDual.lean,Mathlib/Analysis/Convex/Exposed.lean,Mathlib/Analysis/Convex/Function.lean,Mathlib/Analysis/Convex/Gauge.lean,Mathlib/Analysis/Convex/Integral.lean,Mathlib/Analysis/Convex/Radon.lean,Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean,Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean,Mathlib/Analysis/Convex/StrictConvexSpace.lean,Mathlib/Analysis/Convex/Uniform.lean,Mathlib/Analysis/Convolution.lean,Mathlib/Analysis/Fourier/FourierTransformDeriv.lean,Mathlib/Analysis/MellinTransform.lean,Mathlib/Analysis/Meromorphic/Order.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Field/Ultra.lean,Mathlib/Analysis/Normed/Group/AddCircle.lean,Mathlib/Analysis/Normed/Module/Ray.lean,Mathlib/Analysis/NormedSpace/Connected.lean,Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean,Mathlib/Analysis/NormedSpace/Pointwise.lean,Mathlib/Analysis/ODE/Gronwall.lean,Mathlib/Analysis/PSeries.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart/Isometric.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean |
439 |
1 |
['github-actions'] |
bryangingechen assignee:bryangingechen |
0-81718 22 hours ago |
0-81718 22 hours ago |
2-65907 2 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 |
112/6 |
Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean,Mathlib/MeasureTheory/Measure/CharacteristicFunction.lean,Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean |
3 |
1 |
['github-actions'] |
nobody |
0-79452 22 hours ago |
0-79715 22 hours ago |
0-79699 22 hours |
| 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 |
0-79196 21 hours ago |
2-63086 2 days ago |
4-12915 4 days |
| 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 |
4 |
['ADedecker', 'YaelDillies', 'erdOne', 'github-actions'] |
ADedecker assignee:ADedecker |
0-77989 21 hours ago |
20-80742 20 days ago |
20-80796 20 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 |
0-76554 21 hours ago |
7-32657 7 days ago |
7-33566 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 |
0-76446 21 hours ago |
0-76519 21 hours ago |
0-76503 21 hours |
| 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 |
0-76242 21 hours ago |
1-54224 1 day ago |
25-59621 25 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 |
0-75327 20 hours ago |
0-81750 22 hours ago |
1-53639 1 day |
| 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 |
0-73779 20 hours ago |
1-39885 1 day ago |
2-21901 2 days |
| 23254 |
mariainesdff author:mariainesdff |
feat(Algebra/Order/BigOperators/GroupWithZero/Multiset.lean): add multiset_prod_le_pow_card |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
26/2 |
Mathlib/Algebra/Order/BigOperators/GroupWithZero/List.lean,Mathlib/Algebra/Order/BigOperators/GroupWithZero/Multiset.lean |
2 |
15 |
['Ruben-VandeVelde', 'erdOne', 'github-actions', 'mariainesdff'] |
nobody |
0-73416 20 hours ago |
15-66125 15 days ago |
45-12658 45 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 |
0-70662 19 hours ago |
1-75082 1 day ago |
2-52185 2 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 |
0-64716 17 hours ago |
1-1184 1 day ago |
1-1168 1 day |
| 24811 |
Komyyy author:Komyyy |
style: rename `Nat.Partrec.Code.xxx_prim` to `primrec_xxx` |
---
[](https://gitpod.io/from-referrer/)
|
t-computability |
49/21 |
Mathlib/Computability/Halting.lean,Mathlib/Computability/PartrecCode.lean |
2 |
15 |
['Komyyy', 'YaelDillies', 'bryangingechen', 'github-actions'] |
nobody |
0-61844 17 hours ago |
1-57267 1 day ago |
1-63380 1 day |
| 24401 |
JovanGerb author:JovanGerb |
feat(Tactic/ToAdditive): check that existing additive declaration matches up |
When using `@[to_additive existing]`, we check that the expected additive type and the actual additive type are definitionally equal. If not, throw an error.
There are a few reasons why the warnings were showing up:
- The types don't match up because the arguments or universes are in the wrong order
- The types don't match up because `to_additive` is additivizing more expressions than it should. Tagging these with `to_additive` doesn't serve any purpose; unless the heuristics get improved. This is the scenario that leaves potential room for improvement in the implementation of `to_additive`.
- The types don't match up because the multiplicative version uses `Multiplicative` or the additive uses `Additive`, and the other version doesn't use this. Currently, `to_additive` cannot translate between this.
- The two lemmas are using the addition and multiplication of a shared ring/field structure. So it may look like a target for `to_additive`, but it really isn't.
This PR addresses all of these by fixing the statement or removing the tag.
This feature has been upstreamed from #21719
Co-authored-by: @bryangingechen
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
110/121 |
Mathlib/Algebra/Group/End.lean,Mathlib/Algebra/Group/Nat/Hom.lean,Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean,Mathlib/Algebra/Group/ULift.lean,Mathlib/Algebra/MvPolynomial/Eval.lean,Mathlib/Algebra/Order/Group/Synonym.lean,Mathlib/Algebra/Order/Interval/Basic.lean,Mathlib/Analysis/Normed/Group/Seminorm.lean,Mathlib/Combinatorics/Additive/DoublingConst.lean,Mathlib/Data/Int/Cast/Lemmas.lean,Mathlib/Data/Set/Pointwise/Support.lean,Mathlib/Data/ZMod/Basic.lean,Mathlib/Geometry/Manifold/GroupLieAlgebra.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean,Mathlib/GroupTheory/GroupAction/Basic.lean,Mathlib/GroupTheory/GroupAction/Blocks.lean,Mathlib/GroupTheory/OrderOfElement.lean,Mathlib/GroupTheory/Submonoid/Centralizer.lean,Mathlib/MeasureTheory/Measure/Haar/Quotient.lean,Mathlib/NumberTheory/NumberField/Basic.lean,Mathlib/Tactic/ToAdditive.lean,Mathlib/Tactic/ToAdditive/Frontend.lean,Mathlib/Topology/Algebra/ConstMulAction.lean,Mathlib/Topology/Algebra/InfiniteSum/Module.lean,MathlibTest/toAdditive.lean |
25 |
11 |
['JovanGerb', 'bryangingechen', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
0-59349 16 hours ago |
0-61430 17 hours ago |
6-3281 6 days |
| 24845 |
kebekus author:kebekus |
feat: integrability of log ‖meromorphic‖ |
For real-meromorphic functions `f`, establish interval integrability of `log ‖f ·‖`. In particular, show that `log ∘ sin` is interval integrable. For complex-meromorphic functions `f`, establish circle integrability of `log ‖f ·‖`.
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. Integrability of `log ∘ sin` might be useful in future discussions of polylogarithms.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-measure-probability
t-analysis
|
198/2 |
Mathlib.lean,Mathlib/Analysis/Complex/Meromorphic/CircleIntegrability.lean,Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean,Mathlib/Analysis/SpecialFunctions/Integrals.lean,Mathlib/MeasureTheory/Integral/CircleIntegral.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean |
6 |
1 |
['github-actions'] |
nobody |
0-59228 16 hours ago |
0-59228 16 hours ago |
0-60662 16 hours |
| 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 |
0-58495 16 hours ago |
0-58495 16 hours ago |
60-85495 60 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 |
0-56043 15 hours ago |
0-84384 23 hours ago |
0-84434 23 hours |
| 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'] |
nobody |
0-55481 15 hours ago |
0-55492 15 hours ago |
0-55541 15 hours |
| 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 |
0-51123 14 hours ago |
0-56348 15 hours ago |
0-56332 15 hours |
| 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 |
0-50591 14 hours ago |
0-50653 14 hours ago |
82-78568 82 days |
| 23920 |
YaelDillies author:YaelDillies |
feat: entourage-separated sets |
Define a notion of separation of a set relative to an entourage. This will be used to unify metric and dynamical separation.
From MiscYD and LeanAPAP
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
61/0 |
Mathlib.lean,Mathlib/Topology/UniformSpace/Separated.lean |
2 |
13 |
['D-Thomine', 'YaelDillies', 'b-mehta', 'github-actions'] |
ADedecker assignee:ADedecker |
0-49312 13 hours ago |
30-29481 1 month ago |
30-38432 30 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 |
0-48146 13 hours ago |
6-38567 6 days ago |
31-1377 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 |
0-47949 13 hours ago |
3-31153 3 days ago |
3-32709 3 days |
| 24312 |
YaelDillies author:YaelDillies |
feat: more lemmas about torsion-free monoids |
The new imports just come from making `#min_imports` and `mk_iff` available earlier.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
large-import
maintainer-merge
t-algebra
label:t-algebra$ |
117/17 |
Mathlib/Algebra/Group/Pi/Lemmas.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Group/Subgroup/Basic.lean,Mathlib/Algebra/Group/Torsion.lean,Mathlib/Algebra/Lie/Weights/Chain.lean,Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean,Mathlib/GroupTheory/OrderOfElement.lean,Mathlib/GroupTheory/Torsion.lean,Mathlib/Topology/Instances/ZMultiples.lean |
9 |
7 |
['YaelDillies', 'b-mehta', 'github-actions', 'grunweg'] |
b-mehta assignee:b-mehta |
0-46880 13 hours ago |
0-48980 13 hours ago |
20-68054 20 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 |
0-46531 12 hours ago |
5-71457 5 days ago |
10-22660 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 |
0-46513 12 hours ago |
0-46513 12 hours ago |
15-61929 15 days |
| 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
|
121/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Preserves/Shapes/Over.lean,Mathlib/CategoryTheory/WithTerminal/Basic.lean |
3 |
3 |
['Moises-Herradon-Cueto', 'erdOne', 'github-actions'] |
nobody |
0-46161 12 hours ago |
1-73716 1 day ago |
1-73730 1 day |
| 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$ |
299/0 |
Mathlib.lean,Mathlib/GroupTheory/RegularWreathProduct.lean |
2 |
15 |
['ciskiko', 'github-actions', 'tb65536'] |
tb65536 assignee:tb65536 |
0-43469 12 hours ago |
0-70874 19 hours ago |
1-8903 1 day |
| 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 |
0-41918 11 hours ago |
2-55240 2 days ago |
2-60717 2 days |
| 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 |
9 |
['YaelDillies', 'eric-wieser', 'fpvandoorn', 'github-actions', 'joelriou', 'leanprover-community-bot-assistant'] |
nobody |
0-40202 11 hours ago |
0-81400 22 hours ago |
2-51026 2 days |
| 24856 |
FMLJohn author:FMLJohn |
feat(Topology/Subbasis): prove Alexander Subbasis Theorem |
---
[](https://gitpod.io/from-referrer/)
In this pull request, we have proved the Alexander Subbasis Theorem: if `X` has a topology `T` and `hTS : T = generateFrom S`, then `X` is compact if any open cover of `X` with elements in `S` has a finite subcover. |
t-topology |
38/0 |
Mathlib/Topology/Compactness/Compact.lean |
1 |
17 |
['FMLJohn', 'alreadydone', 'erdOne', 'github-actions'] |
nobody |
0-37074 10 hours ago |
0-45373 12 hours ago |
0-45357 12 hours |
| 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-34752 9 hours ago |
0-49996 13 hours ago |
72-8652 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-33767 9 hours ago |
0-49922 13 hours ago |
11-43664 11 days |
| 24344 |
erdOne author:erdOne |
feat: miscellaneous lemmas about transcedence bases |
---
- [ ] depends on: #24806
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
207/10 |
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/Algebraic/Basic.lean,Mathlib/RingTheory/AlgebraicIndependent/Basic.lean,Mathlib/RingTheory/AlgebraicIndependent/Defs.lean,Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean,Mathlib/RingTheory/Norm/Basic.lean |
14 |
19 |
['acmepjz', 'alreadydone', 'erdOne', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
alreadydone assignee:alreadydone |
0-33561 9 hours ago |
0-33561 9 hours ago |
18-30700 18 days |
| 24107 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(GroupTheory/GroupAction/Basic): equivalences between stabilizers |
Define equivalence between stabilizers.
This is concurrent PR to #24039
with a diffferent syntax that fits better my later applications.
This one a `MulEquiv`from `stabilizer G a` to `stabilizer G b` associated with `g : G`
and an equality `hg : b = g · a`.
(The first commit gave the other direction, this one looks preferable.)
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
91/20 |
Mathlib/Algebra/Group/End.lean,Mathlib/GroupTheory/GroupAction/Basic.lean |
2 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
riccardobrasca assignee:riccardobrasca |
0-32305 8 hours ago |
0-36306 10 hours ago |
27-60887 27 days |
| 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
|
132/101 |
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,Mathlib/Probability/Kernel/Condexp.lean |
15 |
7 |
['github-actions', 'grunweg', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
0-31667 8 hours ago |
0-51208 14 hours ago |
0-51592 14 hours |
| 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-30540 8 hours ago |
0-49869 13 hours ago |
0-51385 14 hours |
| 24122 |
apnelson1 author:apnelson1 |
feat(Combinatorics): multigraphs |
This PR defines multigraphs via a structure `Graph a b` consisting of a vertex set, an edge set, and a 'binary incidence' predicate describing which edges are incident with which vertices. The definition uses the same 'embedded set' design as `Matroid`: the vertex and edge sets are modelled as `Set`s rather than types.
We give basic API for incidence, adjacency and extensionality.
[Zulip discussion.](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2324122.20Multigraphs)
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
329/0 |
Mathlib.lean,Mathlib/Combinatorics/Graph/Basic.lean,scripts/noshake.json |
3 |
51 |
['AntoineChambert-Loir', 'Parcly-Taxel', 'apnelson1', 'b-mehta', 'eric-wieser', 'github-actions', 'kmill', 'madvorak'] |
nobody |
0-30005 8 hours ago |
0-34422 9 hours ago |
27-34877 27 days |
| 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-27979 7 hours ago |
10-83591 10 days ago* |
13-85192 13 days* |
| 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-20151 5 hours ago |
1-56722 1 day ago |
1-56706 1 day |
| 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-16378 4 hours ago |
0-16379 4 hours ago |
0-19684 5 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-12038 3 hours ago |
3-77910 3 days ago |
9-18921 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-7290 2 hours ago |
0-42071 11 hours ago |
0-42087 11 hours |
| 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/)
|
t-linter
maintainer-merge
|
176/0 |
scripts/README.md,scripts/create_deprecated_modules.lean |
2 |
23 |
['adomani', 'github-actions', 'grunweg'] |
grunweg assignee:grunweg |
0-1227 20 minutes ago |
0-28117 7 hours ago |
0-30270 8 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-485 8 minutes ago |
12-38999 12 days ago |
12-51325 12 days |