Welcome to the mathlib review page. Everybody's help with reviewing is appreciated. Reviewing contributions is important, and everybody is welcome to review pull requests! If you're not sure how, the pull request review guide is there to help you.
This page contains tables of
| Number |
Author |
Title |
Description |
Labels |
+/- |
Modified files (first 100) |
📝 |
💬 |
All users who commented or reviewed |
Assignee(s) |
Updated |
Last status change |
total time in review |
| 21129 |
chrisflav author:chrisflav |
perf(RingTheory/Kaehler/JacobiZariski): reorder universe variables |
Naming of universe variables has an impact on universe unification. It seems to matter that the universe variables of `R`, `S` and `T` appear before the universe variables of the generators in alphabetical order.
---
[](https://gitpod.io/from-referrer/)
|
performance-hack
t-algebra
label:t-algebra$ |
18/20 |
Mathlib/RingTheory/Kaehler/JacobiZariski.lean |
1 |
37 |
['chrisflav', 'erdOne', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'mattrobball'] |
nobody |
64-680 2 months ago |
98-3141 3 months ago |
106-70845 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-42213 1 month ago |
43-42213 1 month ago |
47-30389 47 days |
| 23684 |
alreadydone author:alreadydone |
feat(RingTheory): integral extensions of comm. rings are local homs |
---
The import increase only affects one file so I hope it's okay.
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
57/64 |
Mathlib/Algebra/Field/Equiv.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/Proper.lean,Mathlib/FieldTheory/LinearDisjoint.lean,Mathlib/LinearAlgebra/Dimension/Localization.lean,Mathlib/RingTheory/Artinian/Ring.lean,Mathlib/RingTheory/IntegralClosure/Algebra/Defs.lean,Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean,Mathlib/RingTheory/LinearDisjoint.lean,Mathlib/RingTheory/Localization/FractionRing.lean,Mathlib/RingTheory/Localization/Integral.lean,Mathlib/RingTheory/SimpleRing/Field.lean |
12 |
4 |
['alreadydone', 'github-actions', 'xroblot'] |
nobody |
39-5800 1 month ago |
39-37198 1 month ago |
39-37219 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-69019 1 month ago |
37-64087 1 month ago |
84-50913 84 days |
| 22474 |
joelriou author:joelriou |
feat(CategoryTheory/Functor): more API for pointwise Kan extensions |
Transport pointwise Kan extensions via isomorphisms/equivalences.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
157/7 |
Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean,Mathlib/CategoryTheory/Limits/HasLimits.lean,Mathlib/CategoryTheory/Limits/Opposites.lean,Mathlib/CategoryTheory/Limits/Shapes/Products.lean |
4 |
1 |
['github-actions'] |
nobody |
35-4389 1 month ago |
71-8252 2 months ago |
72-38524 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-69799 29 days ago |
29-71100 29 days ago |
29-71156 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-42251 29 days ago |
29-46063 29 days ago |
29-46047 29 days |
| 24065 |
kim-em author:kim-em |
chore: script to give topological sort of modules |
This script is not useful by itself: it just gives a topological sort of Mathlib's import graph. But I've several times found it useful when I want to modify many files systematically with minimal rebuilding: just work backwards through the list.
|
|
96/0 |
scripts/README.md,scripts/topological_sort.py |
2 |
4 |
['github-actions', 'jcommelin', 'kim-em'] |
nobody |
29-11180 29 days ago |
29-22218 29 days ago |
29-22202 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-48078 28 days ago |
28-78728 28 days ago |
40-45650 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-24972 28 days ago |
28-24972 28 days ago |
36-57225 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 |
28-432 28 days ago |
28-450 28 days ago |
83-47573 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-50115 26 days ago |
26-50115 26 days ago |
69-31048 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-44636 26 days ago |
37-42539 1 month ago |
211-67302 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-42883 25 days ago |
35-16484 1 month ago |
47-50758 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-68249 24 days ago |
29-50263 29 days ago |
29-50316 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-32997 24 days ago |
unknown |
unknown |
| 23964 |
BoltonBailey author:BoltonBailey |
docs: Add documentation arbitrarily |
@mattrobball asked in the Mathlib Community meeting today what it would look like if we asked Claude code to give us improved documentation. I made this draft PR by selecting five declarations arbitrarily from `nolints.json` and asking Cursor to document them.
---
[](https://gitpod.io/from-referrer/)
|
documentation |
52/14 |
Mathlib/Algebra/Homology/Homotopy.lean,Mathlib/Analysis/BoxIntegral/Partition/Filter.lean,Mathlib/Control/Monad/Cont.lean,Mathlib/Data/Stream/Defs.lean,Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean |
5 |
10 |
['ADedecker', 'BoltonBailey', 'eric-wieser', 'github-actions', 'jcommelin', 'mattrobball'] |
nobody |
24-10652 24 days ago |
31-51495 1 month ago |
32-28114 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-63570 23 days ago |
23-78630 23 days ago |
23-78621 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-47256 23 days ago |
48-75383 1 month ago |
48-75505 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-38851 22 days ago |
56-472 1 month ago |
56-2368 56 days |
| 24295 |
jsm28 author:jsm28 |
feat(Topology/Algebra/AffineSubspace): `AffineSubspace.subtypeA` |
Define the embedding map from an affine subspace to the ambient space as a continuous affine map, analogous to `Submodule.subtypeL`. There wasn't an immediately obvious location importing both continuous affine maps and affine subspaces, so I put this in its own file.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-topology
label:t-algebra$ |
42/0 |
Mathlib.lean,Mathlib/Topology/Algebra/AffineSubspace.lean |
2 |
1 |
['github-actions'] |
nobody |
21-52352 21 days ago |
21-52417 21 days ago |
21-52401 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-61289 20 days ago |
20-61292 20 days ago |
20-62885 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-32061 20 days ago |
20-32061 20 days ago |
20-53542 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-17432 20 days ago |
20-51814 20 days ago |
22-36040 22 days |
| 23926 |
b-reinke author:b-reinke |
feat(Algebra/BigOperators/Finprod): add powerset projection lemmas |
This PR adds lemmas in `Mathlib/Algebra/BigOperators/Finprod.lean` related to products/sums over the powerset `𝒫 s` when we add or remove an element of `s`.
The motivation comes from the proof of the deletion/contraction properties of matroids.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
30/0 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Image.lean |
2 |
5 |
['b-reinke', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
20-7766 20 days ago |
20-9558 20 days ago |
33-10082 33 days |
| 18693 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: add ConjRootClass |
Co-authored-by: FR
---
From #6718
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
213/0 |
Mathlib.lean,Mathlib/FieldTheory/Minpoly/ConjRootClass.lean,Mathlib/FieldTheory/Minpoly/IsConjRoot.lean |
3 |
13 |
['LessnessRandomness', 'Vierkantor', 'alreadydone', 'github-actions', 'grunweg'] |
nobody |
19-59416 19 days ago |
20-10779 20 days ago |
81-78925 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-45427 18 days ago |
18-45427 18 days ago |
39-33243 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-54715 17 days ago |
17-54715 17 days ago |
17-54775 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-85231 16 days ago |
17-815 17 days ago |
20-74648 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-83929 16 days ago |
28-55994 28 days ago |
68-49603 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-78017 16 days ago |
20-68255 20 days ago |
21-7096 21 days |
| 24412 |
pechersky author:pechersky |
feat(UniformSpace/Ultra/Constructions): IsUltraUniformity.{bot,top} |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
29/0 |
Mathlib/Order/Filter/Bases/Basic.lean,Mathlib/Topology/UniformSpace/Defs.lean,Mathlib/Topology/UniformSpace/Ultra/Basic.lean,Mathlib/Topology/UniformSpace/Ultra/Constructions.lean |
4 |
1 |
['github-actions'] |
nobody |
16-68241 16 days ago |
16-68397 16 days ago |
16-68391 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-54007 16 days ago |
69-85910 2 months ago |
69-85893 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-30842 16 days ago |
16-39535 16 days ago |
16-39519 16 days |
| 22961 |
xroblot author:xroblot |
feat(ZLattice/Covolume): add `covolume_div_covolume_eq_relindex` |
Add the following result:
Let `L₁` be a sub-`ℤ`-lattice of `L₂`. Then the index of `L₁` inside `L₂` is equal to `covolume L₁ / covolume L₂`.
---
- [x] depends on: #22940
- [x] depends on: #23759
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
66/4 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Algebra/Module/ZLattice/Covolume.lean,Mathlib/GroupTheory/Index.lean,Mathlib/LinearAlgebra/Determinant.lean |
4 |
10 |
['Ruben-VandeVelde', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'xroblot'] |
nobody |
16-6069 16 days ago |
16-6085 16 days ago |
52-48646 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-79230 14 days ago |
14-79230 14 days ago |
15-66588 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-76104 14 days ago |
14-76104 14 days ago |
14-81488 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-73290 14 days ago |
14-73291 14 days ago |
40-7476 40 days |
| 24448 |
Hagb author:Hagb |
feat(RingTheory/Ideal/Span.lean): some lemmas about zero and span |
`simp` would be able to solve them.
Notice that `span_singleton_zero : span {(0 : R)} = ⊥` itself can be solved by `simp` without this commit, which uses `span_singleton_eq_bot : span ({x} : Set α) = ⊥ ↔ x = 0`, while `simp` cannot solve goals like `f (Ideal.span {(0 : R)}) = f ⊥`, which would be solvable by `simp` with `span_singleton_zero` marked with `@[simp]`.
Without adding also `Ideal.dvd_span_bot` to `Mathlib/RingTheory/DedekindDomain/Ideal.lean`, these lemmas on `Span.lean` would make the following failed, since `simp` would rewrite `{0}` with `⊥` and result in a goal `v.asIdeal ∣ ⊥` that it can't solve.
https://github.com/leanprover-community/mathlib4/blob/3f2556372f27171259a381d4d57db71440700cd8/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean#L123
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
16/1 |
Mathlib/Algebra/Module/PID.lean,Mathlib/RingTheory/DedekindDomain/Ideal.lean,Mathlib/RingTheory/Ideal/Span.lean |
3 |
1 |
['github-actions'] |
nobody |
14-68818 14 days ago |
14-78809 14 days ago |
14-78863 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-46740 14 days ago |
33-62630 1 month ago |
33-63429 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-46667 14 days ago |
14-46667 14 days ago |
30-66113 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-32565 14 days ago |
16-53755 16 days ago |
21-43357 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-80607 13 days ago |
13-81685 13 days ago |
13-81752 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 |
13-2731 13 days ago |
13-2794 13 days ago |
13-2778 13 days |
| 24380 |
chrisflav author:chrisflav |
chore(RingTheory/TensorProduct): more product compatibilities |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
48/4 |
Mathlib/RingTheory/TensorProduct/Pi.lean |
1 |
3 |
['erdOne', 'github-actions'] |
nobody |
12-80690 12 days ago |
12-80690 12 days ago |
14-38651 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-77995 12 days ago |
12-80124 12 days ago |
13-1863 13 days |
| 24517 |
upobir author:upobir |
feat(Algebra/QuadraticDiscriminant): Adding inequalities on quadratic from inequalities on discriminant |
---
This pr adds inequalities that relate `0` and `a * (x * x) + b * x + c` from inequalities of `a` and `discrim a b c`. For example, negative discriminant and negative leading coefficient implies value of quadratic expression is always negative and similar.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
35/0 |
Mathlib/Algebra/QuadraticDiscriminant.lean |
1 |
1 |
['github-actions'] |
nobody |
12-68058 12 days ago |
12-68058 12 days ago |
12-68111 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-61150 12 days ago |
12-61351 12 days ago |
12-61407 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-58579 12 days ago |
12-61220 12 days ago |
21-46363 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-39979 12 days ago |
12-72070 12 days ago |
37-2516 37 days |
| 24245 |
JovanGerb author:JovanGerb |
feat(Geometry/Euclidean/SignedDist): `signedDist` between two points |
This PR defines `signedDist`, the signed distance between two points.
It redefines `signedInfDist` so that it uses `signedDist`.
The motivation is to use this in IMO2020Q6. Additionally this definition will be useful for properly reasoning about the power of a point
[#mathlib4 > Signed distance between points](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Signed.20distance.20between.20points)
some comments:
* should `signedDistLinear` be `private`?
* should `signedDist` and `signedInfDist` be made continuous bunled maps in this PR?
* I'm not too happy about the hypothesis in `signedDist_congr (h : ∃ r > (0 : ℝ), r • v = w)`. This relationship between `v` and `w` is a symmetric one that should have some API around it, similar to `SameRay`. It could also be spelled as `(ℝ≥0 ∙ v) = ℝ≥0 ∙ w`
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
206/23 |
Mathlib/Analysis/InnerProductSpace/Basic.lean,Mathlib/Geometry/Euclidean/SignedDist.lean,Mathlib/Topology/MetricSpace/Pseudo/Defs.lean |
3 |
1 |
['github-actions'] |
nobody |
12-8289 12 days ago |
12-8289 12 days ago |
23-24862 23 days |
| 24533 |
robertmaxton42 author:robertmaxton42 |
feat (ULift): conjugation by ULift.up/down, misc cast/heq lemmas |
* Adds the convenience def `ULift.conj x := `down (f (up x))`, and corresponding basic lemmas
* Adds lemmas showing that `ULift.up` and `.down` commute with casts and preserve `HEq`.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
31/0 |
Mathlib/Data/ULift.lean |
1 |
14 |
['eric-wieser', 'github-actions', 'robertmaxton42'] |
nobody |
12-3496 12 days ago |
12-3496 12 days ago |
12-11412 12 days |
| 24379 |
chrisflav author:chrisflav |
feat(Algebra/AlgHom): `Unique` if target is `Subsingleton` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
32/0 |
Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/Algebra/Hom.lean |
2 |
5 |
['chrisflav', 'eric-wieser', 'github-actions'] |
nobody |
11-79855 11 days ago |
12-80136 12 days ago |
13-29674 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-40332 11 days ago |
11-45394 11 days ago |
48-4150 48 days |
| 24266 |
plp127 author:plp127 |
feat(Order): `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)` |
Proves that `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)`, and also the dual theorem.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
14/0 |
Mathlib/Order/Directed.lean |
1 |
4 |
['github-actions', 'plp127', 'urkud'] |
nobody |
11-28062 11 days ago |
22-39443 22 days ago |
22-39428 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-26701 11 days ago |
12-70838 12 days ago |
12-70891 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-13388 11 days ago |
11-13405 11 days ago |
84-50086 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 |
11-11199 11 days ago |
11-11199 11 days ago |
43-77323 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 |
11-11187 11 days ago |
11-11187 11 days ago |
48-22655 48 days |
| 23676 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprime `induction'` for localizations and quotients |
All these removed instances of `induction'` generate only one subgoal. In some cases `obtain` can be used.
The relevant instances were identified by adding the following to `Mathlib.Tactic.Cases`
```diff
diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean
index 4a60db6c551..08c06520879 100644
--- a/Mathlib/Tactic/Cases.lean
+++ b/Mathlib/Tactic/Cases.lean
@@ -122,6 +122,16 @@ elab (name := induction') "induction' " tgts:(Parser.Tactic.elimTarget,+)
g.assign result.elimApp
let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
(generalized := fvarIds) (toClear := targetFVarIds) (toTag := toTag)
+ let body ← inferType targets[0]!
+ let names : Array Format := if withArg.1.getArgs.size > 1 then
+ (withArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+ let gens : Array Format := if genArg.1.getArgs.size > 1 then
+ (genArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+ let inductor : Format := if usingArg.1.getArgs.size > 1 then
+ Syntax.prettyPrint usingArg.1.getArgs[1]! else "~"
+ if subgoals.toList.length ≤ 1 then
+ logInfoAt tgts m!"{body.getAppFn.setPPExplicit true} {inductor} {gens} {names} \
+ {subgoals.toList.length}"
setGoals <| (subgoals ++ result.others).toList ++ gs
/-- The `cases'` tactic is similar to the `cases` tactic in Lean 4 core, but the syntax for giving
```
and then examining [the output](https://github.com/leanprover-community/mathlib4/actions/runs/14270845291/job/40003467676). |
tech debt |
94/113 |
Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Pointwise/Stabilizer.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Limits/Types/Colimits.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Finsupp/BigOperators.lean,Mathlib/Data/Fintype/Quotient.lean,Mathlib/Data/List/Cycle.lean,Mathlib/Data/Nat/ChineseRemainder.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/FieldTheory/RatFunc/Basic.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/GroupTheory/OreLocalization/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Concrete.lean,Mathlib/GroupTheory/Perm/Sign.lean,Mathlib/GroupTheory/Torsion.lean,Mathlib/RingTheory/OreLocalization/Basic.lean,Mathlib/RingTheory/OreLocalization/Ring.lean,Mathlib/SetTheory/Surreal/Basic.lean |
25 |
10 |
['Parcly-Taxel', 'apnelson1', 'eric-wieser', 'github-actions', 'grunweg', 'urkud'] |
nobody |
11-8651 11 days ago |
11-9694 11 days ago |
38-70414 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-67650 10 days ago |
11-10207 11 days ago |
26-84250 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-64722 10 days ago |
10-81792 10 days ago |
12-50092 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-60568 10 days ago |
10-60584 10 days ago |
21-43186 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-58185 10 days ago |
11-76252 11 days ago |
12-5363 12 days |
| 24567 |
joelriou author:joelriou |
feat(CategoryTheory): the shift functors on the localized category are linear |
If `L : C ⥤ D` is a localization functor with respect to `W : MorphismProperty C` and both `C` and `D` have been equipped with `R`-linear category structures such that `L` is `R`-linear and the shift functors on `C` are `R`-linear, then the shift functors on `D` are `R`-linear.
---
- [x] depends on: #24309
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
48/0 |
Mathlib.lean,Mathlib/CategoryTheory/Shift/Linear.lean |
2 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
10-49999 10 days ago |
10-50007 10 days ago |
10-49991 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-28896 10 days ago |
10-28951 10 days ago |
10-28946 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-24821 10 days ago |
79-26463 2 months ago |
79-26589 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-19192 10 days ago |
10-28410 10 days ago |
10-28404 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-79465 9 days ago |
9-79489 9 days ago |
9-79473 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-14110 9 days ago |
10-14463 10 days ago |
10-14511 10 days |
| 23368 |
b-reinke author:b-reinke |
feat(GroupTheory/FreeGroup/ReducedWords): add theory of reduced words |
Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project.
This PR adds the file `GroupTheory/FreeGroup/ReducedWords.lean`, where the predicate of reduced words is defined. It is shown that `reduce` and `toWord` produce reduced words.
This is done in preparation for the theory of cyclically reduced words.
---
[](https://gitpod.io/from-referrer/)
|
t-geometric-group-theory
t-algebra
label:t-algebra$ |
109/0 |
Mathlib.lean,Mathlib/GroupTheory/FreeGroup/ReducedWords.lean |
2 |
28 |
['b-reinke', 'github-actions', 'vlad902'] |
nobody |
9-11562 9 days ago |
47-77182 1 month ago |
47-85013 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 |
9-1225 9 days ago |
13-67774 13 days ago |
13-67769 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-83588 8 days ago |
29-59979 29 days ago |
53-49431 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-71276 8 days ago |
8-71276 8 days ago |
8-71336 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-63237 8 days ago |
16-61130 16 days ago |
63-67216 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-50657 8 days ago |
8-50657 8 days ago |
13-58613 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-26311 8 days ago |
12-34997 12 days ago |
26-49301 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-17872 8 days ago |
10-19214 10 days ago |
36-63417 36 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-68381 7 days ago |
7-68400 7 days ago |
32-65537 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-66264 7 days ago |
21-81407 21 days ago |
40-82872 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-63287 7 days ago |
8-18320 8 days ago |
8-18371 8 days |
| 24492 |
Parcly-Taxel author:Parcly-Taxel |
chore: remove some adaptation notes |
|
tech debt |
15/32 |
Mathlib/Algebra/Homology/Single.lean,Mathlib/Combinatorics/Enumerative/DyckWord.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Int/Cast/Basic.lean,Mathlib/NumberTheory/DiophantineApproximation/Basic.lean |
5 |
12 |
['JovanGerb', 'Parcly-Taxel', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] |
nobody |
7-11582 7 days ago |
7-11598 7 days ago |
12-5857 12 days |
| 24361 |
Hagb author:Hagb |
feat(Data/Finsupp/MonomialOrder): `0 ≤ a` where `a : m.syn` |
`simp` would be able to solve it.
---
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
easy
|
3/0 |
Mathlib/Data/Finsupp/MonomialOrder.lean |
1 |
1 |
['github-actions'] |
nobody |
7-7489 7 days ago |
7-7489 7 days ago |
19-9167 19 days |
| 24236 |
YaelDillies author:YaelDillies |
feat: closed submodules |
Define closed `R`-submodules.
The plan is to redefine proper `R`-cones as closed `R≥0`-submodules.
From Toric
---
- [x] depends on: #24230
[](https://gitpod.io/from-referrer/)
|
toric
t-topology
|
180/0 |
Mathlib.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean |
2 |
14 |
['YaelDillies', 'b-mehta', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
7-6147 7 days ago |
7-6221 7 days ago |
19-40164 19 days |
| 20171 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): define turanDensity |
Define the Turán density `turanDensity H` of a simple graph `H`: `turanDensity H` is the limit of `extremalNumber n H / n.choose 2` as `n` approaches `∞`.
Also prove
- the Turán density of a simple graph is well-defined, that is, the limit `extremalNumber n H / n.choose 2` as `n` approaches `∞` exists,
- `extremalNumber n H` is asymptotically equivalent to `turanDensity H * n.choose 2` as `n` approaches `∞`.
---
- [x] depends on: #19865
- [x] depends on: #20681
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
182/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/TuranDensity.lean,Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Data/Sym/Sym2.lean |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
7-5525 7 days ago |
7-5569 7 days ago |
7-7564 7 days |
| 20240 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): prove the Kővári–Sós–Turán theorem |
Prove the Kővári–Sós–Turán theorem for simple graphs: the `(completeBipartiteGraph α β).Free` simple graphs for `card α ≤ card β` on the vertex type `V` have at most `(card β-1)^(1/(card α))*(card V)^(2-1/(card α))/2 + (card V)*(card α-1)/2` edges.
---
- [x] depends on: #19865
- [x] depends on: #20738
I'd like to make `aux` not private in the `KovariSosTuran` namespace to enable reuse of the double-counting here, but I don't know what to call it.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
289/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/KovariSosTuran.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
7-3729 7 days ago |
15-34300 15 days ago |
15-34835 15 days |
| 22151 |
alreadydone author:alreadydone |
feat(RingTheory): a semiprimary ring is Noetherian/Artinian iff its Jacobson radical is fg |
A key fact used is `Module.FG.smul`: if `I` is a two-sided ideal of `R` that is f.g. as a left ideal and `N` is a f.g. `R`-module, then `I • M` is also a f.g. `R`-module.
Many lemmas about coprimality of ideals are also generalized to the noncommutative, two-sided setting.
---
- [x] depends on: #21904
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
215/155 |
Mathlib/Algebra/Algebra/Operations.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean,Mathlib/RingTheory/Extension.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/Finiteness/Ideal.lean,Mathlib/RingTheory/HopkinsLevitzki.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/Ideal/Operations.lean |
8 |
6 |
['alreadydone', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
7-1311 7 days ago |
7-1311 7 days ago |
70-61378 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-80046 6 days ago |
6-80047 6 days ago |
6-80111 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-68975 6 days ago |
7-83118 7 days ago |
14-79291 14 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-56958 6 days ago |
6-56958 6 days ago |
6-69875 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-36021 6 days ago |
10-59975 10 days ago |
32-11022 32 days |
| 24669 |
qawbecrdtey author:qawbecrdtey |
feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` |
---
[](https://gitpod.io/from-referrer/)
This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it.
```lean
def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E
```
|
t-analysis |
20/1 |
Mathlib/Analysis/Normed/Operator/LinearIsometry.lean |
1 |
1 |
['github-actions'] |
nobody |
6-21442 6 days ago |
6-21458 6 days ago |
6-21512 6 days |
| 22279 |
xyzw12345 author:xyzw12345 |
feat(RingTheory/GradedAlgebra): homogeneous relation |
In this PR, we defined the concept of a homogeneous relation and proved some properties about homogeneous relations. The main result of this PR is showing that taking `RingQuot` by a homogeneous relation can give a graded structure on the quotient ring. This result can be used to define graded structures on rings obtained using `RingQuot`, e.g. the Symmetric Algebra defined in #21539 can be verified to have such a structure.
Co-authored-by:
Zhixuan Dai @atstarrysky <22300180006@m.fudan.edu.cn>
Yiming Fu @pelicanhere
Zhenyan Fu @pumpkin678
Raphael Douglas Giles @Raph-DG
Jiedong Jiang @jjdishere
- [x] depends on: #22354
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
455/0 |
Mathlib.lean,Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/DirectSum/Basic.lean,Mathlib/Algebra/DirectSum/Module.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/RingQuot.lean,Mathlib/RingTheory/GradedAlgebra/Basic.lean,Mathlib/RingTheory/GradedAlgebra/HomogeneousRelation.lean |
8 |
7 |
['Paul-Lez', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'ocfnash', 'xyzw12345'] |
ocfnash assignee:ocfnash |
6-11935 6 days ago |
42-16516 1 month ago |
43-48304 43 days |
| 22464 |
adomani author:adomani |
feat(CI): declarations diff in Lean |
Rewrites the `declaration_diff` script in Lean.
You can see the effect of the new script in the testing branch #22497.
The new CI step runs in approximately 5mins, but is separate from the `build` step.
---
[](https://gitpod.io/from-referrer/)
|
CI |
151/0 |
.github/workflows/PR_summary_lean.yml,scripts/README.md,scripts/declarations_diff.lean,scripts/declarations_diff_lean_shell_glue.sh |
4 |
6 |
['bryangingechen', 'github-actions', 'grunweg'] |
robertylewis assignee:robertylewis |
6-11759 6 days ago |
70-62404 2 months ago |
70-62394 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 |
6-11492 6 days ago |
25-65575 25 days ago |
25-65630 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 |
6-9930 6 days ago |
6-9930 6 days ago |
24-73803 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 |
6-5606 6 days ago |
6-83087 6 days ago |
66-23872 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 |
6-5107 6 days ago |
6-38848 6 days ago |
60-57468 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-77743 5 days ago |
25-86170 25 days ago |
73-79486 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-77709 5 days ago |
64-67460 2 months ago |
64-67512 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-77631 5 days ago |
26-50075 26 days ago |
37-12493 37 days |
| 23826 |
javra author:javra |
feat(CategoryTheory): linear categories as `ModuleCat R`-enriched categories |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-category-theory
|
195/0 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean,Mathlib/CategoryTheory/Enriched/Linear.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/CategoryTheory/Monoidal/Linear.lean |
5 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
TwoFX assignee:TwoFX |
5-77615 5 days ago |
30-1649 1 month ago |
30-1633 30 days |
| 21103 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialSet): uniqueness of the decomposition involving non-degenerate simplices |
Any simplex `x : X _⦋n⦌` of a simplicial set can be written in a unique way as `X.map f.op y` for an epimorphism `f : ⦋n⦌ ⟶ ⦋m⦌` and a non-degenerate `m`-simplex `y`.
---
- [x] depends on: #21098
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
118/5 |
Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean |
2 |
4 |
['gio256', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
dagurtomas assignee:dagurtomas |
5-75001 5 days ago |
25-48506 25 days ago |
63-80110 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-74988 5 days ago |
22-60268 22 days ago |
22-61792 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-74800 5 days ago |
43-67973 1 month ago |
43-68025 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-73875 5 days ago |
15-69901 15 days ago |
15-70583 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-71337 5 days ago |
41-39041 1 month ago |
46-65683 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-71122 5 days ago |
20-61285 20 days ago |
21-71336 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-68688 5 days ago |
5-68688 5 days ago |
6-29378 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-60769 5 days ago |
5-60832 5 days ago |
5-60817 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-57621 5 days ago |
7-61676 7 days ago |
57-19168 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-49911 5 days ago |
49-69266 1 month ago |
83-54364 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-49417 5 days ago |
5-60198 5 days ago |
5-60247 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-43089 5 days ago |
31-84938 1 month ago |
31-84992 31 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-40874 5 days ago |
39-53511 1 month ago |
39-53563 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-40743 5 days ago |
33-35314 1 month ago |
33-35364 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-33091 5 days ago |
11-11271 11 days ago |
12-79225 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-19471 5 days ago |
5-67307 5 days ago |
5-67362 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 |
5-11255 5 days ago |
36-63186 1 month ago |
36-64978 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 |
5-4485 5 days ago |
5-5083 5 days ago |
5-5068 5 days |
| 8167 |
sebzim4500 author:sebzim4500 |
feat: Add new `grw` tactic for rewriting using inequalities. |
Co-authored-by: @hrmacbeth, @digama0
---
- [x] depends on: #8796
```lean
example (x y z w : ℝ) (h₁ : x < z) (h₂ : w ≤ y + 4) (h₃ : Real.exp z < 5 * w) :
Real.exp x < 5 * (y + 4) := by
grw [h₁, ← h₂]
exact h₃
```
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
modifies-tactic-syntax
|
552/2 |
Mathlib.lean,Mathlib/Data/Int/ModEq.lean,Mathlib/Tactic.lean,Mathlib/Tactic/GCongr/Core.lean,Mathlib/Tactic/GRW.lean,Mathlib/Tactic/GRW/Core.lean,Mathlib/Tactic/GRW/Lemmas.lean,MathlibTest/GRW.lean,scripts/noshake.json |
9 |
53 |
['Vierkantor', 'digama0', 'eric-wieser', 'fpvandoorn', 'github-actions', 'hrmacbeth', 'kim-em', 'leanprover-community-mathlib4-bot', 'sebzim4500'] |
nobody |
4-81672 4 days ago |
66-56116 2 months ago |
97-18365 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-81602 4 days ago |
41-75256 1 month ago |
44-22257 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-81494 4 days ago |
80-26593 2 months ago |
80-26585 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-81468 4 days ago |
59-38851 1 month ago |
64-39388 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-79621 4 days ago |
29-80891 29 days ago |
29-80946 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-79534 4 days ago |
51-54208 1 month ago |
99-73898 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-77185 4 days ago |
4-77185 4 days ago |
35-19578 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-74541 4 days ago |
42-55994 1 month ago |
81-22542 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-73662 4 days ago |
4-75644 4 days ago |
4-75694 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-72890 4 days ago |
4-72890 4 days ago |
4-72946 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-72419 4 days ago |
49-38463 1 month ago |
49-38508 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-69866 4 days ago |
4-80854 4 days ago |
4-80966 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-63932 4 days ago |
7-10134 7 days ago |
7-10185 7 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-63288 4 days ago |
5-72864 5 days ago |
5-72864 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-61182 4 days ago |
4-84926 4 days ago |
19-4362 19 days |
| 24213 |
BoltonBailey author:BoltonBailey |
feat: add simp lemmas for trig functions on `π * 2⁻¹` |
This PR adds a number of simp lemmas to reduce trig functions evaluated on `π * 2⁻¹`. This allows `simp` to reduce expressions such as `sin (π * (1 / 2))`
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
45/0 |
Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean |
1 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
4-60637 4 days ago |
4-60659 4 days ago |
23-31652 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-55116 4 days ago |
5-59519 5 days ago |
5-59504 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-47656 4 days ago |
5-72820 5 days ago |
58-48274 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-46076 4 days ago |
36-68759 1 month ago |
39-31462 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-14173 4 days ago |
4-16949 4 days ago |
8-57356 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 |
4-4610 4 days ago |
20-5606 20 days ago |
20-5667 20 days |
| 23161 |
mans0954 author:mans0954 |
feature(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range |
The distance between two elements of `Finset.range N` (i.e. absolute value of the difference as integers) is less than `N`.
A lemma I found useful for something I was working on, so sharing here in case it's of wider interest.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
30/0 |
Mathlib.lean,Mathlib/Algebra/Order/Group/Unbundled/Abs.lean,Mathlib/Data/Finset/RangeDistance.lean |
3 |
3 |
['fbarroero', 'github-actions'] |
nobody |
4-4551 4 days ago |
54-54145 1 month ago |
54-54137 54 days |
| 24735 |
joelriou author:joelriou |
chore(CategoryTheory/Monoidal): define tensorLeft/Right as abbrev for curriedTensor |
In the study of commutation of tensor products with colimits, we may not be completely sure about phrasing the assumptions (as instances) in terms of `tensorLeft X` (resp. `tensorRight Y`) or in terms of `(curriedTensor C).obj X` (resp. `(curriedTensor C).flip.obj Y`), even though they are defeq, and we could have to introduce lemmas/instances to deduce properties of `tensorLeft X` from that of `(curriedTensor C).obj` and vice versa. By making `tensorLeft` and `tensorRight` abbreviations, this PR makes such issues disappear.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
20/21 |
Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean,Mathlib/CategoryTheory/Closed/Functor.lean,Mathlib/CategoryTheory/Closed/Monoidal.lean,Mathlib/CategoryTheory/Monoidal/Bimod.lean,Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean,Mathlib/CategoryTheory/Monoidal/Category.lean |
6 |
6 |
['fivemeyestore', 'fivemhostingserver', 'fivemserverhostings', 'fivemtebex', 'github-actions', 'scriptforfivem'] |
nobody |
4-1914 4 days ago |
4-5422 4 days ago |
4-5407 4 days |
| 24530 |
chrisflav author:chrisflav |
feat(RingTheory): faithfully flat ring maps |
Co-authored by: Joël Riou
---
- [ ] depends on: #24375
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
159/15 |
Mathlib.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean,Mathlib/RingTheory/LocalProperties/Basic.lean,Mathlib/RingTheory/RingHom/FaithfullyFlat.lean,Mathlib/RingTheory/RingHom/Finite.lean,Mathlib/RingTheory/RingHom/Flat.lean,Mathlib/RingTheory/RingHom/Integral.lean,Mathlib/RingTheory/RingHom/Locally.lean,Mathlib/RingTheory/RingHom/Surjective.lean,Mathlib/RingTheory/RingHom/Unramified.lean,Mathlib/RingTheory/RingHomProperties.lean |
12 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
4-1220 4 days ago |
4-1221 4 days ago |
4-2288 4 days |
| 24711 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal/Limits): miscellany about preservation of (co)limits by tensor products |
Register some instances regarding preservations of (co)limits for the tensor product of a monoidal category. More precisely, we register the fact that if the category is braided and `tensorLeft c` preserves colimits (this can be inferred e.g via `MonoidalClosed C`), then so does `tensorRight c` for every `c`.
We also rephrase preservation of (co)limits for `curriedTensor C` in terms of preservations of (co)limits for `tensorRight c`.
The PR introduces also introduces a directory `CategoryTheory.Monoidal.Limits` and moves the existing file `CategoryTheory.Monoidal.Limits.lean` to `CategoryTheory.Monoidal.Limits.Basic`.
---
The instances registered here are tailored so that for a braided monoidal closed category, `PreservesColimit₂` instances from #24685 can be inferred with the results of #24686 for the external product of diagrams defined in #24703
[](https://gitpod.io/from-referrer/)
|
file-removed
t-category-theory
|
72/2 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean,Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean,Mathlib/CategoryTheory/Monoidal/Limits/Preserves.lean |
4 |
8 |
['github-actions', 'joelriou', 'robin-carlier'] |
nobody |
3-86103 3 days ago |
3-86103 3 days ago |
4-69394 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-85800 3 days ago |
3-85800 3 days ago |
53-35547 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-70241 3 days ago |
6-48764 6 days ago |
6-49793 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-68715 3 days ago |
3-68716 3 days ago |
36-59814 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-60477 3 days ago |
39-47526 1 month ago |
39-47574 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-59043 3 days ago |
3-59060 3 days ago |
5-30142 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-56322 3 days ago |
3-62295 3 days ago |
18-46335 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-42371 3 days ago |
3-49817 3 days ago |
3-49867 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-35711 3 days ago |
13-2279 13 days ago |
13-2263 13 days |
| 24351 |
eric-wieser author:eric-wieser |
feat: fderiv lemmas for `pow` |
This generalizes the lemmas about `fderiv fun x => f x ^ n` to work over arbitrary normed modules and algebras.
Following the convention set by the lemmas about `fderiv` and `*`, we use `'`d names for the non-commutative variants.
Moves:
- `deriv_pow''` -> `deriv_pow`
- `deriv_pow` -> `deriv_pow_field`
- `derivWithin_pow'` -> `derivWithin_pow_field'`
Deletions:
- `deriv_pow'`
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
282/82 |
Mathlib.lean,Mathlib/Analysis/Calculus/Deriv/Polynomial.lean,Mathlib/Analysis/Calculus/Deriv/Pow.lean,Mathlib/Analysis/Calculus/FDeriv/Mul.lean,Mathlib/Analysis/Calculus/FDeriv/Pow.lean,Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Complex/Angle.lean,Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean,Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean |
9 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
3-33523 3 days ago |
3-33523 3 days ago |
3-66971 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-31052 3 days ago |
13-3642 13 days ago |
17-66205 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-29006 3 days ago |
3-29975 3 days ago |
21-837 21 days |
| 24734 |
mbkybky author:mbkybky |
feat(Algebra/Homology/DerivedCategory): `Ext` commutes with finite coproducts |
Prove that `Ext` commutes with finite coproducts and products.
Co-authored-by: Nailin Guan @Thmoas-Guan
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-category-theory
label:t-algebra$ |
83/5 |
Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean,Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean,Mathlib/CategoryTheory/Preadditive/Biproducts.lean |
3 |
6 |
['github-actions', 'joelriou', 'mbkybky'] |
nobody |
3-21745 3 days ago |
3-21745 3 days ago |
3-27456 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-21195 3 days ago |
3-21589 3 days ago |
7-48917 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-13661 3 days ago |
3-13707 3 days ago |
3-13708 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 |
3-10679 3 days ago |
3-10679 3 days ago |
14-73643 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 |
3-2730 3 days ago |
3-7708 3 days ago |
33-11304 33 days |
| 24205 |
meithecatte author:meithecatte |
chore(RegularExpressions): clarify that TODO has pending PRs |
The TODO on equivalence between regular expressions and DFAs seems to be particularly appealing to new contributors, having spawned multiple competing PRs working towards that goal.
It is also one where a new contributor is quite likely to produce a design that is not inline with mathlib's API design philosophy and will require a lot of guidance, which causes the PRs to languish in review.
Reword the TODO to make it less likely that the situation gets worse.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-computability
new-contributor
easy
|
2/1 |
Mathlib/Computability/RegularExpressions.lean |
1 |
7 |
['YaelDillies', 'github-actions', 'meithecatte', 'urkud'] |
nobody |
3-2558 3 days ago |
3-2558 3 days ago |
24-56363 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-84218 2 days ago |
2-84218 2 days ago |
3-44650 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-81031 2 days ago |
2-81095 2 days ago |
2-81080 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-79077 2 days ago |
2-79126 2 days ago |
2-79111 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-76531 2 days ago |
7-52201 7 days ago |
12-40773 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-73653 2 days ago |
6-73242 6 days ago |
13-21262 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-71576 2 days ago |
2-71596 2 days ago |
2-84783 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-65952 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-63387 2 days ago |
2-63639 2 days ago |
2-65581 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-58865 2 days ago |
2-58866 2 days ago |
5-68646 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-56123 2 days ago |
2-56185 2 days ago |
2-56170 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-52795 2 days ago |
2-58746 2 days ago |
50-24568 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-52161 2 days ago |
2-52209 2 days ago |
13-40618 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-49573 2 days ago |
2-49788 2 days ago |
2-51832 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-48149 2 days ago |
39-73338 1 month ago |
42-56727 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-40312 2 days ago |
2-71877 2 days ago |
17-57313 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-37194 2 days ago |
2-38126 2 days ago |
68-38113 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-31665 2 days ago |
2-31665 2 days ago |
2-31722 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-22788 2 days ago |
2-22788 2 days ago |
25-46909 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-21561 2 days ago |
2-39686 2 days ago |
12-22161 12 days |
| 23935 |
Thmoas-Guan author:Thmoas-Guan |
feat(RingTheory/IsSMulRegular): categorical constructions for IsSMulRegular |
The categorical constructions for `IsSMulRegular` for later use related to `Ext` in a separate file.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-category-theory
label:t-algebra$ |
62/0 |
Mathlib.lean,Mathlib/Algebra/Homology/ExactSequence.lean,Mathlib/RingTheory/Regular/Category.lean |
3 |
28 |
['Thmoas-Guan', 'erdOne', 'github-actions', 'joelriou', 'riccardobrasca'] |
joelriou assignee:joelriou |
2-10112 2 days ago |
20-62425 20 days ago |
29-35522 29 days |
| 23718 |
syur2 author:syur2 |
feat(Algebra): hom localize equiv localize hom |
Add the linear equiv of `S^{-1}(M =>[R] N)` equiv `(S^{-1} M) =>[S^{-1}R] (S^{-1} N)` for finitely presented module `M`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
50/0 |
Mathlib/Algebra/Module/FinitePresentation.lean |
1 |
4 |
['Thmoas-Guan', 'acmepjz', 'github-actions'] |
nobody |
2-10073 2 days ago |
38-11952 1 month ago |
38-11947 38 days |
| 21966 |
vasnesterov author:vasnesterov |
feat(Tactic/Order): support `⊤`, `⊥`, and lattice operations |
Support `⊤`, `⊥`, and lattice operations in the `order` tactic.
---
- [x] depends on: #21877
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
248/68 |
Mathlib/Tactic/Order.lean,Mathlib/Tactic/Order/CollectFacts.lean,Mathlib/Tactic/Order/Graph/Basic.lean,Mathlib/Tactic/Order/Preprocessing.lean,MathlibTest/order.lean,scripts/noshake.json |
6 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
2-9163 2 days ago |
41-3584 1 month ago |
75-80 75 days |
| 17914 |
xroblot author:xroblot |
feat(NumberTheory/NumberField): proof of the Analytic Class Number Formula |
Let `K` be a number field. Define
```lean
def dedekindZeta (s : ℂ) :=
LSeries (fun n ↦ Nat.card {I : Ideal (𝓞 K) // absNorm I = n}) s
```
and
```lean
def residue : ℝ :=
(2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * classNumber K) /
(torsionOrder K * Real.sqrt |discr K|)
```
We prove:
```lean
theorem dedekindZeta_residue :
Tendsto (fun s : ℝ ↦ (s - 1) * dedekindZeta K s) (𝓝[>] 1) (𝓝 (residue K))
```
---
- [x] depends on: #16675
- [x] depends on: #16822
- [x] depends on: #12488
- [x] depends on: #12405
- [x] depends on: #17943
- [x] depends on: #17944
- [x] depends on: #18130
- [x] depends on: #18166
- [x] depends on: #18231
- [x] depends on: #18246
- [x] depends on: #18245
- [x] depends on: #18248
- [x] depends on: #18400
- [x] depends on: #20660
- [x] depends on: #22115
- [x] depends on: #22397
- [x] depends on: #22779
- [x] depends on: #22866
- [x] depends on: #23440
- [x] depends on: #24713
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
81/0 |
Mathlib.lean,Mathlib/NumberTheory/NumberField/ClassNumber.lean,Mathlib/NumberTheory/NumberField/DedekindZeta.lean |
3 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'riccardobrasca', 'xroblot'] |
riccardobrasca assignee:riccardobrasca |
1-81715 1 day ago |
2-7656 2 days ago |
2-20967 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-75689 1 day ago |
1-81323 1 day ago |
59-9946 59 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-74494 1 day ago |
1-75493 1 day ago |
3-59568 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-73306 1 day ago |
1-76841 1 day ago |
6-9122 6 days |
| 23673 |
erdOne author:erdOne |
feat(AlgebraicGeometry): delaborator for coercing schemes to types |
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
t-meta
|
46/0 |
Mathlib/AlgebraicGeometry/Scheme.lean,MathlibTest/Delab/Scheme.lean |
2 |
2 |
['github-actions', 'jcommelin'] |
jcommelin assignee:jcommelin |
1-69614 1 day ago |
21-74857 21 days ago |
39-65850 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-67985 1 day ago |
2-10146 2 days ago |
2-13243 2 days |
| 24654 |
grunweg author:grunweg |
feat(lint-style): enforce modules are named in UpperCamelCase |
except for a handful of explicit exceptions
In passing, refactor the other two checks in `lint-style` to return the number of their errors (which is both meaningful and semantically clear), as opposed to a boolean (which can be accidentally inverted).
---
- [x] depends on: #23974 (right now, the linter complains about the two violations fixed in that PR)
[](https://gitpod.io/from-referrer/)
|
t-linter |
58/14 |
scripts/lint-style.lean |
1 |
17 |
['adomani', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] |
nobody |
1-67955 1 day ago |
1-74329 1 day ago |
1-79457 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-58444 1 day ago |
3-65718 3 days ago |
68-61394 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-57680 1 day ago |
1-57709 1 day ago |
15-61859 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-57493 1 day ago |
1-57493 1 day ago |
1-57546 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-54882 1 day ago |
1-54897 1 day ago |
20-32688 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-51541 1 day ago |
1-66850 1 day ago |
1-68434 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-51435 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-50925 1 day ago |
206-73158 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-50166 1 day ago |
1-56799 1 day ago |
5-54664 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-47563 1 day ago |
54-82019 1 month ago |
55-66476 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-47100 1 day ago |
82-79925 2 months ago |
85-42689 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-47050 1 day ago |
48-877 1 month ago |
65-27034 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-46900 1 day ago |
1-46900 1 day ago |
1-85801 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-46899 1 day ago |
20-30830 20 days ago |
20-30885 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-46861 1 day ago |
18-56793 18 days ago |
18-56845 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-46843 1 day ago |
17-54270 17 days ago |
17-54333 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-46540 1 day ago |
14-68133 14 days ago |
15-78964 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-46144 1 day ago |
1-46162 1 day ago |
1-46312 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-45859 1 day ago |
5-46432 5 days ago |
6-5390 6 days |
| 24796 |
erdOne author:erdOne |
feat(AlgebraicGeometry): locally directed gluing |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
433/133 |
Mathlib/AlgebraicGeometry/Gluing.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean,Mathlib/AlgebraicGeometry/Restrict.lean,Mathlib/AlgebraicGeometry/Scheme.lean |
6 |
1 |
['github-actions'] |
nobody |
1-44412 1 day ago |
2-28679 2 days ago |
2-28712 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-43781 1 day ago |
41-62064 1 month ago |
48-45201 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-40526 1 day ago |
21-84883 21 days ago |
21-85709 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-19614 1 day ago |
1-19614 1 day ago |
64-57404 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-18732 1 day ago |
1-18732 1 day ago |
1-24867 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-17801 1 day ago |
1-79735 1 day ago |
1-79785 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 |
1-12903 1 day ago |
1-21543 1 day ago |
1-21598 1 day |
| 24644 |
matthewjasper author:matthewjasper |
chore(RingTheory/DedekindDomain/AdicValuation): Use intValuation over intValuationDef |
`intValuationDef` exists so that we can prove its basic properties before defining `intValuation`, but it shouldn't be used afterwards. Change theorems which use `intValuation` in their names to actually use `intValution` and update usages.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
t-topology
label:t-algebra$ |
108/77 |
Mathlib/NumberTheory/NumberField/FinitePlaces.lean,Mathlib/RingTheory/DedekindDomain/AdicValuation.lean,Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean,Mathlib/RingTheory/LaurentSeries.lean |
4 |
4 |
['github-actions', 'kbuzzard', 'matthewjasper'] |
nobody |
1-12444 1 day ago |
1-12444 1 day ago |
5-17277 5 days |
| 22881 |
Champitoad author:Champitoad |
feat(CategoryTheory/Topos): add representability results for subobject classifier |
We add a section `Representability` at the end of `Mathlib.CategoryTheory.Topos.Classifier` where we formalize the necessary lemmas and definitions that lead to the proof of `CategoryTheory.isRepresentable_hasClassifier_iff`, which states that a category `C` has a subobject classifier if and only if the subobjects presheaf `CategoryTheory.Subobject.presheaf C` is representable (Proposition 1 in Section I.3 of Sheaves in Geometry and Logic [MM92]). The toughest part is found in definition `CategoryTheory.Classifier.fromRepresentation`, which formalizes as closely as possible the argument given in [MM92, pp. 33-34].
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-category-theory
|
251/22 |
Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/Presheaf.lean,Mathlib/CategoryTheory/Topos/Classifier.lean |
3 |
21 |
['Champitoad', 'github-actions', 'joelriou'] |
joelriou assignee:joelriou |
1-11882 1 day ago |
41-69178 1 month ago |
56-2781 56 days |
| 23349 |
BGuillemet author:BGuillemet |
feat: add LocallyLipschitzOn.lipschitzOnWith_of_isCompact and two small lemmas about Lipschitz functions |
Main feat (in Mathlib/Topology/EMetricSpace/Basic.lean): if a function `f` from an extended pseudometric space to a pseudometric space is locally Lipschitz on a compact subset `s`, then `f` is Lipschitz on `s`. The theorem is true only when the codomain of `f` is a pseudometric space, so it needs imports from Mathlib/Topology/MetricSpace.
Other small feat (in Mathlib/Analysis/Calculus/ContDiff/RCLike.lean): a function that is continuously differentiable on an open subset is locally Lipschitz on this subset.
---
- [ ] depends on: #22890
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-topology
|
59/4 |
Mathlib/Analysis/Calculus/ContDiff/RCLike.lean,Mathlib/Topology/EMetricSpace/Lipschitz.lean |
2 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
PatrickMassot assignee:PatrickMassot |
1-11844 1 day ago |
21-84376 21 days ago |
22-4735 22 days |
| 23367 |
b-reinke author:b-reinke |
feat(GroupTheory/FreeGroup/Reduce): add lemmas for toWord and reduce |
Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project.
This PR adds some simple helper lemmas for the interaction of `toWord` and `reduce` and basic list / group operations.
The RHS of the lemmas often contains more appearances of `reduce`, so they are not marked as `simp` lemmas.
---
[](https://gitpod.io/from-referrer/)
|
t-geometric-group-theory
t-algebra
label:t-algebra$ |
23/0 |
Mathlib/GroupTheory/FreeGroup/Reduce.lean |
1 |
9 |
['github-actions', 'grunweg', 'vlad902'] |
tb65536 assignee:tb65536 |
1-11612 1 day ago |
47-77202 1 month ago |
47-85878 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 |
1-11544 1 day ago |
26-79324 26 days ago |
30-46 30 days |
| 24835 |
RemyDegenne author:RemyDegenne |
feat(Probability): lemmas about variance |
- `Var[fun ω ↦ X ω + c; μ] = Var[X; μ]`. Same for `c + X`, `-X`, `X - c` and `c - X`.
- The variance of a Dirac measure is 0
- `Var[X; μ.map Y] = Var[X ∘ Y; μ]`
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
54/0 |
Mathlib/Probability/Variance.lean |
1 |
1 |
['github-actions'] |
nobody |
1-8884 1 day ago |
1-9177 1 day ago |
1-9162 1 day |
| 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 |
1-8630 1 day ago |
1-8630 1 day ago |
2-79220 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 |
1-6364 1 day ago |
1-6627 1 day ago |
1-6612 1 day |
| 24719 |
madvorak author:madvorak |
feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv` |
---
Discussion:
https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2324719.20cannot.20find.20home/with/517142655
|
t-algebra label:t-algebra$ |
10/0 |
Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean |
1 |
8 |
['eric-wieser', 'github-actions', 'madvorak'] |
nobody |
1-6108 1 day ago |
2-76398 2 days ago |
4-26228 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 |
1-4901 1 day ago |
21-7654 21 days ago |
21-7709 21 days |
| 24105 |
urkud author:urkud |
feat(Topology/UniformSpace/Path): new file |
---
- [ ] depends on: #24066
[](https://gitpod.io/from-referrer/)
|
t-topology |
112/5 |
Mathlib.lean,Mathlib/Topology/ContinuousMap/Defs.lean,Mathlib/Topology/Order/ProjIcc.lean,Mathlib/Topology/Path.lean,Mathlib/Topology/UniformSpace/CompactConvergence.lean,Mathlib/Topology/UniformSpace/Path.lean |
6 |
4 |
['ADedecker', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
1-3466 1 day ago |
7-45969 7 days ago |
7-46880 7 days |
| 24838 |
RemyDegenne author:RemyDegenne |
feat(MeasureTheory): tightness of the range of a sequence |
* `isTightMeasureSet_range_iff_tendsto_limsup_measure_norm_gt`: in a proper normed group,
the range of a sequence of measures `μ : ℕ → Measure E` is tight if and only if the function
`r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖x‖}) atTop` tends to `0` at infinity.
* `isTightMeasureSet_range_iff_tendsto_limsup_inner`: in a finite-dimensional inner product space,
the range of a sequence of measures `μ : ℕ → Measure E` is tight if and only if the function
`r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖⟪y, x⟫_𝕜‖}) atTop` tends to `0` at infinity for all `y`.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
133/2 |
Mathlib/MeasureTheory/Measure/TightNormed.lean |
1 |
2 |
['RemyDegenne', 'github-actions'] |
nobody |
1-3358 1 day ago |
1-3431 1 day ago |
1-3416 1 day |
| 7596 |
alreadydone author:alreadydone |
feat: covering maps from properly discontinuous actions and discrete subgroups |
---
- [x] depends on: #23236
[](https://gitpod.io/from-referrer/)
|
file-removed
t-topology
|
351/21 |
Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Topology/Algebra/ConstMulAction.lean,Mathlib/Topology/Algebra/Group/Pointwise.lean,Mathlib/Topology/Covering/AddCircle.lean,Mathlib/Topology/Covering/Basic.lean,Mathlib/Topology/Covering/Galois.lean,Mathlib/Topology/Homotopy/Lifting.lean,Mathlib/Topology/Instances/AddCircle.lean |
9 |
16 |
['ADedecker', 'alreadydone', 'digama0', 'github-actions', 'mathlib4-dependent-issues-bot', 'tb65536'] |
nobody |
1-3154 1 day ago |
1-67536 1 day ago |
25-72934 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 |
1-2239 1 day ago |
1-8662 1 day ago |
1-66952 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 |
1-691 1 day ago |
1-53197 1 day ago |
2-35214 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 |
1-328 1 day ago |
15-79437 15 days ago |
45-25971 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-83974 23 hours ago |
2-1994 2 days ago |
2-65498 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-78028 21 hours ago |
1-14496 1 day ago |
1-14481 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-75156 20 hours ago |
1-70579 1 day ago |
1-76693 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-72661 20 hours ago |
0-74742 20 hours ago |
6-16594 6 days |
| 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-71807 19 hours ago |
0-71807 19 hours ago |
61-12408 61 days |
| 24833 |
jcommelin author:jcommelin |
chore: swap the sides of the argument to `subtypePerm` |
This way the argument will not loop, when used with `simp`.
The argument also appears in many lemmas.
This change is a workaround for the extended simpNF linter, which runs `simp [h]` with `h` of that type.
Zulip: [#mathlib4 > simpNF lint with hyps @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/simpNF.20lint.20with.20hyps/near/517741799)
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
47/47 |
Mathlib/Algebra/Group/End.lean,Mathlib/GroupTheory/Perm/Centralizer.lean,Mathlib/GroupTheory/Perm/Cycle/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Factors.lean,Mathlib/GroupTheory/Perm/Finite.lean,Mathlib/GroupTheory/Perm/Sign.lean,Mathlib/GroupTheory/Perm/Support.lean |
7 |
10 |
['JovanGerb', 'eric-wieser', 'github-actions', 'jcommelin'] |
nobody |
0-69355 19 hours ago |
1-11296 1 day ago |
1-11347 1 day |
| 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-68793 19 hours ago |
0-68804 19 hours ago |
0-68854 19 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-64435 17 hours ago |
0-69660 19 hours ago |
0-69645 19 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-63903 17 hours ago |
0-63965 17 hours ago |
83-5481 83 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-62624 17 hours ago |
30-42793 1 month ago |
30-51746 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-61458 17 hours ago |
6-51879 6 days ago |
31-14690 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-61261 17 hours ago |
3-44465 3 days ago |
3-46022 3 days |
| 24578 |
b-mehta author:b-mehta |
feat(Pointwise): cardinality of product set in GroupWithZero |
This PR:
* generalises the assumptions to `card_le_card_image₂_left` and `card_le_card_image₂_right` and golf these: they previously required injectivity everywhere despite using it in only one place. (These lemmas were also used in exactly one place each in mathlib)
* adds `card_le_card_mul_left_of_injective` and `card_le_card_mul_right_of_injective` which generalise the typeclass assumptions on the existing `card_le_card_mul_left` and `card_le_card_mul_right`
* uses the above to add versions of `card_le_card_mul_left` and `card_le_card_mul_right` in groups with zero. This is useful for applying the pointwise constructions to fields
In fact, the first versions of all the above lemmas were written in this generality, but that was seemingly lost during an upstream.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
54/16 |
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean,Mathlib/Data/Finset/NAry.lean |
3 |
1 |
['github-actions'] |
nobody |
0-59843 16 hours ago |
5-84769 5 days ago |
10-35973 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-59825 16 hours ago |
0-59825 16 hours ago |
15-75242 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-59473 16 hours ago |
2-628 2 days ago |
2-643 2 days |
| 24752 |
MichaelStollBayreuth author:MichaelStollBayreuth |
perf(Data.Real.Sqrt): make Real.sqrt irreducible |
We try to see what happens if we make `Real.sqrt` irreducible.
There are cases where this makes unification *very* significantly faster, compare [#mathlib4 > Coercion triggers timeout @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Coercion.20triggers.20timeout/near/517177117).
---
[](https://gitpod.io/from-referrer/)
|
t-data |
1/0 |
Mathlib/Data/Real/Sqrt.lean |
1 |
18 |
['MichaelStollBayreuth', 'eric-wieser', 'github-actions', 'leanprover-bot'] |
nobody |
0-55230 15 hours ago |
2-68552 2 days ago |
2-74030 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-53514 14 hours ago |
1-8312 1 day ago |
2-64339 2 days |
| 21237 |
scholzhannah author:scholzhannah |
feat: a weaker definition of compactly generated spaces |
This PR defines compactly coherent spaces as a topological space where a set is open iff its intersection with every compact set is open in that compact set. This notion is typically called compactly generated in the literature. There is a different [definition of compactly generated spaces already in mathlib](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Compactness/CompactlyGeneratedSpace.html#CompactlyGeneratedSpace) but that definition is stronger than the one presented here. They do however agree on Hausdorff spaces. See [this wikipedia page](https://en.wikipedia.org/wiki/Compactly_generated_space) for an explanation for the three different definitions of compactly generated spaces used in literature.
Co-authored-by: Floris van Doorn
---
See also [this discussion on Zulip](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Compactly.20generated.20spaces) about compactly generated spaces.
- [x] depends on: #21134
[](https://gitpod.io/from-referrer/)
|
t-topology |
347/0 |
Mathlib.lean,Mathlib/Topology/Compactness/CompactlyCoherentSpace.lean,docs/references.bib |
3 |
22 |
['ADedecker', 'StevenClontz', 'github-actions', 'jzxia', 'mathlib4-dependent-issues-bot', 'scholzhannah', 'urkud'] |
nobody |
0-48064 13 hours ago |
0-63308 17 hours ago |
72-21965 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-47079 13 hours ago |
0-63234 17 hours ago |
11-56977 11 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-44979 12 hours ago |
0-64520 17 hours ago |
0-64905 18 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-43852 12 hours ago |
0-63181 17 hours ago |
0-64698 17 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-43317 12 hours ago |
0-47734 13 hours ago |
27-48190 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-41291 11 hours ago |
11-10503 11 days ago* |
14-12105 14 days* |
| 24868 |
plp127 author:plp127 |
feat(Tactic/Positivity): Support nonnegativity for non-strictly ordered rings. |
Change the positivity extension for multiplication to work on `IsOrderedRing` when proving nonnegativity instead of needing `IsStrictOrderedRing`.
Motivated by [#mathlib4 > `positivity` can't apply `mul_nonneg`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60positivity.60.20can't.20apply.20.60mul_nonneg.60/with/516270014).
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
29/37 |
Mathlib/Tactic/Positivity/Basic.lean,Mathlib/Tactic/Positivity/Core.lean |
2 |
4 |
['github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
nobody |
0-29690 8 hours ago |
0-29691 8 hours ago |
0-32997 9 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-25350 7 hours ago |
4-4822 4 days ago |
9-32234 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-20602 5 hours ago |
0-55383 15 hours ago |
0-55400 15 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-13797 3 hours ago |
12-52311 12 days ago |
12-64638 12 days |
| 24873 |
smmercuri author:smmercuri |
feat: `Subtype.map_ne` |
The restrictions to subtypes of two functions that never agree, also never agree.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
7/0 |
Mathlib/Data/Subtype.lean |
1 |
1 |
['github-actions'] |
nobody |
0-13724 3 hours ago |
0-13726 3 hours ago |
0-13776 3 hours |
| 24875 |
smmercuri author:smmercuri |
feat: injectivity of `InfinitePlace.embedding` |
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
15/0 |
Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-13589 3 hours ago |
0-13589 3 hours ago |
0-13644 3 hours |
| 24880 |
smmercuri author:smmercuri |
feat: predicate for ramified infinite places |
Adds `InfinitePlace.IsRamified` as a shorthand for `¬InfinitePlace.IsUnramified` plus basic API.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
16/0 |
Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean |
1 |
1 |
['github-actions'] |
nobody |
0-12350 3 hours ago |
0-12368 3 hours ago |
0-12414 3 hours |
| 24705 |
grunweg author:grunweg |
feat(workflows): automatically assign reviewers |
Once per day, automatically assign all proposed reviewers from the automatic assignment algorithm.
---
See [the github documentation](https://docs.github.com/en/rest/issues/assignees?apiVersion=2022-11-28#add-assignees-to-an-issue) for the assignment syntax.
[](https://gitpod.io/from-referrer/)
|
CI |
41/0 |
.github/workflows/auto_assign_reviewers.yaml |
1 |
3 |
['adomani', 'github-actions'] |
bryangingechen assignee:bryangingechen |
0-11449 3 hours ago |
1-70034 1 day ago |
1-70019 1 day |
| 22882 |
xroblot author:xroblot |
feat(NumberField/Units): add `regOfFamily` and refactor `regulator` |
This is a refactor of `NumberField.regulator`.
We introduce `regOfFamily` which is the regulator of a family of units indexed by `Fin (Units.rank K)`. It is equal to `0` if the family is not `isMaxRank`. This a `Prop` that says that the image of the family in the `logSpace K` is linearly independent and thus generates a full lattice. All the results about computing the `regulator` by some matrix determinant computation are now proved more generally for `regOfFamily`.
The `regulator` of a number field is still defined as the covolume of the `unitLattice` and we prove that is is also equal to `regOfFamily` of the system of fundamental units `fundSystem K`. Together with the results about computing `regOfFamily`, we recover that way the results about computing the regulator.
---
- [x] depends on: #22868
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
183/53 |
Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean,Mathlib/NumberTheory/NumberField/Units/Regulator.lean |
3 |
5 |
['alreadydone', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
0-10464 2 hours ago |
0-10484 2 hours ago |
56-31165 56 days |
| 24883 |
madvorak author:madvorak |
chore(Data/Matrix): `Matrix.submatrix` naming convention |
I'm suggesting this change for the following reasons:
(1) managing expectations — `r_reindex` looks more like a propositional argument at first glance
(2) the original naming does not do justice to its motivation — there is nothing called `r` and `c` here — it would need to be `row_reindex` and `col_reindex` or something like that (if we wanted to use the convention for naming constants even tho we are naming a variable here)
---
Old version:
https://github.com/leanprover-community/mathlib4/pull/24135 |
t-data |
11/11 |
Mathlib/Data/Matrix/ConjTranspose.lean,Mathlib/Data/Matrix/Defs.lean |
2 |
1 |
['github-actions'] |
nobody |
0-10359 2 hours ago |
0-10359 2 hours ago |
0-10350 2 hours |
| 23955 |
Louddy author:Louddy |
feat: Ideal.count_associates_eq |
Add variant of `UniqueFactorizationMonoid.count_normalizedFactors_eq` for associated Ideals.
This is convenient when you need to talk about an element as `a₀ = x ^ n * a`.
Note the file is slightly over the 1500 lines limit, I hope that is ok.
Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)>
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
35/1 |
Mathlib/RingTheory/DedekindDomain/Ideal.lean |
1 |
7 |
['Louddy', 'Ruben-VandeVelde', 'alreadydone', 'github-actions', 'grunweg'] |
kbuzzard assignee:kbuzzard |
0-9625 2 hours ago |
0-9625 2 hours ago |
27-10386 27 days |
| 24861 |
adomani author:adomani |
feat(deprecated module): automate the generation of deprecated modules |
This PR takes a step further in automating deprecated modules.
The command `#create_deprecated_modules (n)? (comment)? (write)?` generates deprecated modules.
Writing
```lean
#create_deprecated_modules 5 "These files are no longer relevant"
```
looks at the `lean` files in `Mathlib` that existed `4` commits ago
(i.e. the commit that you see with `git log -5`) and that are no longer present.
It shows how the corresponding deprecated modules should look like, using
`"These files are no longer relevant"` as the (optional) comment.
If the number of commits is not explicitly used, `#create_deprecated_modules` defaults to `2`,
namely, the commit just prior to the current one.
If the message is not explicitly used, `#create_deprecated_modules` defaults to
`"Auto-generated deprecation"`.
If you wish there to be no comment, use `#create_deprecated_modules 5 ""`.
Note that the command applies the *same* comment to all the files that it generates.
Finally, if everything looks correct, adding a final `write` actually generates the files:
```lean
#create_deprecated_modules 5 "These files are no longer relevant" write
```
---
[](https://gitpod.io/from-referrer/)
|
t-linter
maintainer-merge
|
176/0 |
scripts/README.md,scripts/create_deprecated_modules.lean |
2 |
30 |
['adomani', 'github-actions', 'grunweg'] |
grunweg assignee:grunweg |
0-7820 2 hours ago |
0-15438 4 hours ago |
0-43583 12 hours |
| 22100 |
smmercuri author:smmercuri |
feat: two inequivalent absolute values have a `< 1` and `> 1` value |
- Two absolute values `v` and `w` are equivalent if and only if `v x < 1` exactly when `w x < 1`
- Two inequivalent absolute values `v` and `w` have a point `x` at which `1 < v x` and `w x < 1`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-analysis
label:t-algebra$ |
176/0 |
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Analysis/AbsoluteValue/Equivalence.lean |
2 |
6 |
['Paul-Lez', 'github-actions', 'smmercuri'] |
faenuccio assignee:faenuccio |
0-7351 2 hours ago |
26-45867 26 days ago |
57-33213 57 days |
| 24878 |
grunweg author:grunweg |
chore: add more deprecations |
Continuation of #24871; all commits were generated semi-automatically using the script in #24681.
---
Commits can be reviewed individually; I updated mk_all in a separate commit.
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
59/0 |
Mathlib.lean,Mathlib/CategoryTheory/FullSubcategory.lean,Mathlib/RingTheory/EisensteinCriterion.lean,Mathlib/RingTheory/Polynomial/Eisenstein/Generalized.lean,Mathlib/Tactic.lean,Mathlib/Tactic/ExtractLets.lean,Mathlib/Tactic/LiftLets.lean |
7 |
2 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
0-6660 1 hour ago |
0-6796 1 hour ago |
0-12832 3 hours |
| 24885 |
xroblot author:xroblot |
chore(NumberField): minor clean up and golf |
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
22/23 |
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean,Mathlib/NumberTheory/NumberField/Units/Basic.lean,Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean |
3 |
4 |
['Ruben-VandeVelde', 'github-actions', 'xroblot'] |
nobody |
0-5818 1 hour ago |
0-5818 1 hour ago |
0-10069 2 hours |
| 24887 |
Ruben-VandeVelde author:Ruben-VandeVelde |
chore: avoid Coe.coe in PowerSeries |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
4/6 |
Mathlib/RingTheory/PowerSeries/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-5623 1 hour ago |
0-5625 1 hour ago |
0-5682 1 hour |
| 22974 |
YaelDillies author:YaelDillies |
refactor: use a junk value for the analytic order of a non-analytic function |
Currently, the order of an analytic function is called `AnalyticAt.order` and has a single explicit argument `hf : AnalyticAt 𝕜 f z₀`. This means that working with analytic functions results in contexts full of `hf.order` or, worse, `⋯.order`.
This PR makes the `f` and `z₀` arguments explicit, and drops the `hf` one by introducing a junk value of `0` for non-analytic functions. The resulting function is called `analyticOrderAt` and I am also adding a `Nat`-valued version `analyticOrderNatAt` since `(analyticOrderAt f z₀).toNat` was appearing in quite a few lemmas.
---
The same change could be performed for meromorphic functions once you are convinced.
[](https://gitpod.io/from-referrer/)
|
t-analysis |
289/164 |
Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Analytic/Order.lean,Mathlib/Analysis/Meromorphic/NormalForm.lean,Mathlib/Analysis/Meromorphic/Order.lean,Mathlib/Data/ENat/Basic.lean |
5 |
37 |
['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'loefflerd', 'sgouezel', 'urkud'] |
nobody |
0-4737 1 hour ago |
0-10402 2 hours ago |
50-77543 50 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 |
0-4525 1 hour ago |
8-59132 8 days ago |
8-59187 8 days |
| 24888 |
YaelDillies author:YaelDillies |
feat: `s \ {a ∈ s | p a} = {a ∈ s | ¬ p a}` |
I wrote this for #22974, but it isn't needed there in the end.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
3/0 |
Mathlib/Data/Set/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-4436 1 hour ago |
0-4439 1 hour ago |
0-4487 1 hour |
| 22078 |
Louddy author:Louddy |
feat(SkewMonoidAlgebra): multiplication and algebraic instances |
# Multiplication and Algebraic Instances
In this PR, we introduce the definition of the skewed convolution product on `SkewMonoidAlgebra k G`. Here, the product of two elements `f g : SkewMonoidAlgebra k G` is the finitely supported function whose value at `a` is the sum of `f x * (x • g y)` over all pairs `x, y` such that `x * y = a`.
We also introduce the associated algebraic instances.
## Context
This is the third part of a planned series of PRs aiming to formalise skew monoid algebras.
The PRs are split to ease the review process. The moral sum of these planned PRs is #10541.
The first and second part were #15878 and #19084.
Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)>
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-algebra
label:t-algebra$ |
453/45 |
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean |
1 |
57 |
['AntoineChambert-Loir', 'Louddy', 'github-actions', 'kbuzzard'] |
nobody |
0-4367 1 hour ago |
0-4367 1 hour ago |
72-24898 72 days |
| 24889 |
Kha author:Kha |
chore: do not include cache requests in build benchmark |
|
|
5/2 |
scripts/bench/temci-config.run.yml |
1 |
1 |
['Kha', 'github-actions'] |
nobody |
0-4043 1 hour ago |
0-4113 1 hour ago |
0-4097 1 hour |
| 24254 |
Louddy author:Louddy |
feat: valuation on RatFunc which is trivial on constants |
Given a valuation `v` on `RatFunc K` that is trivial on the constants `K`, the valuation on `RatFunc.X` determines to some degree the valuation on any `p : Polynomial K`.
These are important in the context of Ostrowski's theorem for `RatFunc K`.
Note that the condition that the valuation is trivial on constants is automatically fulfilled when `K` is finite.
Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)>
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
58/0 |
Mathlib/FieldTheory/RatFunc/AsPolynomial.lean |
1 |
14 |
['Louddy', 'faenuccio', 'github-actions', 'mariainesdff'] |
nobody |
0-2925 48 minutes ago |
0-7520 2 hours ago |
1-1024 1 day |
| 24890 |
grunweg author:grunweg |
style: fix bad tactic indentation |
---
Presumably not exhaustive.
[](https://gitpod.io/from-referrer/)
|
|
24/24 |
Mathlib/Analysis/Analytic/Basic.lean,Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean,Mathlib/Data/Complex/Norm.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Matroid/Loop.lean,Mathlib/Data/Nat/BitIndices.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/GroupTheory/Exponent.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean,Mathlib/RingTheory/Smooth/StandardSmooth.lean,Mathlib/Topology/Algebra/WithZeroTopology.lean,Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean |
12 |
1 |
['github-actions'] |
nobody |
0-1985 33 minutes ago |
0-3910 1 hour ago |
0-3894 1 hour |
| 24121 |
smorel394 author:smorel394 |
feat(RingTheory/Coalgebra/Equiv, RingTheory/Bialgebra/Equiv): constructors for coalgebra and bialgebra equivalences |
Add constructors for equivalences of coalgebras and bialgebras, similar to what already exists for equivalences of algebras:
- `CoalgEquiv.ofCoalgHom` constructs a `CoalgEquiv` from a `CoalgHom` that has an inverse;
- `CoalgEquiv.ofBijective` constructs a `CoalgEquiv` from a bijective `CoalgHom`;
- `BialgEquiv.ofBialgHom` constructs a `BialgEquiv` from a `CoalgHom` that has an inverse;
- `BialgEquiv.ofBijective` constructs a `BialgEquiv` from a bijective `BialgHom`.
Also add some `apply` and `coe` lemmas, following the same model as for `AlgEquiv`s.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
73/0 |
Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Coalgebra/Equiv.lean |
2 |
8 |
['github-actions', 'riccardobrasca', 'smorel394'] |
riccardobrasca assignee:riccardobrasca |
0-1923 32 minutes ago |
27-60359 27 days ago |
27-60428 27 days |
| 24892 |
Ruben-VandeVelde author:Ruben-VandeVelde |
fix: add missing simps projections for ContinuousAddEquiv |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
1/0 |
Mathlib/Topology/Algebra/ContinuousMonoidHom.lean |
1 |
1 |
['github-actions'] |
nobody |
0-1686 28 minutes ago |
0-1688 27 minutes ago |
0-1738 28 minutes |
| 24344 |
erdOne author:erdOne |
feat: miscellaneous lemmas about transcedence bases |
---
- [x] depends on: #24806
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
198/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/AlgebraicIndependent/Basic.lean,Mathlib/RingTheory/AlgebraicIndependent/Defs.lean,Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean,Mathlib/RingTheory/Norm/Basic.lean |
13 |
31 |
['acmepjz', 'alreadydone', 'erdOne', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
alreadydone assignee:alreadydone |
0-1247 20 minutes ago |
0-46873 13 hours ago |
18-44013 18 days |
| 24876 |
kebekus author:kebekus |
feat: introduce the Proximity Function of Value Distribution Theory |
Define the "proximity function" attached to a meromorphic function defined on the complex plane. Also known as the "Nevanlinna Proximity Function", this is one of the three main functions used in Value Distribution Theory.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
97/0 |
Mathlib.lean,Mathlib/Analysis/Complex/ValueDistribution/ProximityFunction.lean |
2 |
2 |
['github-actions', 'jcommelin'] |
nobody |
0-425 7 minutes ago |
0-13205 3 hours ago |
0-13256 3 hours |
| 24816 |
ciskiko author:ciskiko |
feat(GroupTheory): add Regular Wreath Product |
feat: add regular wreath product and some results; add iterated wreath product; add the isomorphism of iterated wreath product of Z_p to sylow p subgroup of S_{p^n}.
Needs some work simplifying final result.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
299/0 |
Mathlib.lean,Mathlib/GroupTheory/RegularWreathProduct.lean |
2 |
15 |
['ciskiko', 'github-actions', 'tb65536'] |
tb65536 assignee:tb65536 |
0-51 51 seconds ago |
0-84186 23 hours ago |
1-22216 1 day |