Welcome to the mathlib review page. Everybody's help with reviewing is appreciated. Reviewing contributions is important, and everybody is welcome to review pull requests! If you're not sure how, the pull request review guide is there to help you.
This page contains tables of
| Number |
Author |
Title |
Description |
Labels |
+/- |
Modified files (first 100) |
📝 |
💬 |
All users who commented or reviewed |
Assignee(s) |
Updated |
Last status change |
total time in review |
| 21129 |
chrisflav author:chrisflav |
perf(RingTheory/Kaehler/JacobiZariski): reorder universe variables |
Naming of universe variables has an impact on universe unification. It seems to matter that the universe variables of `R`, `S` and `T` appear before the universe variables of the generators in alphabetical order.
---
[](https://gitpod.io/from-referrer/)
|
performance-hack
t-algebra
label:t-algebra$ |
18/20 |
Mathlib/RingTheory/Kaehler/JacobiZariski.lean |
1 |
37 |
['chrisflav', 'erdOne', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'mattrobball'] |
nobody |
63-44557 2 months ago |
97-47018 3 months ago |
106-28322 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 |
42-86090 1 month ago |
42-86090 1 month ago |
46-74265 46 days |
| 23684 |
alreadydone author:alreadydone |
feat(RingTheory): integral extensions of comm. rings are local homs |
---
The import increase only affects one file so I hope it's okay.
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
57/64 |
Mathlib/Algebra/Field/Equiv.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/Proper.lean,Mathlib/FieldTheory/LinearDisjoint.lean,Mathlib/LinearAlgebra/Dimension/Localization.lean,Mathlib/RingTheory/Artinian/Ring.lean,Mathlib/RingTheory/IntegralClosure/Algebra/Defs.lean,Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean,Mathlib/RingTheory/LinearDisjoint.lean,Mathlib/RingTheory/Localization/FractionRing.lean,Mathlib/RingTheory/Localization/Integral.lean,Mathlib/RingTheory/SimpleRing/Field.lean |
12 |
4 |
['alreadydone', 'github-actions', 'xroblot'] |
nobody |
38-49677 1 month ago |
38-81075 1 month ago |
38-81096 38 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-26496 1 month ago |
37-21564 1 month ago |
84-8389 84 days |
| 22474 |
joelriou author:joelriou |
feat(CategoryTheory/Functor): more API for pointwise Kan extensions |
Transport pointwise Kan extensions via isomorphisms/equivalences.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
157/7 |
Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean,Mathlib/CategoryTheory/Limits/HasLimits.lean,Mathlib/CategoryTheory/Limits/Opposites.lean,Mathlib/CategoryTheory/Limits/Shapes/Products.lean |
4 |
1 |
['github-actions'] |
nobody |
34-48266 1 month ago |
70-52129 2 months ago |
71-82401 71 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-27276 29 days ago |
29-28577 29 days ago |
29-28632 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 |
28-86128 28 days ago |
29-3540 29 days ago |
29-3523 29 days |
| 24065 |
kim-em author:kim-em |
chore: script to give topological sort of modules |
This script is not useful by itself: it just gives a topological sort of Mathlib's import graph. But I've several times found it useful when I want to modify many files systematically with minimal rebuilding: just work backwards through the list.
|
|
96/0 |
scripts/README.md,scripts/topological_sort.py |
2 |
4 |
['github-actions', 'jcommelin', 'kim-em'] |
nobody |
28-55057 28 days ago |
28-66095 28 days ago |
28-66078 28 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-5555 28 days ago |
28-36205 28 days ago |
40-3127 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 |
27-68849 27 days ago |
27-68849 27 days ago |
36-14702 36 days |
| 22039 |
YaelDillies author:YaelDillies |
feat: simproc for computing `Finset.Ixx` of natural numbers |
---
- [x] depends on: #22290
- [x] depends on: #22559
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
315/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Simproc/FinsetInterval.lean,Mathlib/Util/Qq.lean |
4 |
58 |
['FLDutchmann', 'Paul-Lez', 'YaelDillies', 'eric-wieser', 'github-actions', 'kim-em', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'urkud'] |
nobody |
27-44309 27 days ago |
27-44327 27 days ago |
83-5049 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-7592 26 days ago |
26-7592 26 days ago |
68-74924 68 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-2113 26 days ago |
37-16 1 month ago |
211-24778 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-360 25 days ago |
34-60361 1 month ago |
47-8234 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-25726 24 days ago |
29-7740 29 days ago |
29-7792 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 |
23-76874 23 days ago |
unknown |
unknown |
| 23964 |
BoltonBailey author:BoltonBailey |
docs: Add documentation arbitrarily |
@mattrobball asked in the Mathlib Community meeting today what it would look like if we asked Claude code to give us improved documentation. I made this draft PR by selecting five declarations arbitrarily from `nolints.json` and asking Cursor to document them.
---
[](https://gitpod.io/from-referrer/)
|
documentation |
52/14 |
Mathlib/Algebra/Homology/Homotopy.lean,Mathlib/Analysis/BoxIntegral/Partition/Filter.lean,Mathlib/Control/Monad/Cont.lean,Mathlib/Data/Stream/Defs.lean,Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean |
5 |
10 |
['ADedecker', 'BoltonBailey', 'eric-wieser', 'github-actions', 'jcommelin', 'mattrobball'] |
nobody |
23-54529 23 days ago |
31-8972 1 month ago |
31-71990 31 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-21047 23 days ago |
23-36107 23 days ago |
23-36097 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-4733 23 days ago |
48-32860 1 month ago |
48-32982 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 |
21-82728 21 days ago |
55-44349 1 month ago |
55-46244 55 days |
| 24257 |
quangvdao author:quangvdao |
feat(Data/PFunctor/Univariate): Generalize universe level in `PFunctor` |
This PR generalizes `PFunctor` to have potentially different universe levels for its `A` and `B` fields. This is to aid with my formalization attempt (with @dtumad ) of poly functors [here](https://github.com/dtumad/VCV-io/blob/master/ToMathlib/PFunctor/Basic.lean) (in order to model interactive systems in general, and cryptographic protocols in particular).
There is no plan yet to need `MvPFunctor`, so I do not generalize universe levels of that for now.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
29/25 |
Mathlib/Control/Functor.lean,Mathlib/Data/PFunctor/Univariate/Basic.lean,Mathlib/Data/PFunctor/Univariate/M.lean,Mathlib/Data/QPF/Univariate/Basic.lean |
4 |
4 |
['alexkeizer', 'github-actions'] |
nobody |
21-28572 21 days ago |
22-17395 22 days ago |
22-17450 22 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-9829 21 days ago |
21-9894 21 days ago |
21-9877 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-18766 20 days ago |
20-18769 20 days ago |
20-20361 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 |
19-75938 19 days ago |
19-75938 19 days ago |
20-11018 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 |
19-61309 19 days ago |
20-9291 20 days ago |
21-79916 21 days |
| 23926 |
b-reinke author:b-reinke |
feat(Algebra/BigOperators/Finprod): add powerset projection lemmas |
This PR adds lemmas in `Mathlib/Algebra/BigOperators/Finprod.lean` related to products/sums over the powerset `𝒫 s` when we add or remove an element of `s`.
The motivation comes from the proof of the deletion/contraction properties of matroids.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
30/0 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Image.lean |
2 |
5 |
['b-reinke', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
19-51643 19 days ago |
19-53435 19 days ago |
32-53958 32 days |
| 18693 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: add ConjRootClass |
Co-authored-by: FR
---
From #6718
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
213/0 |
Mathlib.lean,Mathlib/FieldTheory/Minpoly/ConjRootClass.lean,Mathlib/FieldTheory/Minpoly/IsConjRoot.lean |
3 |
13 |
['LessnessRandomness', 'Vierkantor', 'alreadydone', 'github-actions', 'grunweg'] |
nobody |
19-16893 19 days ago |
19-54656 19 days ago |
81-36401 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-2904 18 days ago |
18-2904 18 days ago |
38-77120 38 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-12192 17 days ago |
17-12192 17 days ago |
17-12252 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-42708 16 days ago |
16-44692 16 days ago |
20-32124 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-41406 16 days ago |
28-13471 28 days ago |
68-7079 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-35494 16 days ago |
20-25732 20 days ago |
20-50972 20 days |
| 24412 |
pechersky author:pechersky |
feat(UniformSpace/Ultra/Constructions): IsUltraUniformity.{bot,top} |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
29/0 |
Mathlib/Order/Filter/Bases/Basic.lean,Mathlib/Topology/UniformSpace/Defs.lean,Mathlib/Topology/UniformSpace/Ultra/Basic.lean,Mathlib/Topology/UniformSpace/Ultra/Constructions.lean |
4 |
1 |
['github-actions'] |
nobody |
16-25718 16 days ago |
16-25874 16 days ago |
16-25868 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-11484 16 days ago |
69-43387 2 months ago |
69-43369 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 |
15-74719 15 days ago |
15-83412 15 days ago |
15-83396 15 days |
| 22961 |
xroblot author:xroblot |
feat(ZLattice/Covolume): add `covolume_div_covolume_eq_relindex` |
Add the following result:
Let `L₁` be a sub-`ℤ`-lattice of `L₂`. Then the index of `L₁` inside `L₂` is equal to `covolume L₁ / covolume L₂`.
---
- [x] depends on: #22940
- [x] depends on: #23759
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
66/4 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Algebra/Module/ZLattice/Covolume.lean,Mathlib/GroupTheory/Index.lean,Mathlib/LinearAlgebra/Determinant.lean |
4 |
10 |
['Ruben-VandeVelde', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'xroblot'] |
nobody |
15-49946 15 days ago |
15-49962 15 days ago |
52-6122 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-36707 14 days ago |
14-36707 14 days ago |
15-24065 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-33581 14 days ago |
14-33581 14 days ago |
14-38965 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-30767 14 days ago |
14-30768 14 days ago |
39-51353 39 days |
| 24448 |
Hagb author:Hagb |
feat(RingTheory/Ideal/Span.lean): some lemmas about zero and span |
`simp` would be able to solve them.
Notice that `span_singleton_zero : span {(0 : R)} = ⊥` itself can be solved by `simp` without this commit, which uses `span_singleton_eq_bot : span ({x} : Set α) = ⊥ ↔ x = 0`, while `simp` cannot solve goals like `f (Ideal.span {(0 : R)}) = f ⊥`, which would be solvable by `simp` with `span_singleton_zero` marked with `@[simp]`.
Without adding also `Ideal.dvd_span_bot` to `Mathlib/RingTheory/DedekindDomain/Ideal.lean`, these lemmas on `Span.lean` would make the following failed, since `simp` would rewrite `{0}` with `⊥` and result in a goal `v.asIdeal ∣ ⊥` that it can't solve.
https://github.com/leanprover-community/mathlib4/blob/3f2556372f27171259a381d4d57db71440700cd8/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean#L123
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
16/1 |
Mathlib/Algebra/Module/PID.lean,Mathlib/RingTheory/DedekindDomain/Ideal.lean,Mathlib/RingTheory/Ideal/Span.lean |
3 |
1 |
['github-actions'] |
nobody |
14-26295 14 days ago |
14-36286 14 days ago |
14-36340 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-4217 14 days ago |
33-20107 1 month ago |
33-20905 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-4144 14 days ago |
14-4144 14 days ago |
30-23589 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 |
13-76442 13 days ago |
16-11232 16 days ago |
21-833 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-38084 13 days ago |
13-39162 13 days ago |
13-39229 13 days |
| 24497 |
Parcly-Taxel author:Parcly-Taxel |
feat: IMO 1985 Q2 |
|
IMO |
100/0 |
Archive.lean,Archive/Imo/Imo1985Q2.lean |
2 |
1 |
['github-actions'] |
nobody |
12-46608 12 days ago |
12-46671 12 days ago |
12-46655 12 days |
| 24380 |
chrisflav author:chrisflav |
chore(RingTheory/TensorProduct): more product compatibilities |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
48/4 |
Mathlib/RingTheory/TensorProduct/Pi.lean |
1 |
3 |
['erdOne', 'github-actions'] |
nobody |
12-38167 12 days ago |
12-38167 12 days ago |
13-82528 13 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-35472 12 days ago |
12-37601 12 days ago |
12-45740 12 days |
| 24517 |
upobir author:upobir |
feat(Algebra/QuadraticDiscriminant): Adding inequalities on quadratic from inequalities on discriminant |
---
This pr adds inequalities that relate `0` and `a * (x * x) + b * x + c` from inequalities of `a` and `discrim a b c`. For example, negative discriminant and negative leading coefficient implies value of quadratic expression is always negative and similar.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
35/0 |
Mathlib/Algebra/QuadraticDiscriminant.lean |
1 |
1 |
['github-actions'] |
nobody |
12-25535 12 days ago |
12-25535 12 days ago |
12-25588 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-18627 12 days ago |
12-18828 12 days ago |
12-18884 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-16056 12 days ago |
12-18697 12 days ago |
21-3839 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 |
11-83856 11 days ago |
12-29547 12 days ago |
36-46393 36 days |
| 24245 |
JovanGerb author:JovanGerb |
feat(Geometry/Euclidean/SignedDist): `signedDist` between two points |
This PR defines `signedDist`, the signed distance between two points.
It redefines `signedInfDist` so that it uses `signedDist`.
The motivation is to use this in IMO2020Q6. Additionally this definition will be useful for properly reasoning about the power of a point
[#mathlib4 > Signed distance between points](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Signed.20distance.20between.20points)
some comments:
* should `signedDistLinear` be `private`?
* should `signedDist` and `signedInfDist` be made continuous bunled maps in this PR?
* I'm not too happy about the hypothesis in `signedDist_congr (h : ∃ r > (0 : ℝ), r • v = w)`. This relationship between `v` and `w` is a symmetric one that should have some API around it, similar to `SameRay`. It could also be spelled as `(ℝ≥0 ∙ v) = ℝ≥0 ∙ w`
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
206/23 |
Mathlib/Analysis/InnerProductSpace/Basic.lean,Mathlib/Geometry/Euclidean/SignedDist.lean,Mathlib/Topology/MetricSpace/Pseudo/Defs.lean |
3 |
1 |
['github-actions'] |
nobody |
11-52166 11 days ago |
11-52166 11 days ago |
22-68738 22 days |
| 24533 |
robertmaxton42 author:robertmaxton42 |
feat (ULift): conjugation by ULift.up/down, misc cast/heq lemmas |
* Adds the convenience def `ULift.conj x := `down (f (up x))`, and corresponding basic lemmas
* Adds lemmas showing that `ULift.up` and `.down` commute with casts and preserve `HEq`.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
31/0 |
Mathlib/Data/ULift.lean |
1 |
14 |
['eric-wieser', 'github-actions', 'robertmaxton42'] |
nobody |
11-47373 11 days ago |
11-47373 11 days ago |
11-55289 11 days |
| 24379 |
chrisflav author:chrisflav |
feat(Algebra/AlgHom): `Unique` if target is `Subsingleton` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
32/0 |
Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/Algebra/Hom.lean |
2 |
5 |
['chrisflav', 'eric-wieser', 'github-actions'] |
nobody |
11-37332 11 days ago |
12-37613 12 days ago |
12-73551 12 days |
| 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 |
7 |
['Ruben-VandeVelde', 'chrisflav', 'github-actions', 'mistarro'] |
nobody |
11-27936 11 days ago |
12-9788 12 days ago |
12-22115 12 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 |
10-84209 10 days ago |
11-2871 11 days ago |
47-48026 47 days |
| 24266 |
plp127 author:plp127 |
feat(Order): `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)` |
Proves that `NoBotOrder α` implies `NoMinOrder α` under `IsDirected α (· ≥ ·)`, and also the dual theorem.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
14/0 |
Mathlib/Order/Directed.lean |
1 |
4 |
['github-actions', 'plp127', 'urkud'] |
nobody |
10-71939 10 days ago |
21-83320 21 days ago |
21-83304 21 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 |
10-70578 10 days ago |
12-28315 12 days ago |
12-28368 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 |
10-57265 10 days ago |
10-57282 10 days ago |
84-7562 84 days |
| 23498 |
Ruben-VandeVelde author:Ruben-VandeVelde |
chore(Topology.MetricSpace.Lipschitz): stop depending on Topology.Algebra |
Noticed while playing with the new `directoryDependency` linter. Not sure if these could be proved without assuming the continuity of real multiplication.
Copyright from https://github.com/leanprover-community/mathlib3/pull/1921 and https://github.com/leanprover-community/mathlib4/pull/11840.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
60/34 |
Mathlib.lean,Mathlib/Analysis/Normed/Group/AddTorsor.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Analysis/SpecialFunctions/Exp.lean,Mathlib/Topology/Algebra/MetricSpace/Lipschitz.lean,Mathlib/Topology/MetricSpace/Algebra.lean,Mathlib/Topology/MetricSpace/IsometricSMul.lean,Mathlib/Topology/MetricSpace/Lipschitz.lean,Mathlib/Topology/MetricSpace/PiNat.lean |
9 |
1 |
['github-actions'] |
nobody |
10-55076 10 days ago |
10-55076 10 days ago |
43-34800 43 days |
| 23360 |
kim-em author:kim-em |
chore: review of `erw` in `Algebra/Homology/DerivedCategory` |
|
t-algebra label:t-algebra$ |
21/15 |
Mathlib/Algebra/Homology/DerivedCategory/Basic.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean,Mathlib/Algebra/Homology/DerivedCategory/SingleTriangle.lean,Mathlib/Algebra/Homology/HomotopyCategory/SingleFunctors.lean,Mathlib/CategoryTheory/Shift/SingleFunctors.lean |
5 |
2 |
['Ruben-VandeVelde', 'github-actions'] |
nobody |
10-55064 10 days ago |
10-55064 10 days ago |
47-66532 47 days |
| 23676 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprime `induction'` for localizations and quotients |
All these removed instances of `induction'` generate only one subgoal. In some cases `obtain` can be used.
The relevant instances were identified by adding the following to `Mathlib.Tactic.Cases`
```diff
diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean
index 4a60db6c551..08c06520879 100644
--- a/Mathlib/Tactic/Cases.lean
+++ b/Mathlib/Tactic/Cases.lean
@@ -122,6 +122,16 @@ elab (name := induction') "induction' " tgts:(Parser.Tactic.elimTarget,+)
g.assign result.elimApp
let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
(generalized := fvarIds) (toClear := targetFVarIds) (toTag := toTag)
+ let body ← inferType targets[0]!
+ let names : Array Format := if withArg.1.getArgs.size > 1 then
+ (withArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+ let gens : Array Format := if genArg.1.getArgs.size > 1 then
+ (genArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+ let inductor : Format := if usingArg.1.getArgs.size > 1 then
+ Syntax.prettyPrint usingArg.1.getArgs[1]! else "~"
+ if subgoals.toList.length ≤ 1 then
+ logInfoAt tgts m!"{body.getAppFn.setPPExplicit true} {inductor} {gens} {names} \
+ {subgoals.toList.length}"
setGoals <| (subgoals ++ result.others).toList ++ gs
/-- The `cases'` tactic is similar to the `cases` tactic in Lean 4 core, but the syntax for giving
```
and then examining [the output](https://github.com/leanprover-community/mathlib4/actions/runs/14270845291/job/40003467676). |
tech debt |
94/113 |
Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Pointwise/Stabilizer.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Limits/Types/Colimits.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Finsupp/BigOperators.lean,Mathlib/Data/Fintype/Quotient.lean,Mathlib/Data/List/Cycle.lean,Mathlib/Data/Nat/ChineseRemainder.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/FieldTheory/RatFunc/Basic.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/GroupTheory/OreLocalization/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Concrete.lean,Mathlib/GroupTheory/Perm/Sign.lean,Mathlib/GroupTheory/Torsion.lean,Mathlib/RingTheory/OreLocalization/Basic.lean,Mathlib/RingTheory/OreLocalization/Ring.lean,Mathlib/SetTheory/Surreal/Basic.lean |
25 |
10 |
['Parcly-Taxel', 'apnelson1', 'eric-wieser', 'github-actions', 'grunweg', 'urkud'] |
nobody |
10-52528 10 days ago |
10-53571 10 days ago |
38-27891 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-25127 10 days ago |
10-54084 10 days ago |
26-41727 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-22199 10 days ago |
10-39269 10 days ago |
12-7569 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-18045 10 days ago |
10-18061 10 days ago |
21-662 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-15662 10 days ago |
11-33729 11 days ago |
11-49240 11 days |
| 24567 |
joelriou author:joelriou |
feat(CategoryTheory): the shift functors on the localized category are linear |
If `L : C ⥤ D` is a localization functor with respect to `W : MorphismProperty C` and both `C` and `D` have been equipped with `R`-linear category structures such that `L` is `R`-linear and the shift functors on `C` are `R`-linear, then the shift functors on `D` are `R`-linear.
---
- [x] depends on: #24309
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
48/0 |
Mathlib.lean,Mathlib/CategoryTheory/Shift/Linear.lean |
2 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
10-7476 10 days ago |
10-7484 10 days ago |
10-7468 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 |
9-72773 9 days ago |
9-72828 9 days ago |
9-72823 9 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 |
9-68698 9 days ago |
78-70340 2 months ago |
78-70466 78 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 |
9-63069 9 days ago |
9-72287 9 days ago |
9-72281 9 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-36942 9 days ago |
9-36966 9 days ago |
9-36950 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 |
8-57987 8 days ago |
9-58340 9 days ago |
9-58388 9 days |
| 23368 |
b-reinke author:b-reinke |
feat(GroupTheory/FreeGroup/ReducedWords): add theory of reduced words |
Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project.
This PR adds the file `GroupTheory/FreeGroup/ReducedWords.lean`, where the predicate of reduced words is defined. It is shown that `reduce` and `toWord` produce reduced words.
This is done in preparation for the theory of cyclically reduced words.
---
[](https://gitpod.io/from-referrer/)
|
t-geometric-group-theory
t-algebra
label:t-algebra$ |
109/0 |
Mathlib.lean,Mathlib/GroupTheory/FreeGroup/ReducedWords.lean |
2 |
28 |
['b-reinke', 'github-actions', 'vlad902'] |
nobody |
8-55439 8 days ago |
47-34659 1 month ago |
47-42490 47 days |
| 24480 |
mariainesdff author:mariainesdff |
feat(RingTheory/DividedPowers/SubPDIdeal): add SubDPIdeal |
Let `A` be a commutative (semi)ring and let `I` be an ideal of `A` with a divided power
structure `hI`. A subideal `J` of `I` is a *sub-dp-ideal* of `(I, hI)` if, for all `n ∈ ℕ > 0` and
all `x ∈ J`, `hI.dpow n x ∈ J`.
The "TODOs" listed on the file docstring have been formalized by the authors and will be added in subsequent PRs.
Co-authored-by: @AntoineChambert-Loir
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-number-theory
label:t-algebra$ |
387/0 |
Mathlib.lean,Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean |
2 |
1 |
['github-actions'] |
nobody |
8-45102 8 days ago |
13-25251 13 days ago |
13-25246 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-41065 8 days ago |
29-17456 29 days ago |
53-6907 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-28753 8 days ago |
8-28753 8 days ago |
8-28813 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-20714 8 days ago |
16-18607 16 days ago |
63-24692 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-8134 8 days ago |
8-8134 8 days ago |
13-16090 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 |
7-70188 7 days ago |
11-78874 11 days ago |
26-6777 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 |
7-61749 7 days ago |
9-63091 9 days ago |
36-20894 36 days |
| 24616 |
bwehlin author:bwehlin |
feat(MeasureTheory/Measure/Dirac): Dirac measure applied to a measurable set is either 0 or 1 |
The Dirac measure at a point `a`, applied to a set `s`, is either 0 or 1. This feature provides two if and only ifs that can be used to turn statements in terms of `\ne` into statements in terms of `=`, as well as a "0 or 1 theorem".
(The reason for adding these is to avoid having to simplify in terms of `Set.indicator` over and over while working with Dirac) |
new-contributor
t-measure-probability
|
15/0 |
Mathlib/MeasureTheory/Measure/Dirac.lean |
1 |
1 |
['github-actions'] |
nobody |
7-41112 7 days ago |
8-16609 8 days ago |
8-16664 8 days |
| 23909 |
grunweg author:grunweg |
chore: various fixes for the flexible linter |
---
[](https://gitpod.io/from-referrer/)
|
|
117/83 |
Mathlib/Condensed/Light/Epi.lean,Mathlib/Control/EquivFunctor/Instances.lean,Mathlib/Control/Monad/Cont.lean,Mathlib/Data/FinEnum.lean,Mathlib/Data/Finsupp/MonomialOrder.lean,Mathlib/Data/List/Sigma.lean,Mathlib/Data/List/SplitBy.lean,Mathlib/Data/Matroid/Sum.lean,Mathlib/Data/Ordmap/Invariants.lean,Mathlib/Data/Real/Pi/Irrational.lean,Mathlib/Data/Seq/Parallel.lean,Mathlib/Data/Vector3.lean,Mathlib/Data/WSeq/Relation.lean,Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean,Mathlib/GroupTheory/CoprodI.lean,Mathlib/GroupTheory/Coxeter/Basic.lean,Mathlib/GroupTheory/Coxeter/Inversion.lean,Mathlib/GroupTheory/Goursat.lean,Mathlib/GroupTheory/HNNExtension.lean,Mathlib/GroupTheory/Nilpotent.lean,Mathlib/NumberTheory/Dioph.lean,Mathlib/NumberTheory/FLT/Polynomial.lean,Mathlib/NumberTheory/LSeries/Injectivity.lean,Mathlib/Probability/Kernel/Condexp.lean,Mathlib/RingTheory/Derivation/MapCoeffs.lean,Mathlib/RingTheory/Frobenius.lean,Mathlib/SetTheory/Ordinal/Notation.lean,Mathlib/SetTheory/ZFC/Rank.lean,Mathlib/Tactic/NormNum/NatFactorial.lean |
29 |
11 |
['b-mehta', 'github-actions', 'grunweg', 'jcommelin', 'leanprover-community-bot-assistant'] |
nobody |
7-25858 7 days ago |
7-25877 7 days ago |
32-23013 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-23741 7 days ago |
21-38884 21 days ago |
40-40348 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-20764 7 days ago |
7-62197 7 days ago |
7-62248 7 days |
| 24492 |
Parcly-Taxel author:Parcly-Taxel |
chore: remove some adaptation notes |
|
tech debt |
15/32 |
Mathlib/Algebra/Homology/Single.lean,Mathlib/Combinatorics/Enumerative/DyckWord.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Int/Cast/Basic.lean,Mathlib/NumberTheory/DiophantineApproximation/Basic.lean |
5 |
12 |
['JovanGerb', 'Parcly-Taxel', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] |
nobody |
6-55459 6 days ago |
6-55475 6 days ago |
11-49734 11 days |
| 24361 |
Hagb author:Hagb |
feat(Data/Finsupp/MonomialOrder): `0 ≤ a` where `a : m.syn` |
`simp` would be able to solve it.
---
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
easy
|
3/0 |
Mathlib/Data/Finsupp/MonomialOrder.lean |
1 |
1 |
['github-actions'] |
nobody |
6-51366 6 days ago |
6-51366 6 days ago |
18-53044 18 days |
| 24236 |
YaelDillies author:YaelDillies |
feat: closed submodules |
Define closed `R`-submodules.
The plan is to redefine proper `R`-cones as closed `R≥0`-submodules.
From Toric
---
- [x] depends on: #24230
[](https://gitpod.io/from-referrer/)
|
toric
t-topology
|
180/0 |
Mathlib.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean |
2 |
14 |
['YaelDillies', 'b-mehta', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
6-50024 6 days ago |
6-50098 6 days ago |
18-84040 18 days |
| 20171 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): define turanDensity |
Define the Turán density `turanDensity H` of a simple graph `H`: `turanDensity H` is the limit of `extremalNumber n H / n.choose 2` as `n` approaches `∞`.
Also prove
- the Turán density of a simple graph is well-defined, that is, the limit `extremalNumber n H / n.choose 2` as `n` approaches `∞` exists,
- `extremalNumber n H` is asymptotically equivalent to `turanDensity H * n.choose 2` as `n` approaches `∞`.
---
- [x] depends on: #19865
- [x] depends on: #20681
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
182/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/TuranDensity.lean,Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Data/Sym/Sym2.lean |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
6-49402 6 days ago |
6-49446 6 days ago |
6-51441 6 days |
| 20240 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): prove the Kővári–Sós–Turán theorem |
Prove the Kővári–Sós–Turán theorem for simple graphs: the `(completeBipartiteGraph α β).Free` simple graphs for `card α ≤ card β` on the vertex type `V` have at most `(card β-1)^(1/(card α))*(card V)^(2-1/(card α))/2 + (card V)*(card α-1)/2` edges.
---
- [x] depends on: #19865
- [x] depends on: #20738
I'd like to make `aux` not private in the `KovariSosTuran` namespace to enable reuse of the double-counting here, but I don't know what to call it.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
289/0 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/KovariSosTuran.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
6-47606 6 days ago |
14-78177 14 days ago |
14-78712 14 days |
| 22151 |
alreadydone author:alreadydone |
feat(RingTheory): a semiprimary ring is Noetherian/Artinian iff its Jacobson radical is fg |
A key fact used is `Module.FG.smul`: if `I` is a two-sided ideal of `R` that is f.g. as a left ideal and `N` is a f.g. `R`-module, then `I • M` is also a f.g. `R`-module.
Many lemmas about coprimality of ideals are also generalized to the noncommutative, two-sided setting.
---
- [x] depends on: #21904
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
215/155 |
Mathlib/Algebra/Algebra/Operations.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean,Mathlib/RingTheory/Extension.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/Finiteness/Ideal.lean,Mathlib/RingTheory/HopkinsLevitzki.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/Ideal/Operations.lean |
8 |
6 |
['alreadydone', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
6-45188 6 days ago |
6-45188 6 days ago |
70-18855 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-37523 6 days ago |
6-37524 6 days ago |
6-37588 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-26452 6 days ago |
7-40595 7 days ago |
14-36768 14 days |
| 22078 |
Louddy author:Louddy |
feat(SkewMonoidAlgebra): multiplication and algebraic instances |
# Multiplication and Algebraic Instances
In this PR, we introduce the definition of the skewed convolution product on `SkewMonoidAlgebra k G`. Here, the product of two elements `f g : SkewMonoidAlgebra k G` is the finitely supported function whose value at `a` is the sum of `f x * (x • g y)` over all pairs `x, y` such that `x * y = a`.
We also introduce the associated algebraic instances.
## Context
This is the third part of a planned series of PRs aiming to formalise skew monoid algebras.
The PRs are split to ease the review process. The moral sum of these planned PRs is #10541.
The first and second part were #15878 and #19084.
Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)>
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-algebra
label:t-algebra$ |
443/42 |
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean |
1 |
52 |
['AntoineChambert-Loir', 'Louddy', 'github-actions', 'kbuzzard'] |
nobody |
6-23446 6 days ago |
35-24183 1 month ago |
71-74295 71 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-14435 6 days ago |
6-14435 6 days ago |
6-27352 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 |
5-79898 5 days ago |
10-17452 10 days ago |
31-54898 31 days |
| 24669 |
qawbecrdtey author:qawbecrdtey |
feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` |
---
[](https://gitpod.io/from-referrer/)
This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it.
```lean
def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E
```
|
t-analysis |
20/1 |
Mathlib/Analysis/Normed/Operator/LinearIsometry.lean |
1 |
1 |
['github-actions'] |
nobody |
5-65319 5 days ago |
5-65335 5 days ago |
5-65389 5 days |
| 22279 |
xyzw12345 author:xyzw12345 |
feat(RingTheory/GradedAlgebra): homogeneous relation |
In this PR, we defined the concept of a homogeneous relation and proved some properties about homogeneous relations. The main result of this PR is showing that taking `RingQuot` by a homogeneous relation can give a graded structure on the quotient ring. This result can be used to define graded structures on rings obtained using `RingQuot`, e.g. the Symmetric Algebra defined in #21539 can be verified to have such a structure.
Co-authored-by:
Zhixuan Dai @atstarrysky <22300180006@m.fudan.edu.cn>
Yiming Fu @pelicanhere
Zhenyan Fu @pumpkin678
Raphael Douglas Giles @Raph-DG
Jiedong Jiang @jjdishere
- [x] depends on: #22354
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
455/0 |
Mathlib.lean,Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/DirectSum/Basic.lean,Mathlib/Algebra/DirectSum/Module.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/RingQuot.lean,Mathlib/RingTheory/GradedAlgebra/Basic.lean,Mathlib/RingTheory/GradedAlgebra/HomogeneousRelation.lean |
8 |
7 |
['Paul-Lez', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'ocfnash', 'xyzw12345'] |
ocfnash assignee:ocfnash |
5-55812 5 days ago |
41-60393 1 month ago |
43-5781 43 days |
| 22464 |
adomani author:adomani |
feat(CI): declarations diff in Lean |
Rewrites the `declaration_diff` script in Lean.
You can see the effect of the new script in the testing branch #22497.
The new CI step runs in approximately 5mins, but is separate from the `build` step.
---
[](https://gitpod.io/from-referrer/)
|
CI |
151/0 |
.github/workflows/PR_summary_lean.yml,scripts/README.md,scripts/declarations_diff.lean,scripts/declarations_diff_lean_shell_glue.sh |
4 |
6 |
['bryangingechen', 'github-actions', 'grunweg'] |
robertylewis assignee:robertylewis |
5-55636 5 days ago |
70-19881 2 months ago |
70-19871 70 days |
| 24172 |
LessnessRandomness author:LessnessRandomness |
feat: specialize rational root theorem to usual rational numbers and integers |
Rational root theorem and integral root theorem - the special case for usual rational numbers and integers.
--- |
new-contributor
t-algebra
label:t-algebra$ |
123/0 |
Mathlib.lean,Mathlib/RingTheory/Polynomial/OfRationalNumbers/RationalRootTheorem.lean |
2 |
2 |
['github-actions', 'grunweg'] |
mariainesdff assignee:mariainesdff |
5-55369 5 days ago |
25-23052 25 days ago |
25-23106 25 days |
| 23413 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Join): Pseudofunctoriality of joins of categories |
Promote the constructions `C ↦ C ⋆ D` and `D ↦ C ⋆ D` to pseudofunctors from `Cat` to `Cat`. The construction is carried in a new file `CategoryTheory/Join/Pseudofunctor.lean` to reduce imports.
---
- [x] depends on: #23412
The pseudofunctoriality statements here are not the most general. The "right" statements would be
1) "pseudobifunctoriality".
2) pseudofunctoriality with values in slice bicategories.
Unfortunately, the two-categorical machinery in mathlib is not advanced enough yet to even make sense of the statements (first would require at least product bicategories, or 2-categories of pseudofunctors for a curried version, second would require slice bicategories.).
The content of this file should be upgraded once said constructions in bicategories are available, but for now I want at least to have statements that recover what we already have for `WithInitial` and `WithTerminal` rather than conditioning everything on a (probably rather long) bicategorical sidequest.
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
169/0 |
Mathlib.lean,Mathlib/CategoryTheory/Join/Basic.lean,Mathlib/CategoryTheory/Join/Pseudofunctor.lean |
3 |
9 |
['github-actions', 'joelriou', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'robin-carlier'] |
nobody |
5-53807 5 days ago |
5-53807 5 days ago |
24-31280 24 days |
| 21522 |
riccardobrasca author:riccardobrasca |
feat: add Mathlib.RingTheory.DedekindDomain.Instances |
We add a new file `Mathlib.RingTheory.DedekindDomain.Instances` containing various instances that are useful to work with the localization a prime of an extension of Dedekind domains. As a practical example we golf a tedious proof in `Mathlib.RingTheory.Ideal/Norm.RelNorm`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
253/71 |
Mathlib.lean,Mathlib/RingTheory/DedekindDomain/Different.lean,Mathlib/RingTheory/DedekindDomain/Instances.lean,Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean,Mathlib/RingTheory/Ideal/Norm/RelNorm.lean,Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean,Mathlib/RingTheory/Localization/AtPrime.lean,Mathlib/RingTheory/Localization/Basic.lean,Mathlib/RingTheory/Localization/LocalizationLocalization.lean,Mathlib/RingTheory/RingHom/Finite.lean,Mathlib/RingTheory/Trace/Quotient.lean |
11 |
31 |
['YaelDillies', 'erdOne', 'github-actions', 'riccardobrasca'] |
nobody |
5-49483 5 days ago |
6-40564 6 days ago |
65-67748 65 days |
| 22933 |
chrisflav author:chrisflav |
feat(RingTheory/LocalProperties): constructor for `RingHom.OfLocalizationSpan` |
Adds a constructor for `RingHom.OfLocalizationSpan` where `P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))` has to be shown for a covering family. This is convenient in practice, because the base change API is the more generally applicable framework.
-- -
I think the import increase is fine, but if people are not happy with it, I can instead make a new file `Mathlib.RingTheory.LocalizationAway.BaseChange`.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
102/3 |
Mathlib/Algebra/Algebra/Basic.lean,Mathlib/RingTheory/LocalProperties/Basic.lean,Mathlib/RingTheory/Localization/BaseChange.lean |
3 |
8 |
['chrisflav', 'erdOne', 'github-actions'] |
nobody |
5-48984 5 days ago |
5-82725 5 days ago |
60-14944 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-35220 5 days ago |
25-43647 25 days ago |
73-36962 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-35186 5 days ago |
64-24937 2 months ago |
64-24988 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-35108 5 days ago |
26-7552 26 days ago |
36-56370 36 days |
| 23826 |
javra author:javra |
feat(CategoryTheory): linear categories as `ModuleCat R`-enriched categories |
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-category-theory
|
195/0 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean,Mathlib/CategoryTheory/Enriched/Linear.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/CategoryTheory/Monoidal/Linear.lean |
5 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
TwoFX assignee:TwoFX |
5-35092 5 days ago |
29-45526 29 days ago |
29-45509 29 days |
| 21103 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialSet): uniqueness of the decomposition involving non-degenerate simplices |
Any simplex `x : X _⦋n⦌` of a simplicial set can be written in a unique way as `X.map f.op y` for an epimorphism `f : ⦋n⦌ ⟶ ⦋m⦌` and a non-degenerate `m`-simplex `y`.
---
- [x] depends on: #21098
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
118/5 |
Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean |
2 |
4 |
['gio256', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
dagurtomas assignee:dagurtomas |
5-32478 5 days ago |
25-5983 25 days ago |
63-37586 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-32465 5 days ago |
22-17745 22 days ago |
22-19268 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-32277 5 days ago |
43-25450 1 month ago |
43-25502 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-31352 5 days ago |
15-27378 15 days ago |
15-28059 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-28814 5 days ago |
40-82918 1 month ago |
46-23160 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-28599 5 days ago |
20-18762 20 days ago |
21-28812 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-26165 5 days ago |
5-26165 5 days ago |
5-73255 5 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-18246 5 days ago |
5-18309 5 days ago |
5-18294 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-15098 5 days ago |
7-19153 7 days ago |
56-63044 56 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-7388 5 days ago |
49-26743 1 month ago |
83-11840 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-6894 5 days ago |
5-17675 5 days ago |
5-17724 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-566 5 days ago |
31-42415 1 month ago |
31-42468 31 days |
| 22100 |
smmercuri author:smmercuri |
feat: two inequivalent absolute values have a `< 1` and `> 1` value |
- Two absolute values `v` and `w` are equivalent if and only if `v x < 1` exactly when `w x < 1`
- Two inequivalent absolute values `v` and `w` have a point `x` at which `1 < v x` and `w x < 1`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-analysis
label:t-algebra$ |
174/0 |
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Analysis/AbsoluteValue/Equivalence.lean |
2 |
6 |
['Paul-Lez', 'github-actions', 'smmercuri'] |
faenuccio assignee:faenuccio |
4-84834 4 days ago |
26-3344 26 days ago |
56-77089 56 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 |
4-84751 4 days ago |
39-10988 1 month ago |
39-11040 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 |
4-84620 4 days ago |
32-79191 1 month ago |
32-79240 32 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 |
4-76968 4 days ago |
10-55148 10 days ago |
12-36702 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 |
4-63348 4 days ago |
5-24784 5 days ago |
5-24839 5 days |
| 22420 |
pechersky author:pechersky |
feat(Order/Prod/Lex/{Hom,Monoid,GroupWithZero}): ordered inclusions and projections of prod of ordered groups |
---
- [x] depends on: #22402
[](https://gitpod.io/from-referrer/)
|
t-order
t-algebra
label:t-algebra$ |
256/0 |
Mathlib.lean,Mathlib/Order/Prod/Lex/GroupWithZero.lean,Mathlib/Order/Prod/Lex/Hom.lean,Mathlib/Order/Prod/Lex/Monoid.lean |
4 |
15 |
['YaelDillies', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'pechersky'] |
YaelDillies assignee:YaelDillies |
4-55132 4 days ago |
36-20663 1 month ago |
36-22455 36 days |
| 24703 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal): external product of diagrams in monoidal categories |
Given functors `K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C` with values in a monoidal category, define a construction `externalProduct K₁ K₂` (denoted `K₁ ⊠ K₂`) as the bifunctor `(j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂`.
We show that composition of this construction with the diagonal functor to the product recovers the pointwise tensor product of functors, and we show that this construction satisfies a symmetry whenever `C` is braided.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
99/0 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/ExternalProduct.lean |
2 |
1 |
['github-actions'] |
nobody |
4-48362 4 days ago |
4-48960 4 days ago |
4-48945 4 days |
| 8167 |
sebzim4500 author:sebzim4500 |
feat: Add new `grw` tactic for rewriting using inequalities. |
Co-authored-by: @hrmacbeth, @digama0
---
- [x] depends on: #8796
```lean
example (x y z w : ℝ) (h₁ : x < z) (h₂ : w ≤ y + 4) (h₃ : Real.exp z < 5 * w) :
Real.exp x < 5 * (y + 4) := by
grw [h₁, ← h₂]
exact h₃
```
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
modifies-tactic-syntax
|
552/2 |
Mathlib.lean,Mathlib/Data/Int/ModEq.lean,Mathlib/Tactic.lean,Mathlib/Tactic/GCongr/Core.lean,Mathlib/Tactic/GRW.lean,Mathlib/Tactic/GRW/Core.lean,Mathlib/Tactic/GRW/Lemmas.lean,MathlibTest/GRW.lean,scripts/noshake.json |
9 |
53 |
['Vierkantor', 'digama0', 'eric-wieser', 'fpvandoorn', 'github-actions', 'hrmacbeth', 'kim-em', 'leanprover-community-mathlib4-bot', 'sebzim4500'] |
nobody |
4-39149 4 days ago |
66-13593 2 months ago |
96-62242 96 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-39079 4 days ago |
41-32733 1 month ago |
43-66134 43 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-38971 4 days ago |
79-70470 2 months ago |
79-70462 79 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-38945 4 days ago |
58-82728 1 month ago |
63-83264 63 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-37098 4 days ago |
29-38368 29 days ago |
29-38422 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-37011 4 days ago |
51-11685 1 month ago |
99-31373 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-34662 4 days ago |
4-34662 4 days ago |
34-63454 34 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-32018 4 days ago |
42-13471 1 month ago |
80-66418 80 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-31139 4 days ago |
4-33121 4 days ago |
4-33171 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-30367 4 days ago |
4-30367 4 days ago |
4-30423 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-29896 4 days ago |
48-82340 1 month ago |
48-82385 48 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-27343 4 days ago |
4-38331 4 days ago |
4-38443 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-21409 4 days ago |
6-54011 6 days ago |
6-54062 6 days |
| 24679 |
YaelDillies author:YaelDillies |
refactor: move the construction of `ChosenFiniteProducts` from finite products with `ChosenFiniteProducts` |
Now that `ChosenFiniteProducts` extends `MonoidalCategory`, there is no point having the `MonoidalCategory` version separate from the `ChosenFiniteProducts` one.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-category-theory
|
125/296 |
Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean,Mathlib/CategoryTheory/ChosenFiniteProducts.lean,Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean,Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean |
4 |
2 |
['erdOne', 'github-actions'] |
nobody |
4-20765 4 days ago |
5-30341 5 days ago |
5-30341 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-18659 4 days ago |
4-42403 4 days ago |
18-48239 18 days |
| 24213 |
BoltonBailey author:BoltonBailey |
feat: add simp lemmas for trig functions on `π * 2⁻¹` |
This PR adds a number of simp lemmas to reduce trig functions evaluated on `π * 2⁻¹`. This allows `simp` to reduce expressions such as `sin (π * (1 / 2))`
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
45/0 |
Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean |
1 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
4-18114 4 days ago |
4-18136 4 days ago |
22-75528 22 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-12593 4 days ago |
5-16996 5 days ago |
5-16981 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-5133 4 days ago |
5-30297 5 days ago |
58-5750 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-3553 4 days ago |
36-26236 1 month ago |
38-75339 38 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 |
3-58050 3 days ago |
3-60826 3 days ago |
8-14833 8 days |
| 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 |
3-48693 3 days ago |
3-48699 3 days ago |
8-76111 8 days |
| 24463 |
mans0954 author:mans0954 |
feature(Analysis/SpecialFunctions/Complex/CircleAddChar): ZMod.toCircle_eq_Circle_exp |
Show that `ZMod.toCircle k` equals `Circle.exp (2 * π * (k.val / N))`.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
7/0 |
Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean |
1 |
6 |
['Ruben-VandeVelde', 'github-actions', 'mans0954'] |
nobody |
3-48657 3 days ago |
13-66921 13 days ago |
13-66979 13 days |
| 24337 |
mans0954 author:mans0954 |
feature(Analysis/InnerProductSpace/Basic): Add norm_add_eq_iff_real |
Adds `norm_add_eq_iff_real` - a sufficient and necessary condition for equality in the triangle inequality.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
6/0 |
Mathlib/Analysis/InnerProductSpace/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
3-48487 3 days ago |
19-49483 19 days ago |
19-49543 19 days |
| 23161 |
mans0954 author:mans0954 |
feature(Data/Finset/RangeDistance): abs_sub_lt_of_mem_finset_range |
The distance between two elements of `Finset.range N` (i.e. absolute value of the difference as integers) is less than `N`.
A lemma I found useful for something I was working on, so sharing here in case it's of wider interest.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
30/0 |
Mathlib.lean,Mathlib/Algebra/Order/Group/Unbundled/Abs.lean,Mathlib/Data/Finset/RangeDistance.lean |
3 |
3 |
['fbarroero', 'github-actions'] |
nobody |
3-48428 3 days ago |
54-11622 1 month ago |
54-11613 54 days |
| 24167 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(Data/Fin/Tuple/Embedding): create embeddings of Fin Nat to types |
Define
* `Fin.Embedding.cons`, `Fin.Embedding.tail`
* `Fin.Embedding.snoc`, `Fin.Embedding.init`
* `Fin.Embedding.append`
analogously to `Fin.cons`, `Fin.snoc`, `Fin.append`.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
160/0 |
Mathlib.lean,Mathlib/Data/Fin/Tuple/Basic.lean,Mathlib/Data/Fin/Tuple/Embedding.lean |
3 |
1 |
['github-actions'] |
riccardobrasca assignee:riccardobrasca |
3-47557 3 days ago |
25-43101 25 days ago |
25-43155 25 days |
| 24735 |
joelriou author:joelriou |
chore(CategoryTheory/Monoidal): define tensorLeft/Right as abbrev for curriedTensor |
In the study of commutation of tensor products with colimits, we may not be completely sure about phrasing the assumptions (as instances) in terms of `tensorLeft X` (resp. `tensorRight Y`) or in terms of `(curriedTensor C).obj X` (resp. `(curriedTensor C).flip.obj Y`), even though they are defeq, and we could have to introduce lemmas/instances to deduce properties of `tensorLeft X` from that of `(curriedTensor C).obj` and vice versa. By making `tensorLeft` and `tensorRight` abbreviations, this PR makes such issues disappear.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
20/21 |
Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean,Mathlib/CategoryTheory/Closed/Functor.lean,Mathlib/CategoryTheory/Closed/Monoidal.lean,Mathlib/CategoryTheory/Monoidal/Bimod.lean,Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean,Mathlib/CategoryTheory/Monoidal/Category.lean |
6 |
6 |
['fivemeyestore', 'fivemhostingserver', 'fivemserverhostings', 'fivemtebex', 'github-actions', 'scriptforfivem'] |
nobody |
3-45791 3 days ago |
3-49299 3 days ago |
3-49284 3 days |
| 24530 |
chrisflav author:chrisflav |
feat(RingTheory): faithfully flat ring maps |
Co-authored by: Joël Riou
---
- [ ] depends on: #24375
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
159/15 |
Mathlib.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean,Mathlib/RingTheory/LocalProperties/Basic.lean,Mathlib/RingTheory/RingHom/FaithfullyFlat.lean,Mathlib/RingTheory/RingHom/Finite.lean,Mathlib/RingTheory/RingHom/Flat.lean,Mathlib/RingTheory/RingHom/Integral.lean,Mathlib/RingTheory/RingHom/Locally.lean,Mathlib/RingTheory/RingHom/Surjective.lean,Mathlib/RingTheory/RingHom/Unramified.lean,Mathlib/RingTheory/RingHomProperties.lean |
12 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
3-45097 3 days ago |
3-45098 3 days ago |
3-46165 3 days |
| 24711 |
robin-carlier author:robin-carlier |
feat(CategoryTheory/Monoidal/Limits): miscellany about preservation of (co)limits by tensor products |
Register some instances regarding preservations of (co)limits for the tensor product of a monoidal category. More precisely, we register the fact that if the category is braided and `tensorLeft c` preserves colimits (this can be inferred e.g via `MonoidalClosed C`), then so does `tensorRight c` for every `c`.
We also rephrase preservation of (co)limits for `curriedTensor C` in terms of preservations of (co)limits for `tensorRight c`.
The PR introduces also introduces a directory `CategoryTheory.Monoidal.Limits` and moves the existing file `CategoryTheory.Monoidal.Limits.lean` to `CategoryTheory.Monoidal.Limits.Basic`.
---
The instances registered here are tailored so that for a braided monoidal closed category, `PreservesColimit₂` instances from #24685 can be inferred with the results of #24686 for the external product of diagrams defined in #24703
[](https://gitpod.io/from-referrer/)
|
file-removed
t-category-theory
|
72/2 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean,Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean,Mathlib/CategoryTheory/Monoidal/Limits/Preserves.lean |
4 |
8 |
['github-actions', 'joelriou', 'robin-carlier'] |
nobody |
3-43580 3 days ago |
3-43580 3 days ago |
4-26871 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-43277 3 days ago |
3-43277 3 days ago |
52-79423 52 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-27718 3 days ago |
6-6241 6 days ago |
6-7270 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-26192 3 days ago |
3-26193 3 days ago |
36-17291 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-17954 3 days ago |
39-5003 1 month ago |
39-5051 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-16520 3 days ago |
3-16537 3 days ago |
4-74019 4 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-13799 3 days ago |
3-19772 3 days ago |
18-3812 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 |
2-86248 2 days ago |
3-7294 3 days ago |
3-7344 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 |
2-79588 2 days ago |
12-46156 12 days ago |
12-46140 12 days |
| 24351 |
eric-wieser author:eric-wieser |
feat: fderiv lemmas for `pow` |
This generalizes the lemmas about `fderiv fun x => f x ^ n` to work over arbitrary normed modules and algebras.
Following the convention set by the lemmas about `fderiv` and `*`, we use `'`d names for the non-commutative variants.
Moves:
- `deriv_pow''` -> `deriv_pow`
- `deriv_pow` -> `deriv_pow_field`
- `derivWithin_pow'` -> `derivWithin_pow_field'`
Deletions:
- `deriv_pow'`
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
282/82 |
Mathlib.lean,Mathlib/Analysis/Calculus/Deriv/Polynomial.lean,Mathlib/Analysis/Calculus/Deriv/Pow.lean,Mathlib/Analysis/Calculus/FDeriv/Mul.lean,Mathlib/Analysis/Calculus/FDeriv/Pow.lean,Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Complex/Angle.lean,Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean,Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean |
9 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
2-77400 2 days ago |
2-77400 2 days ago |
3-24448 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 |
2-74929 2 days ago |
12-47519 12 days ago |
17-23681 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 |
2-72883 2 days ago |
2-73852 2 days ago |
20-44713 20 days |
| 24734 |
mbkybky author:mbkybky |
feat(Algebra/Homology/DerivedCategory): `Ext` commutes with finite coproducts |
Prove that `Ext` commutes with finite coproducts and products.
Co-authored-by: Nailin Guan @Thmoas-Guan
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-category-theory
label:t-algebra$ |
83/5 |
Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean,Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean,Mathlib/CategoryTheory/Preadditive/Biproducts.lean |
3 |
6 |
['github-actions', 'joelriou', 'mbkybky'] |
nobody |
2-65622 2 days ago |
2-65622 2 days ago |
2-71333 2 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 |
2-65072 2 days ago |
2-65466 2 days ago |
7-6393 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 |
2-57538 2 days ago |
2-57584 2 days ago |
2-57585 2 days |
| 24450 |
justus-springer author:justus-springer |
feat(Algebra/Order/Nonneg): A finite module is finite over the nonnegative scalars |
From Toric
---
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
new-contributor
t-algebra
label:t-algebra$ |
21/3 |
Mathlib/Algebra/Order/Nonneg/Module.lean |
1 |
3 |
['YaelDillies', 'github-actions'] |
nobody |
2-54556 2 days ago |
2-54556 2 days ago |
14-31120 14 days |
| 23940 |
YaelDillies author:YaelDillies |
feat: polytopes |
From Toric
Co-authored-by: Matthew Johnson
---
[](https://gitpod.io/from-referrer/)
|
toric
t-analysis
|
74/0 |
Mathlib.lean,Mathlib/Geometry/Convex/Polytope.lean,Mathlib/Geometry/Convex/README.md |
3 |
6 |
['Parcly-Taxel', 'YaelDillies', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
2-46607 2 days ago |
2-51585 2 days ago |
32-55180 32 days |
| 24205 |
meithecatte author:meithecatte |
chore(RegularExpressions): clarify that TODO has pending PRs |
The TODO on equivalence between regular expressions and DFAs seems to be particularly appealing to new contributors, having spawned multiple competing PRs working towards that goal.
It is also one where a new contributor is quite likely to produce a design that is not inline with mathlib's API design philosophy and will require a lot of guidance, which causes the PRs to languish in review.
Reword the TODO to make it less likely that the situation gets worse.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-computability
new-contributor
easy
|
2/1 |
Mathlib/Computability/RegularExpressions.lean |
1 |
7 |
['YaelDillies', 'github-actions', 'meithecatte', 'urkud'] |
nobody |
2-46435 2 days ago |
2-46435 2 days ago |
24-13839 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-41695 2 days ago |
2-41695 2 days ago |
3-2127 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-38508 2 days ago |
2-38572 2 days ago |
2-38557 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-36554 2 days ago |
2-36603 2 days ago |
2-36588 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-34008 2 days ago |
7-9678 7 days ago |
11-84650 11 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-31130 2 days ago |
6-30719 6 days ago |
12-65139 12 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-29053 2 days ago |
2-29073 2 days ago |
2-42260 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-23429 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-20864 2 days ago |
2-21116 2 days ago |
2-23058 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-16342 2 days ago |
2-16343 2 days ago |
5-26123 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-13600 2 days ago |
2-13662 2 days ago |
2-13647 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-10272 2 days ago |
2-16223 2 days ago |
49-68445 49 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-9638 2 days ago |
2-9686 2 days ago |
12-84495 12 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-7050 2 days ago |
2-7265 2 days ago |
2-9309 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-5626 2 days ago |
39-30815 1 month ago |
42-14203 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 |
1-84189 1 day ago |
2-29354 2 days ago |
17-14790 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 |
1-81071 1 day ago |
1-82003 1 day ago |
67-81989 67 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 |
1-75542 1 day ago |
1-75542 1 day ago |
1-75599 1 day |
| 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 |
1-66665 1 day ago |
1-66665 1 day ago |
25-4385 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 |
1-65438 1 day ago |
1-83563 1 day ago |
11-66038 11 days |
| 22915 |
pimotte author:pimotte |
feat(Combinatorics/SimpleGraph): Tutte's theorem |
Proves Tutte's theorem.
---
- [x] depends on: #22242
- [x] depends on: #22119
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
260/30 |
Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Operations.lean,Mathlib/Combinatorics/SimpleGraph/Tutte.lean,docs/1000.yaml |
5 |
45 |
['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'pimotte'] |
nobody |
1-58664 1 day ago |
1-58664 1 day ago |
8-20354 8 days |
| 23935 |
Thmoas-Guan author:Thmoas-Guan |
feat(RingTheory/IsSMulRegular): categorical constructions for IsSMulRegular |
The categorical constructions for `IsSMulRegular` for later use related to `Ext` in a separate file.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-category-theory
label:t-algebra$ |
62/0 |
Mathlib.lean,Mathlib/Algebra/Homology/ExactSequence.lean,Mathlib/RingTheory/Regular/Category.lean |
3 |
28 |
['Thmoas-Guan', 'erdOne', 'github-actions', 'joelriou', 'riccardobrasca'] |
joelriou assignee:joelriou |
1-53989 1 day ago |
20-19902 20 days ago |
28-79398 28 days |
| 23718 |
syur2 author:syur2 |
feat(Algebra): hom localize equiv localize hom |
Add the linear equiv of `S^{-1}(M =>[R] N)` equiv `(S^{-1} M) =>[S^{-1}R] (S^{-1} N)` for finitely presented module `M`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
50/0 |
Mathlib/Algebra/Module/FinitePresentation.lean |
1 |
4 |
['Thmoas-Guan', 'acmepjz', 'github-actions'] |
nobody |
1-53950 1 day ago |
37-55829 1 month ago |
37-55824 37 days |
| 21966 |
vasnesterov author:vasnesterov |
feat(Tactic/Order): support `⊤`, `⊥`, and lattice operations |
Support `⊤`, `⊥`, and lattice operations in the `order` tactic.
---
- [x] depends on: #21877
[](https://gitpod.io/from-referrer/)
|
large-import
t-meta
|
248/68 |
Mathlib/Tactic/Order.lean,Mathlib/Tactic/Order/CollectFacts.lean,Mathlib/Tactic/Order/Graph/Basic.lean,Mathlib/Tactic/Order/Preprocessing.lean,MathlibTest/order.lean,scripts/noshake.json |
6 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
1-53040 1 day ago |
40-47461 1 month ago |
74-43956 74 days |
| 17914 |
xroblot author:xroblot |
feat(NumberTheory/NumberField): proof of the Analytic Class Number Formula |
Let `K` be a number field. Define
```lean
def dedekindZeta (s : ℂ) :=
LSeries (fun n ↦ Nat.card {I : Ideal (𝓞 K) // absNorm I = n}) s
```
and
```lean
def residue : ℝ :=
(2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * classNumber K) /
(torsionOrder K * Real.sqrt |discr K|)
```
We prove:
```lean
theorem dedekindZeta_residue :
Tendsto (fun s : ℝ ↦ (s - 1) * dedekindZeta K s) (𝓝[>] 1) (𝓝 (residue K))
```
---
- [x] depends on: #16675
- [x] depends on: #16822
- [x] depends on: #12488
- [x] depends on: #12405
- [x] depends on: #17943
- [x] depends on: #17944
- [x] depends on: #18130
- [x] depends on: #18166
- [x] depends on: #18231
- [x] depends on: #18246
- [x] depends on: #18245
- [x] depends on: #18248
- [x] depends on: #18400
- [x] depends on: #20660
- [x] depends on: #22115
- [x] depends on: #22397
- [x] depends on: #22779
- [x] depends on: #22866
- [x] depends on: #23440
- [x] depends on: #24713
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
81/0 |
Mathlib.lean,Mathlib/NumberTheory/NumberField/ClassNumber.lean,Mathlib/NumberTheory/NumberField/DedekindZeta.lean |
3 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'riccardobrasca', 'xroblot'] |
riccardobrasca assignee:riccardobrasca |
1-39192 1 day ago |
1-51533 1 day ago |
1-64842 1 day |
| 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-33166 1 day ago |
1-38800 1 day ago |
58-53822 58 days |
| 24706 |
riccardobrasca author:riccardobrasca |
feat: add RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_le_pow_inertiaDeg_of_mem_primesOver_of_mem_Icc |
We improve the statement of `RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_mem_primesOver_of_le` to `RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_le_pow_inertiaDeg_of_mem_primesOver_of_mem_Icc`: it is enough to only test primes `p` and ideals `P` such that `p ^ ((span {p}).inertiaDeg P` is less than Minkowski's bound.
We also improve the structure of the file.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
t-number-theory
label:t-algebra$ |
84/50 |
Mathlib/NumberTheory/NumberField/ClassNumber.lean,Mathlib/NumberTheory/RamificationInertia/Basic.lean |
2 |
1 |
['github-actions'] |
nobody |
1-31971 1 day ago |
1-32970 1 day ago |
3-17045 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-30783 1 day ago |
1-34318 1 day ago |
5-52999 5 days |
| 23673 |
erdOne author:erdOne |
feat(AlgebraicGeometry): delaborator for coercing schemes to types |
Co-authored-by: Christian Merten
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
t-meta
|
46/0 |
Mathlib/AlgebraicGeometry/Scheme.lean,MathlibTest/Delab/Scheme.lean |
2 |
2 |
['github-actions', 'jcommelin'] |
jcommelin assignee:jcommelin |
1-27091 1 day ago |
21-32334 21 days ago |
39-23327 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-25462 1 day ago |
1-54023 1 day ago |
1-57120 1 day |
| 24654 |
grunweg author:grunweg |
feat(lint-style): enforce modules are named in UpperCamelCase |
except for a handful of explicit exceptions
In passing, refactor the other two checks in `lint-style` to return the number of their errors (which is both meaningful and semantically clear), as opposed to a boolean (which can be accidentally inverted).
---
- [x] depends on: #23974 (right now, the linter complains about the two violations fixed in that PR)
[](https://gitpod.io/from-referrer/)
|
t-linter |
58/14 |
scripts/lint-style.lean |
1 |
17 |
['adomani', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] |
nobody |
1-25432 1 day ago |
1-31806 1 day ago |
1-36934 1 day |
| 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 |
1-22957 1 day ago |
1-27511 1 day ago |
1-27496 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-15921 1 day ago |
3-23195 3 days ago |
68-18871 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-15157 1 day ago |
1-15186 1 day ago |
15-19336 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-14970 1 day ago |
1-14970 1 day ago |
1-15023 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-12359 1 day ago |
1-12374 1 day ago |
19-76564 19 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-9018 1 day ago |
1-24327 1 day ago |
1-25910 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-8912 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-8402 1 day ago |
206-30635 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-7643 1 day ago |
1-14276 1 day ago |
5-12141 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-5040 1 day ago |
54-39496 1 month ago |
55-23952 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-4577 1 day ago |
82-37402 2 months ago |
85-165 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-4527 1 day ago |
47-44754 1 month ago |
64-70910 64 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-4377 1 day ago |
1-4377 1 day ago |
1-43278 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-4376 1 day ago |
19-74707 19 days ago |
19-74761 19 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-4338 1 day ago |
18-14270 18 days ago |
18-14322 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-4320 1 day ago |
17-11747 17 days ago |
17-11810 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-4017 1 day ago |
14-25610 14 days ago |
15-36441 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-3621 1 day ago |
1-3639 1 day ago |
1-3789 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-3336 1 day ago |
5-3909 5 days ago |
5-49267 5 days |
| 24796 |
erdOne author:erdOne |
feat(AlgebraicGeometry): locally directed gluing |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
433/133 |
Mathlib/AlgebraicGeometry/Gluing.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean,Mathlib/AlgebraicGeometry/Restrict.lean,Mathlib/AlgebraicGeometry/Scheme.lean |
6 |
1 |
['github-actions'] |
nobody |
1-1889 1 day ago |
1-72556 1 day ago |
1-72589 1 day |
| 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-1258 1 day ago |
41-19541 1 month ago |
48-2678 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 |
0-84403 23 hours ago |
21-42360 21 days ago |
21-43186 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 |
0-63491 17 hours ago |
0-63491 17 hours ago |
64-14880 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 |
0-62609 17 hours ago |
0-62609 17 hours ago |
0-68744 19 hours |
| 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 |
0-61678 17 hours ago |
1-37212 1 day ago |
1-37262 1 day |
| 24829 |
urkud author:urkud |
fix(Topology/Homotopy): fix name&args order of `comp` |
`ContinuousMap.Homotopy.hcomp` used name & arguments order
that matches Mathlib's category theory conventions,
not topology conventions.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
30/19 |
Mathlib/Topology/Homotopy/Basic.lean,Mathlib/Topology/Homotopy/Contractible.lean,Mathlib/Topology/Homotopy/Equiv.lean,Mathlib/Topology/Homotopy/Lifting.lean |
4 |
5 |
['github-actions', 'grunweg', 'urkud'] |
nobody |
0-56780 15 hours ago |
0-65420 18 hours ago |
0-65475 18 hours |
| 24644 |
matthewjasper author:matthewjasper |
chore(RingTheory/DedekindDomain/AdicValuation): Use intValuation over intValuationDef |
`intValuationDef` exists so that we can prove its basic properties before defining `intValuation`, but it shouldn't be used afterwards. Change theorems which use `intValuation` in their names to actually use `intValution` and update usages.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
t-topology
label:t-algebra$ |
108/77 |
Mathlib/NumberTheory/NumberField/FinitePlaces.lean,Mathlib/RingTheory/DedekindDomain/AdicValuation.lean,Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean,Mathlib/RingTheory/LaurentSeries.lean |
4 |
4 |
['github-actions', 'kbuzzard', 'matthewjasper'] |
nobody |
0-56321 15 hours ago |
0-56321 15 hours ago |
4-61154 4 days |
| 22881 |
Champitoad author:Champitoad |
feat(CategoryTheory/Topos): add representability results for subobject classifier |
We add a section `Representability` at the end of `Mathlib.CategoryTheory.Topos.Classifier` where we formalize the necessary lemmas and definitions that lead to the proof of `CategoryTheory.isRepresentable_hasClassifier_iff`, which states that a category `C` has a subobject classifier if and only if the subobjects presheaf `CategoryTheory.Subobject.presheaf C` is representable (Proposition 1 in Section I.3 of Sheaves in Geometry and Logic [MM92]). The toughest part is found in definition `CategoryTheory.Classifier.fromRepresentation`, which formalizes as closely as possible the argument given in [MM92, pp. 33-34].
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-category-theory
|
251/22 |
Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/Presheaf.lean,Mathlib/CategoryTheory/Topos/Classifier.lean |
3 |
21 |
['Champitoad', 'github-actions', 'joelriou'] |
joelriou assignee:joelriou |
0-55759 15 hours ago |
41-26655 1 month ago |
55-46657 55 days |
| 23349 |
BGuillemet author:BGuillemet |
feat: add LocallyLipschitzOn.lipschitzOnWith_of_isCompact and two small lemmas about Lipschitz functions |
Main feat (in Mathlib/Topology/EMetricSpace/Basic.lean): if a function `f` from an extended pseudometric space to a pseudometric space is locally Lipschitz on a compact subset `s`, then `f` is Lipschitz on `s`. The theorem is true only when the codomain of `f` is a pseudometric space, so it needs imports from Mathlib/Topology/MetricSpace.
Other small feat (in Mathlib/Analysis/Calculus/ContDiff/RCLike.lean): a function that is continuously differentiable on an open subset is locally Lipschitz on this subset.
---
- [ ] depends on: #22890
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-topology
|
59/4 |
Mathlib/Analysis/Calculus/ContDiff/RCLike.lean,Mathlib/Topology/EMetricSpace/Lipschitz.lean |
2 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
PatrickMassot assignee:PatrickMassot |
0-55721 15 hours ago |
21-41853 21 days ago |
21-48612 21 days |
| 23367 |
b-reinke author:b-reinke |
feat(GroupTheory/FreeGroup/Reduce): add lemmas for toWord and reduce |
Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project.
This PR adds some simple helper lemmas for the interaction of `toWord` and `reduce` and basic list / group operations.
The RHS of the lemmas often contains more appearances of `reduce`, so they are not marked as `simp` lemmas.
---
[](https://gitpod.io/from-referrer/)
|
t-geometric-group-theory
t-algebra
label:t-algebra$ |
23/0 |
Mathlib/GroupTheory/FreeGroup/Reduce.lean |
1 |
9 |
['github-actions', 'grunweg', 'vlad902'] |
tb65536 assignee:tb65536 |
0-55489 15 hours ago |
47-34679 1 month ago |
47-43355 47 days |
| 24015 |
alreadydone author:alreadydone |
feat(RingTheory): lemmas on finiteness of `LinearMap` and `Module.End` |
---
One less lemma than #24012, but with the advantage of not depending on #23963.
- [x] depends on: #24115
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
91/32 |
Mathlib/Algebra/Module/LinearMap/End.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean,Mathlib/LinearAlgebra/BilinearMap.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/Projection.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/SimpleModule/Basic.lean |
7 |
9 |
['alreadydone', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-dependent-issues-bot'] |
erdOne assignee:erdOne |
0-55421 15 hours ago |
26-36801 26 days ago |
29-43922 29 days |
| 24121 |
smorel394 author:smorel394 |
feat(RingTheory/Coalgebra/Equiv, RingTheory/Bialgebra/Equiv): constructors for coalgebra and bialgebra equivalences |
Add constructors for equivalences of coalgebras and bialgebras, similar to what already exists for equivalences of algebras:
- `CoalgEquiv.ofCoalgHom` constructs a `CoalgEquiv` from a `CoalgHom` that has an inverse;
- `CoalgEquiv.ofBijective` constructs a `CoalgEquiv` from a bijective `CoalgHom`;
- `BialgEquiv.ofBialgHom` constructs a `BialgEquiv` from a `CoalgHom` that has an inverse;
- `BialgEquiv.ofBijective` constructs a `BialgEquiv` from a bijective `BialgHom`.
Also add some `apply` and `coe` lemmas, following the same model as for `AlgEquiv`s.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
72/0 |
Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Coalgebra/Equiv.lean |
2 |
1 |
['github-actions'] |
riccardobrasca assignee:riccardobrasca |
0-53411 14 hours ago |
27-17836 27 days ago |
27-17904 27 days |
| 24835 |
RemyDegenne author:RemyDegenne |
feat(Probability): lemmas about variance |
- `Var[fun ω ↦ X ω + c; μ] = Var[X; μ]`. Same for `c + X`, `-X`, `X - c` and `c - X`.
- The variance of a Dirac measure is 0
- `Var[X; μ.map Y] = Var[X ∘ Y; μ]`
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
54/0 |
Mathlib/Probability/Variance.lean |
1 |
1 |
['github-actions'] |
nobody |
0-52761 14 hours ago |
0-53054 14 hours ago |
0-53039 14 hours |
| 24775 |
JovanGerb author:JovanGerb |
chore(Order): use new `ge`/`gt` naming convention - Part 1 |
This is the first PR in a sequence of PRs to apply the new naming convention for order lemmas.
This PR changes all lemmas that have multiple occurences of `lt` or `le` in their name, and where `<` and `≤` have their arguments swapped in some places. Then those occurrences of `<` and `≤` are referred to as `gt` and `ge`.
The first commit is an automatic replacement of lemma names. The second commit adds deprecations for the renamed lemmas. Later commits are manual fixes. This should make it easy to review.
---
The naming convention is described at https://github.com/leanprover-community/leanprover-community.github.io/pull/626
[](https://gitpod.io/from-referrer/)
|
t-order |
969/944 |
Archive/Imo/Imo1959Q2.lean,Archive/Imo/Imo1960Q2.lean,Archive/Imo/Imo1986Q5.lean,Archive/Imo/Imo1988Q6.lean,Archive/Imo/Imo2015Q6.lean,Archive/Imo/Imo2024Q6.lean,Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean,Archive/Wiedijk100Theorems/CubingACube.lean,Archive/Wiedijk100Theorems/FriendshipGraphs.lean,Counterexamples/AharoniKorman.lean,Counterexamples/SeminormLatticeNotDistrib.lean,Mathlib/Algebra/BigOperators/Group/List/Basic.lean,Mathlib/Algebra/BigOperators/Intervals.lean,Mathlib/Algebra/BigOperators/Ring/Finset.lean,Mathlib/Algebra/CharP/Basic.lean,Mathlib/Algebra/CubicDiscriminant.lean,Mathlib/Algebra/GCDMonoid/Nat.lean,Mathlib/Algebra/GeomSum.lean,Mathlib/Algebra/Group/Subgroup/Finite.lean,Mathlib/Algebra/Group/Subgroup/Ker.lean,Mathlib/Algebra/Group/UniqueProds/Basic.lean,Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean,Mathlib/Algebra/Lie/Nilpotent.lean,Mathlib/Algebra/LinearRecurrence.lean,Mathlib/Algebra/Module/PID.lean,Mathlib/Algebra/Module/Submodule/Map.lean,Mathlib/Algebra/Order/AddTorsor.lean,Mathlib/Algebra/Order/Archimedean/Basic.lean,Mathlib/Algebra/Order/Archimedean/IndicatorCard.lean,Mathlib/Algebra/Order/BigOperators/Group/List.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/CompleteField.lean,Mathlib/Algebra/Order/Field/Basic.lean,Mathlib/Algebra/Order/Floor/Div.lean,Mathlib/Algebra/Order/Floor/Semiring.lean,Mathlib/Algebra/Order/Group/Abs.lean,Mathlib/Algebra/Order/Group/Unbundled/Basic.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean,Mathlib/Algebra/Order/Interval/Set/Group.lean,Mathlib/Algebra/Order/Ring/Basic.lean,Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean,Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean,Mathlib/Algebra/Order/Round.lean,Mathlib/Algebra/Order/ToIntervalMod.lean,Mathlib/Algebra/Polynomial/CoeffList.lean,Mathlib/Algebra/Polynomial/Degree/Domain.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Algebra/Polynomial/Div.lean,Mathlib/Algebra/Polynomial/HasseDeriv.lean,Mathlib/Algebra/Ring/Divisibility/Lemmas.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/Analysis/Analytic/Basic.lean,Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Asymptotics/ExpGrowth.lean,Mathlib/Analysis/BoxIntegral/Partition/Filter.lean,Mathlib/Analysis/BoxIntegral/Partition/Split.lean,Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean,Mathlib/Analysis/Calculus/Darboux.lean,Mathlib/Analysis/Calculus/Deriv/ZPow.lean,Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean,Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean,Mathlib/Analysis/Complex/AbelLimit.lean,Mathlib/Analysis/Complex/PhragmenLindelof.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean,Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Analysis/Convex/Cone/InnerDual.lean,Mathlib/Analysis/Convex/Exposed.lean,Mathlib/Analysis/Convex/Function.lean,Mathlib/Analysis/Convex/Gauge.lean,Mathlib/Analysis/Convex/Integral.lean,Mathlib/Analysis/Convex/Radon.lean,Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean,Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean,Mathlib/Analysis/Convex/StrictConvexSpace.lean,Mathlib/Analysis/Convex/Uniform.lean,Mathlib/Analysis/Convolution.lean,Mathlib/Analysis/Fourier/FourierTransformDeriv.lean,Mathlib/Analysis/MellinTransform.lean,Mathlib/Analysis/Meromorphic/Order.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Field/Ultra.lean,Mathlib/Analysis/Normed/Group/AddCircle.lean,Mathlib/Analysis/Normed/Module/Ray.lean,Mathlib/Analysis/NormedSpace/Connected.lean,Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean,Mathlib/Analysis/NormedSpace/Pointwise.lean,Mathlib/Analysis/ODE/Gronwall.lean,Mathlib/Analysis/PSeries.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart/Isometric.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean |
439 |
1 |
['github-actions'] |
bryangingechen assignee:bryangingechen |
0-52507 14 hours ago |
0-52507 14 hours ago |
2-36697 2 days |
| 24836 |
RemyDegenne author:RemyDegenne |
feat(MeasureTheory): characteristic function in a Banach space |
Define `charFunCLM μ L`, the characteristic function of a measure `μ` at `L : E →L[ℝ] ℝ` in a normed space `E`. This is the integral `∫ v, exp (L v * I) ∂μ`.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
112/6 |
Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean,Mathlib/MeasureTheory/Measure/CharacteristicFunction.lean,Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean |
3 |
1 |
['github-actions'] |
nobody |
0-50241 13 hours ago |
0-50504 14 hours ago |
0-50489 14 hours |
| 24719 |
madvorak author:madvorak |
feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv` |
---
Discussion:
https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2324719.20cannot.20find.20home/with/517142655
|
t-algebra label:t-algebra$ |
10/0 |
Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean |
1 |
8 |
['eric-wieser', 'github-actions', 'madvorak'] |
nobody |
0-49985 13 hours ago |
2-33875 2 days ago |
3-70105 3 days |
| 24304 |
YaelDillies author:YaelDillies |
feat: continuous perfect pairings |
Andrew and I do not know what a continuous perfect pairing should be. It's certainly at least a map `M →ₗ[R] N →ₗ[R] R`, but we probably want it to be continuous in both arguments simultaneously, ie as a map `M × N → R`, otherwise it wouldn't induce a map `N → M →L[R] R`. We probably also want the fact that a continuous perfect pairing between `M` and `N` implies that `M` is the dual of `N` and vice-versa. That means we would need the two maps `M → N →[L] R` and `N → M →L[R] R` to be homeorphisms. We are currently only assuming that they are bijective, which is enough to show that the double dual of a proper cone is itself.
From Toric
Co-authored-by: Andrew Yang
---
[](https://gitpod.io/from-referrer/)
|
toric
t-topology
|
92/0 |
Mathlib.lean,Mathlib/Topology/Algebra/Module/PerfectPairing.lean |
2 |
4 |
['ADedecker', 'YaelDillies', 'erdOne', 'github-actions'] |
ADedecker assignee:ADedecker |
0-48778 13 hours ago |
20-51531 20 days ago |
20-51585 20 days |
| 24105 |
urkud author:urkud |
feat(Topology/UniformSpace/Path): new file |
---
- [ ] depends on: #24066
[](https://gitpod.io/from-referrer/)
|
t-topology |
112/5 |
Mathlib.lean,Mathlib/Topology/ContinuousMap/Defs.lean,Mathlib/Topology/Order/ProjIcc.lean,Mathlib/Topology/Path.lean,Mathlib/Topology/UniformSpace/CompactConvergence.lean,Mathlib/Topology/UniformSpace/Path.lean |
6 |
4 |
['ADedecker', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
0-47343 13 hours ago |
7-3446 7 days ago |
7-4356 7 days |
| 24838 |
RemyDegenne author:RemyDegenne |
feat(MeasureTheory): tightness of the range of a sequence |
* `isTightMeasureSet_range_iff_tendsto_limsup_measure_norm_gt`: in a proper normed group,
the range of a sequence of measures `μ : ℕ → Measure E` is tight if and only if the function
`r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖x‖}) atTop` tends to `0` at infinity.
* `isTightMeasureSet_range_iff_tendsto_limsup_inner`: in a finite-dimensional inner product space,
the range of a sequence of measures `μ : ℕ → Measure E` is tight if and only if the function
`r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖⟪y, x⟫_𝕜‖}) atTop` tends to `0` at infinity for all `y`.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
133/2 |
Mathlib/MeasureTheory/Measure/TightNormed.lean |
1 |
2 |
['RemyDegenne', 'github-actions'] |
nobody |
0-47235 13 hours ago |
0-47308 13 hours ago |
0-47293 13 hours |
| 7596 |
alreadydone author:alreadydone |
feat: covering maps from properly discontinuous actions and discrete subgroups |
---
- [x] depends on: #23236
[](https://gitpod.io/from-referrer/)
|
file-removed
t-topology
|
351/21 |
Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Topology/Algebra/ConstMulAction.lean,Mathlib/Topology/Algebra/Group/Pointwise.lean,Mathlib/Topology/Covering/AddCircle.lean,Mathlib/Topology/Covering/Basic.lean,Mathlib/Topology/Covering/Galois.lean,Mathlib/Topology/Homotopy/Lifting.lean,Mathlib/Topology/Instances/AddCircle.lean |
9 |
16 |
['ADedecker', 'alreadydone', 'digama0', 'github-actions', 'mathlib4-dependent-issues-bot', 'tb65536'] |
nobody |
0-47031 13 hours ago |
1-25013 1 day ago |
25-30411 25 days |
| 24814 |
grunweg author:grunweg |
chore(LpSeminorm/Basic): golf a norm lemma using its enorm equivalent |
Follow-up to #24640: prove norm lemmas using their enorm counterpart.
---
[](https://gitpod.io/from-referrer/)
|
carleson
t-measure-probability
|
21/22 |
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean |
1 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
0-46116 12 hours ago |
0-52539 14 hours ago |
1-24429 1 day |
| 24792 |
eric-wieser author:eric-wieser |
feat: add `Matrix.vec` |
The module docstring explains the choice to make this diverge from `Function.uncurry`, as "row major" vectorization seems to be in the minority.
From eric-wieser/lean-matrix-cookbook
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
150/0 |
Mathlib.lean,Mathlib/Data/Matrix/Vec.lean |
2 |
22 |
['b-mehta', 'eric-wieser', 'github-actions'] |
nobody |
0-44568 12 hours ago |
1-10674 1 day ago |
1-79091 1 day |
| 23254 |
mariainesdff author:mariainesdff |
feat(Algebra/Order/BigOperators/GroupWithZero/Multiset.lean): add multiset_prod_le_pow_card |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
26/2 |
Mathlib/Algebra/Order/BigOperators/GroupWithZero/List.lean,Mathlib/Algebra/Order/BigOperators/GroupWithZero/Multiset.lean |
2 |
15 |
['Ruben-VandeVelde', 'erdOne', 'github-actions', 'mariainesdff'] |
nobody |
0-44205 12 hours ago |
15-36914 15 days ago |
44-69848 44 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-41451 11 hours ago |
1-45871 1 day ago |
2-22975 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-35505 9 hours ago |
0-58373 16 hours ago |
0-58358 16 hours |
| 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-32633 9 hours ago |
1-28056 1 day ago |
1-34170 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-30138 8 hours ago |
0-32219 8 hours ago |
5-60471 5 days |
| 24845 |
kebekus author:kebekus |
feat: integrability of log ‖meromorphic‖ |
For real-meromorphic functions `f`, establish interval integrability of `log ‖f ·‖`. In particular, show that `log ∘ sin` is interval integrable. For complex-meromorphic functions `f`, establish circle integrability of `log ‖f ·‖`.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. Integrability of `log ∘ sin` might be useful in future discussions of polylogarithms.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-measure-probability
t-analysis
|
198/2 |
Mathlib.lean,Mathlib/Analysis/Complex/Meromorphic/CircleIntegrability.lean,Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean,Mathlib/Analysis/SpecialFunctions/Integrals.lean,Mathlib/MeasureTheory/Integral/CircleIntegral.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean |
6 |
1 |
['github-actions'] |
nobody |
0-30017 8 hours ago |
0-30017 8 hours ago |
0-31452 8 hours |
| 21162 |
smmercuri author:smmercuri |
feat: add `Valued.WithZeroMulInt.tendsto_zero_pow_of_le_neg_one` |
If `K` is a valued ring taking values in the multiplicative integers wth a zero adjoined, then `Valued.WithZeroMulInt.tendsto_zero_pow_of_le_neg_one` is the result that `x ^ n` tends to zero in this ring if `v x` is at most `-1` valued.
---
- [x] depends on: #21160
- [x] depends on: #22055
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
label:t-algebra$ |
89/5 |
Mathlib.lean,Mathlib/Algebra/GroupWithZero/Int.lean,Mathlib/Algebra/GroupWithZero/WithZero.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Topology/Algebra/Valued/WithZeroMulInt.lean |
5 |
14 |
['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'smmercuri'] |
nobody |
0-29284 8 hours ago |
0-29284 8 hours ago |
60-56285 60 days |
| 24833 |
jcommelin author:jcommelin |
chore: swap the sides of the argument to `subtypePerm` |
This way the argument will not loop, when used with `simp`.
The argument also appears in many lemmas.
This change is a workaround for the extended simpNF linter, which runs `simp [h]` with `h` of that type.
Zulip: [#mathlib4 > simpNF lint with hyps @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/simpNF.20lint.20with.20hyps/near/517741799)
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
47/47 |
Mathlib/Algebra/Group/End.lean,Mathlib/GroupTheory/Perm/Centralizer.lean,Mathlib/GroupTheory/Perm/Cycle/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Factors.lean,Mathlib/GroupTheory/Perm/Finite.lean,Mathlib/GroupTheory/Perm/Sign.lean,Mathlib/GroupTheory/Perm/Support.lean |
7 |
10 |
['JovanGerb', 'eric-wieser', 'github-actions', 'jcommelin'] |
nobody |
0-26832 7 hours ago |
0-55173 15 hours ago |
0-55224 15 hours |
| 24849 |
jano-wol author:jano-wol |
feat: simple lie algebras have irreducible root systems |
Simple lie algebras have irreducible root systems
---
PR shows that simple lie algebras have irreducible root systems.
This work is part of the framework: https://github.com/orgs/leanprover-community/projects/17
Issue link: https://github.com/leanprover-community/mathlib4/issues/22831
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
176/0 |
Mathlib/Algebra/Lie/Weights/RootSystem.lean |
1 |
1 |
['github-actions'] |
nobody |
0-26270 7 hours ago |
0-26281 7 hours ago |
0-26331 7 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-21912 6 hours ago |
0-27137 7 hours ago |
0-27122 7 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-21380 5 hours ago |
0-21442 5 hours ago |
82-49358 82 days |
| 23920 |
YaelDillies author:YaelDillies |
feat: entourage-separated sets |
Define a notion of separation of a set relative to an entourage. This will be used to unify metric and dynamical separation.
From MiscYD and LeanAPAP
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
61/0 |
Mathlib.lean,Mathlib/Topology/UniformSpace/Separated.lean |
2 |
13 |
['D-Thomine', 'YaelDillies', 'b-mehta', 'github-actions'] |
ADedecker assignee:ADedecker |
0-20101 5 hours ago |
30-270 1 month ago |
30-9222 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-18935 5 hours ago |
6-9356 6 days ago |
30-58566 30 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-18738 5 hours ago |
3-1942 3 days ago |
3-3499 3 days |
| 24312 |
YaelDillies author:YaelDillies |
feat: more lemmas about torsion-free monoids |
The new imports just come from making `#min_imports` and `mk_iff` available earlier.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
large-import
maintainer-merge
t-algebra
label:t-algebra$ |
117/17 |
Mathlib/Algebra/Group/Pi/Lemmas.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Group/Subgroup/Basic.lean,Mathlib/Algebra/Group/Torsion.lean,Mathlib/Algebra/Lie/Weights/Chain.lean,Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean,Mathlib/GroupTheory/OrderOfElement.lean,Mathlib/GroupTheory/Torsion.lean,Mathlib/Topology/Instances/ZMultiples.lean |
9 |
7 |
['YaelDillies', 'b-mehta', 'github-actions', 'grunweg'] |
b-mehta assignee:b-mehta |
0-17669 4 hours ago |
0-19769 5 hours ago |
20-38843 20 days |
| 24578 |
b-mehta author:b-mehta |
feat(Pointwise): cardinality of product set in GroupWithZero |
This PR:
* generalises the assumptions to `card_le_card_image₂_left` and `card_le_card_image₂_right` and golf these: they previously required injectivity everywhere despite using it in only one place. (These lemmas were also used in exactly one place each in mathlib)
* adds `card_le_card_mul_left_of_injective` and `card_le_card_mul_right_of_injective` which generalise the typeclass assumptions on the existing `card_le_card_mul_left` and `card_le_card_mul_right`
* uses the above to add versions of `card_le_card_mul_left` and `card_le_card_mul_right` in groups with zero. This is useful for applying the pointwise constructions to fields
In fact, the first versions of all the above lemmas were written in this generality, but that was seemingly lost during an upstream.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
54/16 |
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean,Mathlib/Data/Finset/NAry.lean |
3 |
1 |
['github-actions'] |
nobody |
0-17320 4 hours ago |
5-42246 5 days ago |
9-79850 9 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-17302 4 hours ago |
0-17302 4 hours ago |
15-32719 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-16950 4 hours ago |
1-44505 1 day ago |
1-44520 1 day |
| 24465 |
adomani author:adomani |
feat: a linter to enforce formatting |
This linter enforces that the hypotheses of every declaration are correctly formatted.
This already required multiple PRs to make mathlib compliant. Ideally, little by little the linter can be extended to format more of mathlib.
---
The default linter option is `false`, but the lakefile enforces it to be `true`.
This means that the linter does not run on `MathlibTest`. However, the tests should still be compliant, since the default option was `true` in development and the tests were fixed.
[](https://gitpod.io/from-referrer/)
|
large-import
t-linter
|
624/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter.lean,Mathlib/Tactic/Linter/CommandStart.lean,MathlibTest/CommandStart.lean,MathlibTest/EuclideanSpace.lean,MathlibTest/Simps.lean,MathlibTest/Traversable.lean,MathlibTest/antidiagonal.lean,MathlibTest/delabLinearIndependent.lean,MathlibTest/matrix.lean,MathlibTest/norm_num.lean,MathlibTest/set_like.lean,MathlibTest/vec_notation.lean,lakefile.lean |
15 |
20 |
['Parcly-Taxel', 'adomani', 'github-actions', 'grunweg'] |
grunweg assignee:grunweg |
0-15418 4 hours ago |
10-54380 10 days ago* |
13-55982 13 days* |
| 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-14258 3 hours ago |
0-41663 11 hours ago |
0-66093 18 hours |
| 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 form 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 |
1 |
['github-actions'] |
nobody |
0-12822 3 hours ago |
0-12860 3 hours ago |
0-12877 3 hours |
| 24858 |
j-loreaux author:j-loreaux |
feat: `a * b⁻¹` for `a b : Aˣ` is unitary if `star a * a = star b * b` |
---
from [LeanOA](https://github.com/j-loreaux/LeanOA)
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
19/0 |
Mathlib/Algebra/Star/Unitary.lean |
1 |
1 |
['github-actions'] |
nobody |
0-12787 3 hours ago |
0-13863 3 hours ago |
0-13914 3 hours |
| 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-12707 3 hours ago |
2-26029 2 days ago |
2-31507 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-10991 3 hours ago |
0-52189 14 hours ago |
2-21816 2 days |
| 24856 |
FMLJohn author:FMLJohn |
feat(Topology/Subbasis): prove Alexander Subbasis Theorem |
---
[](https://gitpod.io/from-referrer/)
In this pull request, we have proved the Alexander Subbasis Theorem: if `X` has a topology `T` and `hTS : T = generateFrom S`, then `X` is compact if any open cover of `X` with elements in `S` has a finite subcover. |
t-topology |
38/0 |
Mathlib/Topology/Compactness/Compact.lean |
1 |
17 |
['FMLJohn', 'alreadydone', 'erdOne', 'github-actions'] |
nobody |
0-7863 2 hours ago |
0-16162 4 hours ago |
0-16147 4 hours |
| 21237 |
scholzhannah author:scholzhannah |
feat: a weaker definition of compactly generated spaces |
This PR defines compactly coherent spaces as a topological space where a set is open iff its intersection with every compact set is open in that compact set. This notion is typically called compactly generated in the literature. There is a different [definition of compactly generated spaces already in mathlib](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Compactness/CompactlyGeneratedSpace.html#CompactlyGeneratedSpace) but that definition is stronger than the one presented here. They do however agree on Hausdorff spaces. See [this wikipedia page](https://en.wikipedia.org/wiki/Compactly_generated_space) for an explanation for the three different definitions of compactly generated spaces used in literature.
Co-authored-by: Floris van Doorn
---
See also [this discussion on Zulip](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Compactly.20generated.20spaces) about compactly generated spaces.
- [x] depends on: #21134
[](https://gitpod.io/from-referrer/)
|
t-topology |
347/0 |
Mathlib.lean,Mathlib/Topology/Compactness/CompactlyCoherentSpace.lean,docs/references.bib |
3 |
22 |
['ADedecker', 'StevenClontz', 'github-actions', 'jzxia', 'mathlib4-dependent-issues-bot', 'scholzhannah', 'urkud'] |
nobody |
0-5541 1 hour ago |
0-20785 5 hours ago |
71-65842 71 days |
| 24855 |
euprunin author:euprunin |
feat: register more tactics for `hint` |
The following example shows test cases that `hint` now supports, which were unsupported prior to this PR:
```
import Mathlib
-- The tactics registered in this PR
register_hint compute_degree
register_hint field_simp
register_hint finiteness
-- "hint" now correctly suggests "compute_degree" which closes the goal (no closing tactic suggested prior to this PR)
open Polynomial in
example : natDegree ((X + 1) : Nat[X]) ≤ 1 := by hint
-- "hint" now correctly suggests "field_simp" which closes the goal (no closing tactic suggested prior to this PR)
example (R : Type) (a b : R) [CommRing R] (u₁ : Rˣ) : a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁ := by hint
-- "hint" now correctly suggests "finiteness" which closes the goal (no closing tactic suggested prior to this PR)
example (a : ℝ) : (ENNReal.ofReal (1 + a ^ 2))⁻¹ < ⊤ := by hint
``` |
maintainer-merge
t-meta
|
15/0 |
Mathlib/Tactic/ComputeDegree.lean,Mathlib/Tactic/FieldSimp.lean,Mathlib/Tactic/Finiteness.lean |
3 |
4 |
['euprunin', 'github-actions', 'grunweg'] |
nobody |
0-4853 1 hour ago |
0-7220 2 hours ago |
0-16610 4 hours |
| 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-4556 1 hour ago |
0-20711 5 hours ago |
11-14454 11 days |
| 24344 |
erdOne author:erdOne |
feat: miscellaneous lemmas about transcedence bases |
---
- [ ] depends on: #24806
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
207/10 |
Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean,Mathlib/FieldTheory/PrimitiveElement.lean,Mathlib/FieldTheory/PurelyInseparable/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableClosure.lean,Mathlib/LinearAlgebra/Dimension/Basic.lean,Mathlib/LinearAlgebra/Dimension/Free.lean,Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean,Mathlib/RingTheory/Algebraic/Basic.lean,Mathlib/RingTheory/AlgebraicIndependent/Basic.lean,Mathlib/RingTheory/AlgebraicIndependent/Defs.lean,Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean,Mathlib/RingTheory/Norm/Basic.lean |
14 |
19 |
['acmepjz', 'alreadydone', 'erdOne', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
alreadydone assignee:alreadydone |
0-4350 1 hour ago |
0-4350 1 hour ago |
18-1489 18 days |
| 24850 |
pechersky author:pechersky |
feat(Topology/UniformSpace/Ultra): uniform spaces induced by pseudometrics are ultra if system is ultra |
Any uniform space has a natural system of pseudometrics definable on it,
comprised of those pseudometrics constructed from a descending chain of
equivalence relation entourages. In a nonarchimedean uniformity, this pseudometric system
induces the uniformity.
---
[](https://gitpod.io/from-referrer/)
- [ ] depends on: #23111 |
t-topology |
693/0 |
Mathlib.lean,Mathlib/Topology/MetricSpace/BundledFun.lean,Mathlib/Topology/UniformSpace/Ultra/Pseudometrizable.lean |
3 |
7 |
['ADedecker', 'fpvandoorn', 'github-actions', 'mathlib4-dependent-issues-bot', 'pechersky'] |
nobody |
0-1329 22 minutes ago |
0-20658 5 hours ago |
0-22175 6 hours |
| 24860 |
j-loreaux author:j-loreaux |
feat: convenience theorems for uniform convergence |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
147/0 |
Mathlib/Topology/MetricSpace/UniformConvergence.lean,Mathlib/Topology/UniformSpace/CompactConvergence.lean,Mathlib/Topology/UniformSpace/UniformConvergence.lean |
3 |
1 |
['github-actions'] |
nobody |
0-336 5 minutes ago |
0-7940 2 hours ago |
0-7939 2 hours |