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 |
| 28511 |
YaelDillies author:YaelDillies |
feat(Finsupp): `congr!`-compatible version of `prod_congr` |
`congr!` doesn't like the `g1 x (f x)` appearing in the hypothesis of `Finsupp.prod_congr`: `f x` isn't a free variable.
Note: A few proofs broke due to `simp` using `congr` lemmas internally.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
17/11 |
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean,Mathlib/Algebra/Category/MonCat/Adjunctions.lean,Mathlib/Data/Finsupp/Multiset.lean,Mathlib/Data/Nat/Choose/Multinomial.lean,Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean |
5 |
12 |
['JovanGerb', 'YaelDillies', 'eric-wieser', 'github-actions', 'kmill'] |
kmill assignee:kmill |
74-50066 2 months ago |
96-56521 3 months ago |
96-56551 96 days |
| 26985 |
agjftucker author:agjftucker |
feat(Analysis/Calculus/Implicit): define implicitFunOfProdDomain |
This PR continues the work from #16743.
Original PR: https://github.com/leanprover-community/mathlib4/pull/16743
---
- [x] depends on: #28352
[](https://gitpod.io/from-referrer/) |
new-contributor
t-analysis
|
107/4 |
Mathlib/Analysis/Calculus/Implicit.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
hrmacbeth assignee:hrmacbeth |
44-85380 1 month ago |
52-59468 1 month ago |
52-61043 52 days |
| 28604 |
alreadydone author:alreadydone |
chore(Algebra/Ring/Defs): add two classes (minimally invasive version) |
Add the missing `NonAssocComm(Semi)ring` classes and add some missing instances between existing classes. Contrary to #28532, the approach here doesn't add any new `extends`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
59/17 |
Mathlib/Algebra/Colimit/DirectLimit.lean,Mathlib/Algebra/Ring/Defs.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean |
3 |
21 |
['alreadydone', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'riccardobrasca'] |
riccardobrasca assignee:riccardobrasca |
34-32232 1 month ago |
50-3174 1 month ago |
50-62188 50 days |
| 30432 |
kckennylau author:kckennylau |
feat(AlgebraicGeometry): define the non-vanishing locus of a set in Proj |
Given a subset `s : Set A`, the non-vanishing locus of `s` is the set of points whose corresponding prime ideal does not fully contain `s`. In other words, where not all elements of `s` vanish.
I could not find a name for this in the literature.
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
66/0 |
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean |
1 |
1 |
['github-actions'] |
alexjbest assignee:alexjbest |
32-85336 1 month ago |
40-57881 1 month ago |
40-57911 40 days |
| 29706 |
kim-em author:kim-em |
feat: add piCongrSigmaFiber and piCongrFiberwise equivalences |
## Summary
Add two new equivalence functions for working with fibers and sigma types:
- `Equiv.piCongrSigmaFiber`: transforms between functions on sigma fibers and regular pi types
- `Equiv.piCongrFiberwise`: lifts fiber-wise equivalences to product equivalences
These functions are from the FLT (Fermat's Last Theorem) project and are useful for manipulating dependent function types indexed by fibers of a function.
## Details
The new definitions allow for elegant transformations between:
1. Functions defined on sigma types representing fibers of a function
2. Regular dependent functions
These are particularly useful in algebraic contexts where one needs to work with products indexed by fibers.
## Context
This PR was prepared by Claude (Claude Code) based on the following prompt:
> "Please read FLT/Mathlib/Logic/Equiv/Basic.lean, and also the corresponding file in the Mathlib repository. Please prepare a PR to Mathlib containing this content, putting it at an appropriate point in the corresponding Mathlib file. Make sure the PR is label FLT, and write in the PR comment an explanation that the PR was prepared by Claude, including quoting the prompting."
The content is sourced from `/Users/kim/projects/lean/FLT/FLT/Mathlib/Logic/Equiv/Basic.lean` in the FLT project repository.
🤖 Generated with [Claude Code](https://claude.ai/code) |
FLT
t-logic
|
39/0 |
Mathlib/Logic/Equiv/Basic.lean |
1 |
5 |
['Ruben-VandeVelde', 'github-actions', 'kim-em'] |
fpvandoorn assignee:fpvandoorn |
32-3730 1 month ago |
65-40709 2 months ago |
65-56913 65 days |
| 30750 |
SnirBroshi author:SnirBroshi |
feat(Data/Quot): `toSet` and `equivClassOf` |
Define `toSet` which gets the set corresponding to an element of a quotient, and `equivClassOf` which gets the equivalence class of an element under a quotient.
---
I found these definitions helpful when working with quotients, specifically `ConnectedComponents` of a `TopologicalSpace`.
Additionally, I need `equivSigmaToSet` (in `Data/Setoid/Basic`) to prove things about `SimpleGraph.ConnectedComponent`.
[](https://gitpod.io/from-referrer/)
|
t-data |
179/0 |
Mathlib/Data/Quot.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Setoid/Basic.lean |
4 |
2 |
['eric-wieser', 'github-actions'] |
nobody |
29-53910 29 days ago |
30-43403 30 days ago |
30-43443 30 days |
| 29422 |
jsm28 author:jsm28 |
fix(Data/Finset/Max): Use `DecidableEq` for `insert` lemmas |
These `insert` in these lemma statements uses a `DecidableEq` instance derived from `LinearOrder`; make them syntactically more general by passing in a `DecidableEq` instance separately. (Some `insert` lemmas in this file already take `DecidableEq` hypotheses.)
---
[](https://gitpod.io/from-referrer/)
|
t-data |
8/8 |
Mathlib/Data/Finset/Max.lean |
1 |
2 |
['eric-wieser', 'github-actions'] |
pechersky assignee:pechersky |
27-85384 27 days ago |
73-83329 2 months ago |
73-83302 73 days |
| 30436 |
wwylele author:wwylele |
feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered |
This extends the existing `Finset.prod_one_sub_ordered` to infinite sum/product, and also adds the more natural `add` version.
Together with some previous PRs about infinite sum/prod and powerseries, this is part of my effort of upstreaming useful stuff from https://github.com/wwylele/PentagonalNumberTheorem. It starts getting into niche lemma, so suggestions such that not wanting this in mathlib, or it should be stated in a different form, are all welcomed.
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
44/0 |
Mathlib/Algebra/BigOperators/Ring/Finset.lean,Mathlib/Topology/Algebra/InfiniteSum/Ring.lean |
2 |
1 |
['github-actions'] |
grunweg assignee:grunweg |
25-85364 25 days ago |
33-24013 1 month ago |
40-43734 40 days |
| 27664 |
pechersky author:pechersky |
feat(Topology,Analysis): discrete topology metric space and normed groups |
Explicit construction of the discrete topology metric space and normed groups where `dist x y = 1` for all `x != y`
Provide PseudoMetricSpace, MetricSpace, Seminormed(Add)Group, and Normed(Add)Group constructions
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
138/0 |
Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Topology/MetricSpace/Basic.lean,Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean |
3 |
6 |
['github-actions', 'kckennylau', 'mathlib4-merge-conflict-bot', 'pechersky'] |
urkud assignee:urkud |
20-33222 20 days ago |
20-36075 20 days ago |
113-71290 113 days |
| 27308 |
xyzw12345 author:xyzw12345 |
feat(LinearAlgebra/SymmetricAlgebra): IsSymmetricAlgebra |
This PR continues the work from #24602.
Original PR: https://github.com/leanprover-community/mathlib4/pull/24602 |
t-algebra label:t-algebra$ |
107/1 |
Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/Basis.lean |
2 |
13 |
['github-actions', 'kckennylau', 'mattrobball', 'xyzw12345'] |
mattrobball assignee:mattrobball |
16-46528 16 days ago |
16-50158 16 days ago |
122-71797 122 days |
| 30181 |
alreadydone author:alreadydone |
feat(Data/Nat): reducible strong recursion |
+ Redefine `Nat.strongRec'` to allow Lean kernel computation (reduction) with the strong Nat recursor. TODO: maybe merge this with Batteries' `Nat.strongRec`.
+ Redefine `Nat.xgcd` to use `Nat.strongRec'` to allow kernel reduction.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
46/72 |
Mathlib/Data/Int/GCD.lean,Mathlib/Data/Nat/Digits/Defs.lean,Mathlib/Data/Nat/Init.lean |
3 |
4 |
['github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
pechersky assignee:pechersky |
15-85364 15 days ago |
48-11969 1 month ago |
48-18015 48 days |
| 30973 |
vihdzp author:vihdzp |
feat: generalize `Finsupp.lex_lt_iff_of_unique` |
---
- [x] depends on: #30481
[](https://gitpod.io/from-referrer/)
|
t-order |
46/13 |
Mathlib/Data/DFinsupp/Lex.lean,Mathlib/Data/Finsupp/Lex.lean,Mathlib/Order/PiLex.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
bryangingechen assignee:bryangingechen |
15-85353 15 days ago |
23-40171 23 days ago |
23-49037 23 days |
| 30994 |
kim-em author:kim-em |
feat: `fix_deprecations.py` script |
|
CI |
131/0 |
scripts/README.md,scripts/fix_deprecations.py |
2 |
18 |
['SnirBroshi', 'github-actions', 'kim-em'] |
bryangingechen assignee:bryangingechen |
15-85349 15 days ago |
23-55447 23 days ago |
23-55489 23 days |
| 30678 |
YaelDillies author:YaelDillies |
refactor(Algebra/Quaternion): intermediate `Module` instance |
This `Module` instance allows me to not ungeneralise the `NoZeroSMulDivisors R ℍ[R,c₁,c₂,c₃]` in #30563.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
45/28 |
Mathlib/Algebra/Quaternion.lean |
1 |
20 |
['YaelDillies', 'eric-wieser', 'github-actions'] |
joneugster assignee:joneugster |
14-57244 14 days ago |
31-56306 1 month ago |
31-81043 31 days |
| 30416 |
SnirBroshi author:SnirBroshi |
feat(Logic/Relation): lemmas relating `Relation.Map` and `Function.onFun` |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-logic
|
32/0 |
Mathlib/Logic/Relation.lean |
1 |
1 |
['github-actions'] |
awainverse assignee:awainverse |
14-37064 14 days ago |
41-17764 1 month ago |
41-19989 41 days |
| 31077 |
peabrainiac author:peabrainiac |
feat(Topology): `nhdsSetWithin` filter |
Add a relative version `nhdsSetWithin` of `nhdsSet`, analogous to `nhdsWithin`. The main application of this is a slightly more general variant of the tube lemma (`generalized_tube_lemma_left`) that came up while working in analysis files.
---
- [x] depends on: #31090
[](https://gitpod.io/from-referrer/)
|
t-topology |
159/4 |
Mathlib/Topology/Compactness/Compact.lean,Mathlib/Topology/ContinuousOn.lean,Mathlib/Topology/Defs/Filter.lean,Mathlib/Topology/NhdsWithin.lean |
4 |
7 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'peabrainiac', 'plp127'] |
fpvandoorn assignee:fpvandoorn |
13-85367 13 days ago |
21-24037 21 days ago |
21-57360 21 days |
| 30669 |
harahu author:harahu |
doc(Algebra): fix typos |
Found with help from Codex. I've tried to limit the PR to changes that are easy to review.
---
Should you find it difficult to review any particular part of this PR, know that I have nothing against trimming this PR down in favor of smaller free-standing PRs for the difficult-to-review parts.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
46/46 |
Mathlib/Algebra/AddConstMap/Basic.lean,Mathlib/Algebra/BigOperators/Pi.lean,Mathlib/Algebra/BrauerGroup/Defs.lean,Mathlib/Algebra/CharZero/AddMonoidHom.lean,Mathlib/Algebra/Field/Action/ConjAct.lean,Mathlib/Algebra/Field/Power.lean,Mathlib/Algebra/Field/ULift.lean,Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/Algebra/Homology/ComplexShapeSigns.lean,Mathlib/Algebra/Homology/DerivedCategory/Basic.lean,Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean,Mathlib/Algebra/Homology/Factorizations/Basic.lean,Mathlib/Algebra/Homology/HomologySequenceLemmas.lean,Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean,Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean,Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean,Mathlib/Algebra/Homology/HomotopyCategory/SingleFunctors.lean,Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean,Mathlib/Algebra/Homology/HomotopyCofiber.lean,Mathlib/Algebra/Homology/Localization.lean,Mathlib/Algebra/Lie/Free.lean,Mathlib/Algebra/Lie/InvariantForm.lean,Mathlib/Algebra/Lie/Quotient.lean,Mathlib/Algebra/Lie/Sl2.lean,Mathlib/Algebra/Lie/Submodule.lean,Mathlib/Algebra/Lie/TraceForm.lean,Mathlib/Algebra/Order/Ring/Nat.lean,Mathlib/Algebra/Polynomial/Lifts.lean,Mathlib/Algebra/Polynomial/RuleOfSigns.lean,Mathlib/Algebra/SkewMonoidAlgebra/Single.lean,Mathlib/Algebra/Star/NonUnitalSubsemiring.lean |
31 |
1 |
['github-actions'] |
kim-em assignee:kim-em |
13-4881 13 days ago |
32-47459 1 month ago |
32-52104 32 days |
| 30559 |
SnirBroshi author:SnirBroshi |
feat(Data/Sym/Sym2): add `Sym2.diagSet` |
feat(Data/Sym/Sym2): add `Sym2.diagSet`, the set of elements on the diagonal
---
This should help state theorems in simple graphs more easily (e.g. see `SimpleGraph.edgeSet_fromEdgeSet`, `SimpleGraph.edgeSet_eq_iff`, `SimpleGraph.edgeSet_sdiff_sdiff_isDiag`, `SimpleGraph.edgeSet_subset_setOf_not_isDiag`) and more importantly work with such statements.
[](https://gitpod.io/from-referrer/)
|
t-data |
42/5 |
Mathlib/Data/Sym/Sym2.lean |
1 |
1 |
['github-actions'] |
nobody |
11-82678 11 days ago |
37-13827 1 month ago |
37-13864 37 days |
| 28557 |
ShreckYe author:ShreckYe |
feat(Data/Nat/Factorization): some results on equality of powers of naturals proved from factorization |
I came across some math olympiad problems in number theory that could benefit from these theorems, expecially those on the prime power equality `p ^ m = a ^ n`. A specialized `eq_of_factorization_eq'` is added BTW to help with proof search. |
t-data |
96/0 |
Mathlib/Data/Nat/Factorization/Basic.lean,Mathlib/Data/Nat/Factorization/Defs.lean,Mathlib/Data/Nat/Factorization/PrimePow.lean |
3 |
22 |
['Ruben-VandeVelde', 'ShreckYe', 'github-actions', 'robin-carlier'] |
pechersky assignee:pechersky |
11-75443 11 days ago |
11-84147 11 days ago |
91-36233 91 days |
| 31416 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Walk): lemmas about the first and last darts/edges |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
43/0 |
Mathlib/Combinatorics/SimpleGraph/Walk.lean |
1 |
1 |
['github-actions'] |
nobody |
11-60492 11 days ago |
11-60494 11 days ago |
11-60527 11 days |
| 30232 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Connectivity/Subgraph): add `ConnectedComponent.toSubgraph` |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
43/0 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean |
3 |
20 |
['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib4-merge-conflict-bot'] |
YaelDillies assignee:YaelDillies |
11-58503 11 days ago |
11-58527 11 days ago |
45-38441 45 days |
| 31418 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): impl `Iso.degree_eq` and `Iso.minDegree_eq` and `Iso.maxDegree_eq` |
Move `Iso.card_edgeFinset_eq` further down in Finite.lean and implement:
- `Iso.degree_eq`
- `Iso.minDegree_eq`
- `Iso.maxDegree_eq`
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
51/12 |
Mathlib/Combinatorics/SimpleGraph/Finite.lean |
1 |
1 |
['github-actions'] |
nobody |
11-50468 11 days ago |
11-50742 11 days ago |
11-50766 11 days |
| 31206 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Incenter): bound coordinates of the incenter |
`inv_height_lt_sum_inv_height`, used to prove existence of the excenter opposite a vertex, has a remark in the docstring about what it also implies about the location of the incenter. Change this to an actual lemma `excenterWeights_empty_lt_inv_two` (which I think is the most natural form for that information that can then be applied further in any context where this information is useful).
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
16/2 |
Mathlib/Geometry/Euclidean/Incenter.lean |
1 |
1 |
['github-actions'] |
JovanGerb assignee:JovanGerb |
10-85357 10 days ago |
18-7285 18 days ago |
18-7260 18 days |
| 31467 |
maix00 author:maix00 |
feat(Combinatorics/SimpleGraph): add simp lemma `getVert_map` for `Walk.map` |
feat(Combinatorics/SimpleGraph) add simp lemma `getVert_map` to `Walk.map`; set longFile
simple fact but can only be proved by reverting the start point of the walk due to the inductive definition
---
- in concept similar to `List.getElem_map`
- deserve a simp lemma (useful when pushing walks between Subgraphs)
lemma getVert_map (i : ℕ) : (p.map f).getVert i = f (p.getVert i) := by
revert u; induction i with
| zero => simp
| succ => intro _ p; cases p <;> simp [*]
can not just use simp to prove this fact |
new-contributor
t-combinatorics
|
6/0 |
Mathlib/Combinatorics/SimpleGraph/Walk.lean |
1 |
1 |
['github-actions'] |
nobody |
10-41454 10 days ago |
10-41466 10 days ago |
10-41503 10 days |
| 31429 |
llllvvuu author:llllvvuu |
feat(Topology): generalize `IsModuleTopology` lemmas to semilinear maps |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
116/52 |
Mathlib/Topology/Algebra/Module/Basic.lean,Mathlib/Topology/Algebra/Module/ModuleTopology.lean |
2 |
3 |
['erdOne', 'github-actions', 'llllvvuu'] |
kbuzzard assignee:kbuzzard |
10-32454 10 days ago |
11-43108 11 days ago |
11-43105 11 days |
| 26912 |
pechersky author:pechersky |
chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` |
s-multiplying by a subtype is easiest to manipulate when both terms are in the ambient type. Many places that had to use the _def lemma for a rewrite, or to include it in a simp set, no longer have to.
Ported from #25308
---
[](https://gitpod.io/from-referrer/)
I found this being not-simp frustrating when talking about submodules over a valuation subring. |
t-algebra label:t-algebra$ |
67/66 |
Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/Group/Subgroup/Actions.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Module/LocalizedModule/Exact.lean,Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean,Mathlib/Algebra/Module/LocalizedModule/Submodule.lean,Mathlib/Algebra/Ring/Periodic.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean,Mathlib/LinearAlgebra/RootSystem/Irreducible.lean,Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean,Mathlib/RingTheory/Etale/Kaehler.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/LocalProperties/Projective.lean,Mathlib/RingTheory/Localization/InvSubmonoid.lean,Mathlib/RingTheory/OreLocalization/Basic.lean |
25 |
19 |
['artie2000', 'eric-wieser', 'github-actions', 'j-loreaux', 'linesthatinterlace', 'mathlib4-merge-conflict-bot', 'pechersky'] |
joelriou assignee:joelriou |
9-6854 9 days ago |
9-12796 9 days ago |
61-425 61 days |
| 30570 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Connectivity/Connected): `reachabilitySet` |
feat(Combinatorics/SimpleGraph/Connectivity/Connected): define `reachabilitySet` as the set of all pairs that have a walk between them
---
The main motivation is making it easier to work with the bridge definition (see `isBridge_iff_mem_edgeSet_and_notMem_reachabilitySet_deleteEdges` and `mem_edgeSet_and_mem_reachabilitySet_deleteEdges_iff_exists_isCycle_and_mem_edges` at the bottom), although I think this set is worth defining regardless.
- [x] depends on: #30542
[](https://gitpod.io/from-referrer/)
|
|
57/0 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
kex-y assignee:kex-y |
8-85366 8 days ago |
13-24955 13 days ago |
13-27466 13 days |
| 31242 |
plp127 author:plp127 |
feat: express filter as supremum of principal filter and free filter |
Prove a filter is free iff it is smaller than the cofinite filter. Prove that every filter decomposes as the disjoint supremum of a principal filter and a free filter.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
52/0 |
Mathlib/Order/Filter/Cofinite.lean,Mathlib/Order/Lattice.lean |
2 |
1 |
['github-actions'] |
bryangingechen assignee:bryangingechen |
8-85358 8 days ago |
16-76890 16 days ago |
16-76880 16 days |
| 31309 |
gasparattila author:gasparattila |
feat(Probability/Independence): reindexing lemmas for `iIndep*` |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
105/30 |
Mathlib/Probability/Independence/Basic.lean,Mathlib/Probability/Independence/Kernel.lean |
2 |
3 |
['EtienneC30', 'gasparattila', 'github-actions'] |
sgouezel assignee:sgouezel |
8-85347 8 days ago |
15-5712 15 days ago |
15-5749 15 days |
| 31315 |
Parcly-Taxel author:Parcly-Taxel |
feat: IMO 2010 Q5 |
I use an opaque power function to avoid `(kernel) deep recursion detected`. Cf. [#general > Panic in rw: Nat.pow exponent is too big @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Panic.20in.20rw.3A.20Nat.2Epow.20exponent.20is.20too.20big/near/513294906). |
IMO |
252/0 |
Archive.lean,Archive/Imo/Imo2010Q5.lean |
2 |
2 |
['github-actions', 'jsm28'] |
dwrensha assignee:dwrensha |
8-85346 8 days ago |
14-74084 14 days ago |
14-74065 14 days |
| 31401 |
SnirBroshi author:SnirBroshi |
feat(NumberTheory/Real/GoldenRatio): add two more fib identities |
---
In case using `grind` here is considered too fragile, there are alternative proofs without `grind` in the first commit, let me know if I should switch to them.
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
8/0 |
Mathlib/NumberTheory/Real/GoldenRatio.lean |
1 |
1 |
['github-actions'] |
mariainesdff assignee:mariainesdff |
8-85335 8 days ago |
12-7956 12 days ago |
12-7988 12 days |
| 28884 |
kim-em author:kim-em |
chore: deprecate ShiftLeft Int instance |
This PR proposes deprecating the `ShiftLeft Int` instance (which allows bit-shifting an integer by an integer), and similarly for `ShiftRight`.
These are unused in Mathlib.
I'm happy if someone wants to keep this, but I would ask that they:
* fix the doc-strings to explain what happens for negative shifts
* ~~restores the theorem `Int.shiftLeft_add` which I've commented out on `nightly-testing` (and then revert b33c9d7aaea on `nightly-testing`).~~
* ideally but optionally, complete the API, e.g. reducing shifts by casts back to shifts by a Nat |
t-data |
22/3 |
Mathlib/Data/Int/Bitwise.lean |
1 |
9 |
['Rob23oba', 'eric-wieser', 'github-actions', 'kim-em', 'mathlib4-merge-conflict-bot', 'pechersky'] |
pechersky assignee:pechersky |
8-13112 8 days ago |
65-85388 2 months ago |
87-53482 87 days |
| 13740 |
YaelDillies author:YaelDillies |
feat: more robust ae notation |
Make sure that, when `μ : FiniteMeasure Ω`, `f =ᵐ[μ] g` elaborates to `f =ᵐ[↑μ] g` instead of complaining about `OuterMeasureClass (FiniteMeasure Ω) (Set Ω) ℝ≥0∞` not existing.
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ae.20of.20a.20finite.20measure)
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
t-meta
|
67/8 |
Mathlib/MeasureTheory/Integral/Bochner/L1.lean,Mathlib/MeasureTheory/Measure/Decomposition/IntegralRNDeriv.lean,Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean,Mathlib/MeasureTheory/OuterMeasure/AE.lean,Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean,Mathlib/Probability/Notation.lean |
6 |
23 |
['YaelDillies', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant', 'urkud'] |
RemyDegenne assignee:RemyDegenne |
7-85370 7 days ago |
15-32460 15 days ago |
15-32416 15 days |
| 31441 |
harahu author:harahu |
doc(Dynamics): polish docstrings |
This PR fixes a batch of typos in `Dynamics`. The typos were found and fixed with the help of Codex.
---
[](https://gitpod.io/from-referrer/)
|
t-dynamics |
11/12 |
Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean,Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean,Mathlib/Dynamics/Ergodic/Ergodic.lean |
3 |
2 |
['github-actions', 'harahu'] |
sgouezel assignee:sgouezel |
7-85344 7 days ago |
11-24828 11 days ago |
11-24865 11 days |
| 31434 |
stepanholub author:stepanholub |
feat: simple divisibility lemma |
---
Add a simple lemma about divisibility. It can be seen as a description of the last step of the Euclidean algorithm (when only subtraction is used) |
t-data
new-contributor
|
6/0 |
Mathlib/Data/Nat/GCD/Basic.lean |
1 |
9 |
['github-actions', 'grunweg', 'ocfnash', 'stepanholub', 'wwylele'] |
nobody |
7-45777 7 days ago |
7-45778 7 days ago |
11-31757 11 days |
| 31579 |
xroblot author:xroblot |
feat(Data/Nat/Digits): prove the bijection induced by `Nat.ofDigits` and use it to compute the sum of the sum of digits |
We prove that `Nat.ofDigits` induces a bijection between the set of list of natural integers of length `l`
with coefficients `< b` and the set of natural integers `< b ^ l` and develop some API.
As a application, we prove that
```lean
theorem Nat.sum_digits_sum_eq {b : ℕ} (hb : 1 < b) (l : ℕ) :
∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = l * b ^ (l - 1) * b.choose 2
```
---
|
t-data |
186/0 |
Mathlib/Data/Nat/Digits/Lemmas.lean |
1 |
3 |
['eric-wieser', 'github-actions', 'xroblot'] |
nobody |
7-43943 7 days ago |
7-58643 7 days ago |
7-58677 7 days |
| 30133 |
smmercuri author:smmercuri |
feat: `WithVal v` and `WithVal w` are isomorphic as uniform spaces when `v` and `w` are equivalent valuations |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-topology
label:t-algebra$ |
97/0 |
Mathlib/Algebra/Order/Hom/Ring.lean,Mathlib/Topology/Algebra/Valued/WithVal.lean |
2 |
3 |
['github-actions', 'kbuzzard', 'robin-carlier'] |
kbuzzard and pechersky assignee:pechersky assignee:kbuzzard |
6-59257 6 days ago |
6-59459 6 days ago |
21-26362 21 days |
| 30879 |
grunweg author:grunweg |
feat: beta reduce in the `T%` elaborator |
Whenever the `T%` elaborator succeeds, head beta reduce the resulting application.
This enables applying it with anonymous functions or inside big operators without issue.
(For instance, all changes to `SmoothSection` in #30357 are now possible without additional `dsimp` steps.)
In the process, also extract the workhorse component of the elaborator into an independent function
and improve its doc-string to mention the corresponding tracing option.
---
- [x] depends on: #30413
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-differential-geometry
t-meta
|
62/20 |
Mathlib/Geometry/Manifold/Notation.lean,MathlibTest/DifferentialGeometry/Notation.lean |
2 |
14 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'thorimur'] |
thorimur assignee:thorimur |
6-10106 6 days ago |
6-22576 6 days ago |
19-64308 19 days |
| 31512 |
gasparattila author:gasparattila |
feat(MeasureTheory): typeclass for measurability of equality |
Currently, there are multiple lemmas of the form `MeasurableSet {x | f x = g x}` with different typeclass assumptions. This PR unifies them using a new `MeasurableEq` typeclass. A new instance for second-countable Hausdorff spaces is also added.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
75/50 |
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean,Mathlib/MeasureTheory/Group/Arithmetic.lean,Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean,Mathlib/MeasureTheory/MeasurableSpace/Defs.lean,Mathlib/MeasureTheory/Measure/AEMeasurable.lean,Mathlib/MeasureTheory/Measure/Trim.lean,Mathlib/Probability/Kernel/CondDistrib.lean,Mathlib/Probability/Kernel/Posterior.lean |
8 |
1 |
['github-actions'] |
RemyDegenne assignee:RemyDegenne |
5-85361 5 days ago |
9-31020 9 days ago |
9-31063 9 days |
| 31027 |
YaelDillies author:YaelDillies |
chore: shortcut instance for `Nat` to be mul-torsion-free |
This instance can already be found by typeclass search using the fact that `Nat` is a `LinearOrderedCommMonoidWithZero`, but it is better practice to not rely on algebraic order theory to prove algebraic results about such basic types. Similarly for `IsAddTorsionFree Int`.
From ClassFieldTheory
---
[](https://gitpod.io/from-referrer/)
|
CFT
t-algebra
label:t-algebra$ |
9/3 |
Mathlib/Algebra/Group/Int/Defs.lean,Mathlib/Algebra/Group/Nat/Defs.lean |
2 |
2 |
['github-actions', 'plp127'] |
mattrobball assignee:mattrobball |
5-31419 5 days ago |
18-23376 18 days ago |
23-23680 23 days |
| 31526 |
Aaron1011 author:Aaron1011 |
feat: Add multiplicative version of structure theorem for finitely generated abelian groups |
This is similar to the multiplicative version of the structure theorem for *finite* abelian groups (using a pi type instead of a direct sum)
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory
new-contributor
|
18/0 |
Mathlib/GroupTheory/FiniteAbelian/Basic.lean |
1 |
1 |
['github-actions'] |
tb65536 assignee:tb65536 |
4-85350 4 days ago |
8-84398 8 days ago |
8-84437 8 days |
| 31550 |
RemyDegenne author:RemyDegenne |
feat: properties of sub-Gaussian random variables |
Add several simple lemmas, and the fact that for `X, Y` two independent sub-Gaussian random variables such that `μ[X] ≥ μ[Y]`, the probability that `X ≤ Y` is bounded by an exponential function of `(μ[X] - μ[Y])^2`.
From the LeanBandits project.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
93/0 |
Mathlib/Probability/Moments/Basic.lean,Mathlib/Probability/Moments/IntegrableExpMul.lean,Mathlib/Probability/Moments/SubGaussian.lean |
3 |
1 |
['github-actions'] |
EtienneC30 assignee:EtienneC30 |
4-85344 4 days ago |
8-42046 8 days ago |
8-42089 8 days |
| 31564 |
EtienneC30 author:EtienneC30 |
feat: injectivity of the map forgetting the continuity of bilinear maps |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
15/0 |
Mathlib/Topology/Algebra/Module/StrongTopology.lean |
1 |
2 |
['github-actions', 'themathqueen'] |
PatrickMassot assignee:PatrickMassot |
4-85341 4 days ago |
8-11823 8 days ago |
8-11949 8 days |
| 31205 |
jsm28 author:jsm28 |
feat(Analysis/Convex/Side): affine combinations and sides of faces of a simplex |
Add lemmas saying when (in terms of the weights in the combinations) two affine combinations of the vertices of a simplex lie (strictly or weakly) on the same or opposite sides of a face of that simplex opposite a vertex.
---
- [x] depends on: #31204
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry |
216/0 |
Mathlib/Analysis/Convex/Side.lean |
1 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
4-16699 4 days ago |
4-21907 4 days ago |
4-22625 4 days |
| 31287 |
YaelDillies author:YaelDillies |
refactor(SetTheory/ZFC): deduplicate coercion to sets |
Currently, we have both `ZFSet.toSet` and `SetLike.coe` to turn a `ZFSet` into a `Set ZFSet`. This is bad for simp normal form. This PR removes the first spelling in favor of the second one.
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory |
111/104 |
Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/SetTheory/ZFC/Class.lean,Mathlib/SetTheory/ZFC/Ordinal.lean |
3 |
16 |
['YaelDillies', 'eric-wieser', 'github-actions', 'staroperator'] |
alreadydone assignee:alreadydone |
3-85361 3 days ago |
15-35279 15 days ago |
15-35316 15 days |
| 31592 |
gasparattila author:gasparattila |
chore(Tactic/Measurability): `fun_prop` lemmas for solving `MeasurableSet {x | ...}` goals |
Currently, lemmas of the form `MeasurableSet {x | ...}` cannot be used by `measurability`, because `simp` changes the goal to `Measurable fun x => ...`. This PR adds the necessary `fun_prop` lemmas so that they work with `measurability` (except for statements involving equality, which are done in #31512). This fixes #26620.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
13/7 |
Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean,Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean,MathlibTest/measurability.lean |
3 |
1 |
['github-actions'] |
kex-y assignee:kex-y |
3-85347 3 days ago |
7-38675 7 days ago |
7-38712 7 days |
| 31210 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/MongePoint): `reindex` lemmas |
Add lemmas about `mongePoint`, `mongePlane` and `orthocenter` applied to `Simplex.reindex`.
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
28/0 |
Mathlib/Geometry/Euclidean/MongePoint.lean |
1 |
2 |
['JovanGerb', 'github-actions'] |
JovanGerb assignee:JovanGerb |
3-84217 3 days ago |
17-81246 17 days ago |
17-81222 17 days |
| 31256 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/SignedDist): `signedInfDist_reindex` |
Add a lemma saying how `Affine.Simplex.signedInfDist` interacts with `Affine.Simplex.reindex`.
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
5/0 |
Mathlib/Geometry/Euclidean/SignedDist.lean |
1 |
8 |
['JovanGerb', 'github-actions', 'jsm28'] |
JovanGerb assignee:JovanGerb |
3-82622 3 days ago |
16-49526 16 days ago |
16-49501 16 days |
| 31693 |
YaelDillies author:YaelDillies |
feat(SimpleGraph): characterise when `fromEdgeSet` is less than another graph |
From ProofBench
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
5/2 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean |
1 |
3 |
['SnirBroshi', 'YaelDillies', 'github-actions'] |
nobody |
3-69845 3 days ago |
4-53721 4 days ago |
4-53761 4 days |
| 31054 |
jsm28 author:jsm28 |
feat(LinearAlgebra/AffineSpace/Simplex/Basic): faces and `reindex` |
Add lemmas about the set of vertices of a `face` or `faceOpposite` of `Simplex.reindex`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
14/0 |
Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean |
1 |
3 |
['JovanGerb', 'github-actions', 'jsm28'] |
kim-em assignee:kim-em |
3-47388 3 days ago |
22-46507 22 days ago |
22-46482 22 days |
| 31293 |
erdOne author:erdOne |
feat(Algebra/InfiniteSum): `HasProdUniformly` and friends |
Also refactors `HasProdUniformlyOn` to take one set instead of a family of sets. See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/SummableUniformlyOn/with/553935898
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-topology
RFC
label:t-algebra$ |
338/101 |
Mathlib/Analysis/NormedSpace/MultipliableUniformlyOn.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean,Mathlib/Topology/Algebra/InfiniteSum/TsumUniformlyOn.lean,Mathlib/Topology/Algebra/InfiniteSum/UniformOn.lean |
4 |
1 |
['github-actions'] |
jcommelin assignee:jcommelin |
3-33122 3 days ago |
15-26991 15 days ago |
15-26980 15 days |
| 31541 |
RemyDegenne author:RemyDegenne |
feat: Monotonicity of hitting times |
Monotonicity of hitting times with respect to their various arguments (set, minimal time, maximal time).
From the Brownian motion project.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
107/7 |
Mathlib/Probability/Process/HittingTime.lean |
1 |
10 |
['EtienneC30', 'RemyDegenne', 'github-actions'] |
nobody |
3-31954 3 days ago |
3-31954 3 days ago |
3-58122 3 days |
| 31603 |
alreadydone author:alreadydone |
chore(Algebra): make `RatFunc` an abbrev |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
RFC
label:t-algebra$ |
81/431 |
Mathlib/FieldTheory/Laurent.lean,Mathlib/FieldTheory/RatFunc/AsPolynomial.lean,Mathlib/FieldTheory/RatFunc/Basic.lean,Mathlib/FieldTheory/RatFunc/Defs.lean |
4 |
4 |
['github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
erdOne assignee:erdOne |
3-26799 3 days ago |
7-7715 7 days ago |
7-10176 7 days |
| 31692 |
YaelDillies author:YaelDillies |
feat(SimpleGraph): `deleteEdges` distributes over `sup` |
... and other lemmas
From ProofBench
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
8/1 |
Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean |
1 |
5 |
['SnirBroshi', 'YaelDillies', 'github-actions'] |
nobody |
3-23700 3 days ago |
4-54059 4 days ago |
4-54046 4 days |
| 31107 |
rudynicolop author:rudynicolop |
feat(Data/Multiset): add Multiset filter and bind lemmas |
Add basic lemmas equating `Multiset` `filter`, `filterMap`, `join`, and `bind` operations.
---
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
|
67/2 |
Mathlib/Data/Multiset/Bind.lean,Mathlib/Data/Multiset/Filter.lean |
2 |
7 |
['Ruben-VandeVelde', 'github-actions', 'rudynicolop'] |
nobody |
3-10004 3 days ago |
21-8373 21 days ago |
21-8409 21 days |
| 30213 |
SnirBroshi author:SnirBroshi |
feat(Data/List/GetD): golf and add lemmas for `get` and `getElem?` |
---
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
|
17/15 |
Mathlib/Data/List/GetD.lean |
1 |
20 |
['SnirBroshi', 'eric-wieser', 'github-actions', 'kim-em', 'themathqueen'] |
pechersky assignee:pechersky |
3-2781 3 days ago |
3-2781 3 days ago |
45-49420 45 days |
| 29688 |
tb65536 author:tb65536 |
feat(FieldTheory/IsGaloisGroup): prove the Galois correspondence for `IsGaloisGroup` |
This PR reproves the Galois correspondence for `IsGaloisGroup`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
122/0 |
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean |
1 |
9 |
['github-actions', 'kckennylau'] |
joneugster assignee:joneugster |
2-85866 2 days ago |
2-85866 2 days ago |
63-6699 63 days |
| 31523 |
kim-em author:kim-em |
chore: fix version comparison in lake update hook |
|
|
5/2 |
lakefile.lean |
1 |
3 |
['eric-wieser', 'github-actions', 'kim-em'] |
erdOne assignee:erdOne |
2-85369 2 days ago |
7-2143 7 days ago |
8-58470 8 days |
| 31758 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph): lemmas about the support of cycles |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
17/0 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean,Mathlib/Combinatorics/SimpleGraph/Paths.lean |
2 |
1 |
['github-actions'] |
nobody |
2-71330 2 days ago |
2-71337 2 days ago |
2-71372 2 days |
| 30758 |
Timeroot author:Timeroot |
chore: tag abs_inv and abs_div with grind= |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
2/1 |
Mathlib/Algebra/Order/Field/Basic.lean |
1 |
n/a |
['github-actions'] |
nobody |
2-59870 2 days ago |
unknown |
unknown |
| 31597 |
grunweg author:grunweg |
chore(AtLocation): allow throwing a warning when no progress is being made |
A future PR will use this to make `by_contra!` and friends warn if the `push_neg` step makes no progress.
Co-authored by: Jovan Gerbscheid
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
46/28 |
Mathlib/Tactic/Abel.lean,Mathlib/Tactic/Field.lean,Mathlib/Tactic/FieldSimp.lean,Mathlib/Tactic/NormNum/Core.lean,Mathlib/Tactic/Push.lean,Mathlib/Tactic/ReduceModChar.lean,Mathlib/Tactic/Ring/RingNF.lean,Mathlib/Util/AtLocation.lean,MathlibTest/FieldSimp.lean,MathlibTest/abel.lean |
10 |
5 |
['JovanGerb', 'fpvandoorn', 'github-actions'] |
thorimur assignee:thorimur |
2-27341 2 days ago |
7-10195 7 days ago |
7-10175 7 days |
| 31780 |
euprunin author:euprunin |
feat: add `grind` annotation for `SimpleGraph.Walk.length_support` |
---
Note that the lemma being annotated is
1. already actively used with `grind` via explicit `grind [lemma]` invocations in Mathlib, and
2. already tagged with `@[simp]`.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
8/8 |
Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean,Mathlib/Combinatorics/SimpleGraph/Walk.lean |
2 |
1 |
['github-actions'] |
nobody |
2-23617 2 days ago |
2-23930 2 days ago |
2-23965 2 days |
| 31785 |
euprunin author:euprunin |
feat: add `grind` annotation for `LinearPMap.mem_graph_iff` |
---
Note that the lemma being annotated is
1. already actively used with `grind` via explicit `grind [lemma]` invocations in Mathlib, and
2. already tagged with `@[simp]`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
6/6 |
Mathlib/LinearAlgebra/LinearPMap.lean |
1 |
1 |
['github-actions'] |
nobody |
2-20147 2 days ago |
2-20165 2 days ago |
2-20201 2 days |
| 30107 |
grunweg author:grunweg |
chore: track occurrences of 'nonrec' as technical debt |
Matches leanprover-community/leanprover-community.github.io#689: only merge when that is deemed a good idea.
--------
TODO: make the count more robust, for instance count all occurrences of "^nonrec " plus those of "^[private|protected] nonrec ".
---
[](https://gitpod.io/from-referrer/)
|
tech debt
CI
|
1/0 |
scripts/technical-debt-metrics.sh |
1 |
1 |
['github-actions'] |
jcommelin assignee:jcommelin |
1-85371 1 day ago |
50-58259 1 month ago |
50-58234 50 days |
| 30842 |
kim-em author:kim-em |
feat: add Aristotle task for command palette |
---
[](https://gitpod.io/from-referrer/)
|
CI |
128/0 |
.vscode/tasks.json,scripts/README.md,scripts/aristotle/README.md |
3 |
17 |
['eric-wieser', 'euprunin', 'github-actions', 'kim-em', 'vikram-shanker'] |
bryangingechen assignee:bryangingechen |
1-85369 1 day ago |
27-74717 27 days ago |
27-74754 27 days |
| 30853 |
JovanGerb author:JovanGerb |
feat(LinearAlgebra/AffineSpace/Simplex): `CoeFun` instance for `Simplex` |
This PR introduces the notation `s i` to refer to the `i`th vertex of simplex `s`, which replaces the current `s.points i`. It does this by adding a `CoeFun` instance.
I first tried using `FunLike`, but this came with some different problems related to discrimination tree indexing in `simp`.
---
[](https://gitpod.io/from-referrer/)
|
|
348/338 |
Archive/Imo/Imo2019Q2.lean,Mathlib/Analysis/Convex/Between.lean,Mathlib/Analysis/Normed/Affine/Simplex.lean,Mathlib/Geometry/Euclidean/Altitude.lean,Mathlib/Geometry/Euclidean/Angle/Sphere.lean,Mathlib/Geometry/Euclidean/Circumcenter.lean,Mathlib/Geometry/Euclidean/Incenter.lean,Mathlib/Geometry/Euclidean/MongePoint.lean,Mathlib/Geometry/Euclidean/Projection.lean,Mathlib/Geometry/Euclidean/SignedDist.lean,Mathlib/Geometry/Euclidean/Simplex.lean,Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean,Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean,scripts/nolints.json |
15 |
7 |
['JovanGerb', 'github-actions', 'jsm28'] |
mattrobball assignee:mattrobball |
1-85368 1 day ago |
27-43184 27 days ago |
27-43158 27 days |
| 31591 |
gasparattila author:gasparattila |
chore(Topology/Sets): use prefix naming for `toCompacts` in `simps` |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
6/8 |
Mathlib/Topology/Sets/Compacts.lean |
1 |
1 |
['github-actions'] |
jcommelin assignee:jcommelin |
1-85362 1 day ago |
7-41907 7 days ago |
7-41947 7 days |
| 31665 |
metakunt author:metakunt |
feat: Add exists_toCycle_toList and toCycle_next |
Adds exists_toCycle_toList and toCycle_next.
|
t-group-theory
new-contributor
|
23/0 |
Mathlib/GroupTheory/Perm/Cycle/Concrete.lean |
1 |
1 |
['github-actions'] |
tb65536 assignee:tb65536 |
1-85356 1 day ago |
5-26574 5 days ago |
5-26612 5 days |
| 30826 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Connectivity/Subgraph): map a walk to its own subgraph |
While this is not very interesting on its own, it opens the possibility of mapping a walk to any graph, given a graph homomorphism from the walk's subgraph.
---
Related: #30590
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
15/0 |
Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean |
1 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
b-mehta assignee:b-mehta |
1-78449 1 day ago |
1-78472 1 day ago |
28-17496 28 days |
| 31760 |
mcdoll author:mcdoll |
feat(Topology/Algebra): generalize `precomp` and `postcomp` to `UniformConvergenceCLM` |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
34/12 |
Mathlib/Topology/Algebra/Module/StrongTopology.lean |
1 |
1 |
['github-actions'] |
nobody |
1-70586 1 day ago |
1-70899 1 day ago |
2-57181 2 days |
| 31796 |
dobronx1325 author:dobronx1325 |
feat(Data/Real/EReal): add mul_lt_mul_of_pos_left theorem |
This PR adds the theorem `EReal.mul_lt_mul_of_pos_left`, which states that for a positive real number `a` and extended reals `b < c`, left multiplication by `a` preserves the strict order: `(a : EReal) * b < (a : EReal) * c`.
The theorem complements existing order-preserving properties for addition in `EReal` and extends the algebraic structure for multiplication. The proof uses basic properties of extended reals and order relations.
---
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
|
23/0 |
Mathlib/Data/EReal/Operations.lean |
1 |
1 |
['github-actions'] |
nobody |
1-69861 1 day ago |
1-69870 1 day ago |
1-69908 1 day |
| 31221 |
themathqueen author:themathqueen |
feat(LinearAlgebra/Matrix/ToLin): `star A.toLin' = (A.map star).toLin'` (intrinsic star) |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
43/0 |
Mathlib/Algebra/Star/LinearMap.lean,Mathlib/LinearAlgebra/Matrix/ToLin.lean |
2 |
1 |
['github-actions'] |
chrisflav assignee:chrisflav |
1-58762 1 day ago |
5-9025 5 days ago |
17-35027 17 days |
| 31663 |
xroblot author:xroblot |
feat(Algebra): more instances about `min` and `max` of sub-algebras |
Let `S₁ S₂ : Subalgebra R C`, we add more `Algebra` instances about their min and max, and also the corresponding `IsScalarTower` instances.
We also add the corresponding instances for `K₁ K₂ : IntermediateField F E`. Note that, in this situation, some `IsScalarTower` instances are not added since they can be deduced automatically.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
52/6 |
Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean |
2 |
5 |
['github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'xroblot'] |
mariainesdff assignee:mariainesdff |
1-58310 1 day ago |
5-24286 5 days ago |
5-29535 5 days |
| 29354 |
themathqueen author:themathqueen |
refactor(Algebra/Algebra/Equiv): allow for non-unital `AlgEquiv` |
This refactors `AlgEquiv` to allow for non-unital algebras. More specifically, we weaken the type class assumptions from:
```lean
structure AlgEquiv (R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B]
[Algebra R A] [Algebra R B]
```
to
```lean
structure AlgEquiv (R A B : Type*) [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B]
```
Instead of a `commutes'` field, we now have a `map_smul'` field. We also include a definition `AlgEquiv.ofCommutes` which takes in a `RingEquiv` and a `commutes'` field to match before and for convenience.
`StarAlgEquiv` now extends `AlgEquiv`. We also generalize a few files to allow for non-unital.
I suspect there are a few more things to generalize, but will leave this for later.
Co-authored-by: Jireh Loreaux
---
Revives #8686.
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
560/479 |
Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/Algebra/Opposite.lean,Mathlib/Algebra/Algebra/Pi.lean,Mathlib/Algebra/Algebra/Prod.lean,Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Algebra/Subalgebra/MulOpposite.lean,Mathlib/Algebra/Algebra/Tower.lean,Mathlib/Algebra/Algebra/TransferInstance.lean,Mathlib/Algebra/Category/AlgCat/Basic.lean,Mathlib/Algebra/Category/CommAlgCat/Basic.lean,Mathlib/Algebra/Category/CommAlgCat/FiniteType.lean,Mathlib/Algebra/Category/Ring/Constructions.lean,Mathlib/Algebra/DualQuaternion.lean,Mathlib/Algebra/MonoidAlgebra/Basic.lean,Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Algebra/MvPolynomial/Rename.lean,Mathlib/Algebra/Polynomial/AlgebraMap.lean,Mathlib/Algebra/Polynomial/Taylor.lean,Mathlib/Algebra/Quaternion.lean,Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean,Mathlib/Algebra/Star/Free.lean,Mathlib/Algebra/Star/StarAlgHom.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean,Mathlib/Analysis/Normed/Lp/LpEquiv.lean,Mathlib/Analysis/Normed/Module/Basic.lean,Mathlib/Analysis/RCLike/Basic.lean,Mathlib/Data/Matrix/Basic.lean,Mathlib/Data/Matrix/Composition.lean,Mathlib/Data/Matrix/DualNumber.lean,Mathlib/FieldTheory/Fixed.lean,Mathlib/FieldTheory/Galois/Basic.lean,Mathlib/FieldTheory/Galois/Notation.lean,Mathlib/FieldTheory/Galois/Profinite.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean,Mathlib/FieldTheory/IntermediateField/Basic.lean,Mathlib/FieldTheory/Normal/Basic.lean,Mathlib/FieldTheory/PrimitiveElement.lean,Mathlib/FieldTheory/RatFunc/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean,Mathlib/LinearAlgebra/Complex/Module.lean,Mathlib/LinearAlgebra/Matrix/Basis.lean,Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean,Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean,Mathlib/LinearAlgebra/Matrix/Reindex.lean,Mathlib/LinearAlgebra/Matrix/ToLin.lean,Mathlib/LinearAlgebra/Matrix/Unique.lean,Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean,Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean,Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean,Mathlib/NumberTheory/NumberField/Discriminant/Defs.lean,Mathlib/RingTheory/AdjoinRoot.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/DedekindDomain/Different.lean,Mathlib/RingTheory/Etale/Field.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/Flat/Equalizer.lean,Mathlib/RingTheory/FractionalIdeal/Operations.lean,Mathlib/RingTheory/Frobenius.lean,Mathlib/RingTheory/GradedAlgebra/Basic.lean,Mathlib/RingTheory/HahnSeries/PowerSeries.lean,Mathlib/RingTheory/Ideal/Operations.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean,Mathlib/RingTheory/Invariant/Basic.lean,Mathlib/RingTheory/Invariant/Profinite.lean,Mathlib/RingTheory/IsTensorProduct.lean,Mathlib/RingTheory/Jacobson/Artinian.lean,Mathlib/RingTheory/Jacobson/Ring.lean,Mathlib/RingTheory/Kaehler/Basic.lean,Mathlib/RingTheory/LaurentSeries.lean,Mathlib/RingTheory/Localization/Basic.lean,Mathlib/RingTheory/Localization/FractionRing.lean,Mathlib/RingTheory/MatrixAlgebra.lean,Mathlib/RingTheory/MvPolynomial/Localization.lean,Mathlib/RingTheory/Norm/Basic.lean,Mathlib/RingTheory/Polynomial/Quotient.lean,Mathlib/RingTheory/PolynomialAlgebra.lean,Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean,Mathlib/RingTheory/RingHom/FiniteType.lean,Mathlib/RingTheory/SimpleModule/Isotypic.lean,Mathlib/RingTheory/Smooth/Basic.lean,Mathlib/RingTheory/Smooth/Pi.lean,Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean,Mathlib/RingTheory/TensorProduct/Maps.lean,Mathlib/RingTheory/TensorProduct/MvPolynomial.lean,Mathlib/RingTheory/TensorProduct/Pi.lean,Mathlib/RingTheory/TensorProduct/Quotient.lean,Mathlib/RingTheory/Trace/Basic.lean,Mathlib/RingTheory/Unramified/Field.lean,Mathlib/Topology/Algebra/Algebra/Equiv.lean,Mathlib/Topology/Algebra/Module/FiniteDimension.lean,Mathlib/Topology/LocallyConstant/Algebra.lean,MathlibTest/GalNotation.lean |
100 |
39 |
['fpvandoorn', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
joelriou assignee:joelriou |
1-58268 1 day ago |
3-77773 3 days ago |
64-19462 64 days |
| 30988 |
erdOne author:erdOne |
feat(AlgebraicGeometry): descending affine cover of an inverse limit |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
347/35 |
Mathlib/Algebra/Category/Ring/Constructions.lean,Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean,Mathlib/AlgebraicGeometry/Gluing.lean,Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean,Mathlib/AlgebraicGeometry/Pullbacks.lean,Mathlib/AlgebraicGeometry/QuasiAffine.lean,Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean,Mathlib/Topology/LocalAtTarget.lean |
8 |
21 |
['chrisflav', 'erdOne', 'github-actions'] |
alexjbest assignee:alexjbest |
1-57816 1 day ago |
14-11371 14 days ago |
23-60733 23 days |
| 31565 |
EtienneC30 author:EtienneC30 |
feat: characteristic function equals dual characteristic function |
---
- [ ] depends on: #31563
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
7/0 |
Mathlib/MeasureTheory/Measure/CharacteristicFunction.lean |
1 |
5 |
['EtienneC30', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
nobody |
1-56917 1 day ago |
1-57230 1 day ago |
1-61219 1 day |
| 26212 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): the Rees theorem for depth |
In this PR we proved the Rees theorem for depth.
Co-authored-by: Hu Yongle
---
- [x] depends on: #27416
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
258/10 |
Mathlib/Algebra/Category/Grp/Preadditive.lean,Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean,Mathlib/RingTheory/Regular/Category.lean,Mathlib/RingTheory/Regular/Depth.lean |
4 |
n/a |
['Thmoas-Guan', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-55827 1 day ago |
unknown |
unknown |
| 31661 |
EtienneC30 author:EtienneC30 |
feat: many lemmas on integrability of a bounded linear map composed with two functions |
Generalize [MeasureTheory.Integrable.simpleFunc_mul](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Integral/Bochner/Set.html#MeasureTheory.Integrable.simpleFunc_mul) to a general bilinear map.
Specialize [ContinuousLinearMap.memLp_of_bilin](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/Holder.html#ContinuousLinearMap.memLp_of_bilin) to the case where one of the argument is bounded and the other is integrable.
Add a version of [MeasureTheory.Integrable.bdd_mul'](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/L1Space/Integrable.html#MeasureTheory.Integrable.bdd_mul') for scalar multiplication.
This is needed for #31666.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
67/22 |
Mathlib/MeasureTheory/Function/Holder.lean,Mathlib/MeasureTheory/Function/L1Space/Integrable.lean,Mathlib/MeasureTheory/Integral/Bochner/Set.lean |
3 |
1 |
['github-actions'] |
kex-y assignee:kex-y |
1-54169 1 day ago |
5-20284 5 days ago |
5-30920 5 days |
| 31778 |
xroblot author:xroblot |
feat(NumberField): formula for the sign of the discriminant |
Let `K` be a number field, then `(discr K).sign = (-1) ^ nrComplexPlaces K`
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
91/9 |
Mathlib/Analysis/Complex/Order.lean,Mathlib/GroupTheory/Perm/Cycle/Type.lean,Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean,Mathlib/NumberTheory/NumberField/EquivReindex.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean |
6 |
3 |
['github-actions', 'mathlib4-merge-conflict-bot', 'riccardobrasca'] |
riccardobrasca assignee:riccardobrasca |
1-53052 1 day ago |
1-53068 1 day ago |
2-27794 2 days |
| 31797 |
joelriou author:joelriou |
feat(AlgebraicTopology): multicoequalizers and pushouts of simplicial sets |
Let `X` be a simplicial set. In this PR, we show that a bicartesian square in the lattice of subcomplexes of `X` gives a pushout in the category `SSet`, and "multicoequalizer diagrams" in this lattice also allow to express certain subcomplexes as the multicoequalizers in the category of simplicial sets.
From https://github.com/joelriou/topcat-model-category
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology |
138/1 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean,Mathlib/AlgebraicTopology/SimplicialSet/SubcomplexColimits.lean,Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean,Mathlib/CategoryTheory/Limits/Types/Multicoequalizer.lean |
5 |
3 |
['github-actions', 'joelriou'] |
nobody |
1-51109 1 day ago |
1-56502 1 day ago |
1-56523 1 day |
| 31673 |
vasnesterov author:vasnesterov |
chore(Tactic/Order): use `AtomM` |
The `order` tactic uses its own machinery to collect atoms and facts from the context. This PR replaces it with `AtomM` to unify with other tactics like `ring`.
---
- [x] depends on: #26580
[](https://gitpod.io/from-referrer/)
|
t-meta |
167/132 |
Mathlib/Tactic/Order.lean,Mathlib/Tactic/Order/CollectFacts.lean,Mathlib/Tactic/Order/Graph/Basic.lean,Mathlib/Tactic/Order/Graph/Tarjan.lean,Mathlib/Tactic/Order/Preprocessing.lean,Mathlib/Tactic/Order/ToInt.lean,Mathlib/Util/AtomM.lean,MathlibTest/order.lean |
8 |
n/a |
['JovanGerb', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vasnesterov'] |
JovanGerb assignee:JovanGerb |
1-50902 1 day ago |
unknown |
unknown |
| 30877 |
YaelDillies author:YaelDillies |
feat(Algebra/MonoidAlgebra): extend the `R[M]` notation to `MonoidAlgebra R M` |
It currently only is notation for `AddMonoidAlgebra R M`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
212/161 |
Mathlib/Algebra/MonoidAlgebra/Basic.lean,Mathlib/Algebra/MonoidAlgebra/Defs.lean,Mathlib/Algebra/MonoidAlgebra/Lift.lean,Mathlib/Algebra/MonoidAlgebra/MapDomain.lean,Mathlib/Algebra/MonoidAlgebra/Module.lean,Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean,Mathlib/Algebra/MonoidAlgebra/Opposite.lean,Mathlib/Algebra/MonoidAlgebra/Support.lean,MathlibTest/Algebra/MonoidAlgebra/Defs.lean |
9 |
17 |
['YaelDillies', 'eric-wieser', 'github-actions', 'vihdzp'] |
kmill assignee:kmill |
1-50894 1 day ago |
23-22696 23 days ago |
23-53234 23 days |
| 31144 |
YaelDillies author:YaelDillies |
feat: transfer `FaithfulSMul`/`NoZeroSMulDivisors` along equivs |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
26/1 |
Mathlib/Algebra/Group/Action/TransferInstance.lean,Mathlib/Algebra/Module/TransferInstance.lean |
2 |
12 |
['YaelDillies', 'erdOne', 'github-actions', 'mathlib4-merge-conflict-bot'] |
kim-em assignee:kim-em |
1-50834 1 day ago |
1-50847 1 day ago |
18-61852 18 days |
| 27971 |
smmercuri author:smmercuri |
feat: weak approximation theorems for infinite places of a number field |
Under the diagonal embedding into infinite places, a number field $K$ is dense inside both the product $\prod_{v \mid \infty} (K, v)$, where $(K, v)$ denotes $K$ equipped with $v$'s topology, and the infinite adele ring $\prod_v K_v$.
This PR continues the work from #22153.
Original PR: https://github.com/leanprover-community/mathlib4/pull/22153
---
- [x] depends on: #27969 |
FLT
t-algebra
t-number-theory
label:t-algebra$ |
98/2 |
Mathlib/Analysis/Normed/Field/WithAbs.lean,Mathlib/NumberTheory/NumberField/AdeleRing.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean |
3 |
8 |
['faenuccio', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'smmercuri'] |
Vierkantor assignee:Vierkantor |
1-50832 1 day ago |
31-60940 1 month ago |
49-9086 49 days |
| 28719 |
mitchell-horner author:mitchell-horner |
refactor: redefine `IsTuranMaximal` |
Redefined `IsTuranMaximal := G.IsExtremal (CliqueFree · (r + 1))` and
- replaced `classical` in `IsTuranMaximal.le_iff_eq` with `DecidableRel`
- refactored `turanGraph.instDecidableRelAdj`, `turanGraph_zero`, `exists_isTuranMaximal`
- added `open Fintype`
- replaced `simp only` with `rw` or `simp_rw`
---
- [x] depends on: #28721
- [x] depends on: #29054
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
33/46 |
Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean |
1 |
13 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mitchell-horner', 'vihdzp'] |
kmill assignee:kmill |
1-50484 1 day ago |
1-50498 1 day ago |
80-68218 80 days |
| 30981 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π |
Add lemmas relating equal distance to two lines to bisecting the angle between them mod π (expressed as usual as equality of twice angles), building on the previous lemmas (#30477) dealing with bisection mod 2π.
---
- [ ] depends on: #30474
- [ ] depends on: #30477
- [ ] depends on: #30600
- [ ] depends on: #30703
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
146/4 |
Mathlib/Geometry/Euclidean/Angle/Bisector.lean |
1 |
4 |
['github-actions', 'jsm28', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
JovanGerb assignee:JovanGerb |
1-49906 1 day ago |
1-49923 1 day ago |
6-6753 6 days |
| 29946 |
smmercuri author:smmercuri |
feat(InfinitePlace/Ramification): embeddings of unramified/ramified infinite places satisfy `IsUnmixed/IsMixed` |
---
- [x] depends on: #29945
[](https://gitpod.io/from-referrer/)
|
FLT
t-number-theory
|
67/2 |
Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean |
1 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'smmercuri', 'xroblot'] |
alexjbest assignee:alexjbest |
1-49726 1 day ago |
22-18547 22 days ago |
52-45339 52 days |
| 30363 |
smmercuri author:smmercuri |
feat: `PadicInt` is isomorphic to the integers of the uniform space completion `(Rat.padicValuation p).Completion` |
- Uniform and ring isomorphisms between `𝒪[(Rat.padicValuation p).Completion]` and `ℤ_[p]`
- A homeomorphism `e : X ≃ Y` gives a closed set `{ x : X | p x ↔ q (e x) }` for clopen subsets given by `p` and `q`
- Move `Padic.isUnit_den` to an earlier file to avoid having to import `Padics.RingHoms` unnecessarily
---
- [x] depends on: #30361
[](https://gitpod.io/from-referrer/)
|
|
86/21 |
Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/NumberTheory/Padics/PadicIntegers.lean,Mathlib/NumberTheory/Padics/RingHoms.lean,Mathlib/NumberTheory/Padics/WithVal.lean,Mathlib/Topology/Homeomorph/Defs.lean |
5 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
dwrensha assignee:dwrensha |
1-49522 1 day ago |
1-49539 1 day ago |
42-21764 42 days |
| 31452 |
jsm28 author:jsm28 |
feat(Analysis/Convex/StrictCombination): convex combinations in strictly convex sets and spaces |
Add various lemmas that combinations of points (nonnegative weights, at least two weights of distinct points nonzero) in strictly convex sets lie in the interior of that set, or in strictly convex spaces or affine spaces for such spaces lie in a ball when the points lie in the corresponding closed ball.
These are analogous to existing lemmas for convex combinations and for pairs of points in strictly convex sets or spaces. In particular, the way `StrictConvex.centerMass_mem_interior` is stated with various hypotheses after the colon follows how `Convex.centerMass_mem` is stated (the hypotheses could of course move before the colon if they were then generalized for the induction).
Convenience lemmas for the cases of `closedInterior` (excluding vertices) of a simplex, and `interior` of a simplex, are included. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Triangle.20interior.20and.20its.20circumsphere/with/540305703 requested such a statement (in a different form). They don't include anything for bundled spheres since those are currently defined in `Mathlib.Geometry.Euclidean`, though given a suitable more generic name for the bundled sphere structure, various basic material about such spheres could move to a more generic metric space location, at which point it would be reasonable to add versions of these statements that use bundled spheres.
---
- [ ] depends on: #31450
- [ ] depends on: #31451
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry |
166/0 |
Mathlib.lean,Mathlib/Analysis/Convex/StrictCombination.lean |
2 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-49494 1 day ago |
1-49509 1 day ago |
6-36740 6 days |
| 31079 |
mcdoll author:mcdoll |
feat(Analysis/ContDiff): smooth compactly supported functions are dense in Lp |
---
- [x] depends on: #31278
[](https://gitpod.io/from-referrer/)
|
t-analysis |
125/16 |
Mathlib.lean,Mathlib/Analysis/Calculus/BumpFunction/SmoothApproxLp.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/UniformIntegrable.lean,Mathlib/MeasureTheory/Measure/MeasureSpace.lean,scripts/noshake.json |
6 |
19 |
['ADedecker', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mcdoll'] |
nobody |
1-48233 1 day ago |
1-57247 1 day ago |
9-50012 9 days |
| 27599 |
mitchell-horner author:mitchell-horner |
feat(Combinatorics/SimpleGraph): define `CompleteEquipartiteSubgraph` |
Define the complete equipartite subgraphs in `r` parts each of size `t` in `G` as the `r` subsets of vertices each of size `t` such that vertices in distinct subsets are adjacent.
In this case `Nonempty (G.CompleteEquipartiteSubgraph r t)` is equivalent to `completeEquipartiteGraph r t ⊑ G`, that is, finding `r` subsets of vertices each of size `t` in `G` such that vertices in distinct subsets are adjacent is equivalent to finding an injective homomorphism from `completeEquipartiteGraph r t` to `G`.
---
- [x] depends on: #27597
- [x] depends on: #30287
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
117/7 |
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean |
1 |
26 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'mitchell-horner'] |
YaelDillies assignee:YaelDillies |
1-45544 1 day ago |
1-50292 1 day ago |
51-21157 51 days |
| 31259 |
YaelDillies author:YaelDillies |
refactor(Dynamics): use `SetRel` notions of separation and cover |
... instead of the handmade ones.
---
[](https://gitpod.io/from-referrer/)
|
t-dynamics |
173/203 |
Mathlib/Data/Rel/Cover.lean,Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean,Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean,Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean,Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean,Mathlib/Dynamics/TopologicalEntropy/Subset.lean,Mathlib/Topology/UniformSpace/Defs.lean |
7 |
3 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
urkud assignee:urkud |
1-45388 1 day ago |
1-45404 1 day ago |
14-47331 14 days |
| 31198 |
YaelDillies author:YaelDillies |
feat(Algebra): characterise when a quotient is nontrivial |
From BrauerGroup and ClassFieldTheory
---
[](https://gitpod.io/from-referrer/)
|
CFT
t-algebra
label:t-algebra$ |
167/133 |
Mathlib/Algebra/Lie/Engel.lean,Mathlib/Algebra/Lie/Subalgebra.lean,Mathlib/Algebra/Module/Submodule/Lattice.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/GroupTheory/Congruence/Hom.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/GroupTheory/QuotientGroup/Defs.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean,Mathlib/LinearAlgebra/Quotient/Basic.lean,Mathlib/LinearAlgebra/Quotient/Defs.lean,Mathlib/NumberTheory/RamificationInertia/Basic.lean,Mathlib/RingTheory/AdjoinRoot.lean,Mathlib/RingTheory/ClassGroup.lean,Mathlib/RingTheory/Congruence/Basic.lean,Mathlib/RingTheory/Congruence/Defs.lean,Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean,Mathlib/RingTheory/Ideal/AssociatedPrime/Finiteness.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/Ideal/Quotient/Basic.lean,Mathlib/RingTheory/Jacobson/Ring.lean,Mathlib/RingTheory/KrullDimension/NonZeroDivisors.lean,Mathlib/RingTheory/KrullDimension/Regular.lean,Mathlib/RingTheory/LocalRing/Quotient.lean,Mathlib/RingTheory/NoetherNormalization.lean,Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean,Mathlib/RingTheory/Regular/Depth.lean,Mathlib/RingTheory/Regular/RegularSequence.lean,Mathlib/RingTheory/Support.lean,Mathlib/RingTheory/TensorProduct/Finite.lean,Mathlib/RingTheory/Unramified/LocalRing.lean |
32 |
3 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
kim-em assignee:kim-em |
1-45121 1 day ago |
1-45129 1 day ago |
18-1382 18 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/)
|
file-removed
t-algebra
label:t-algebra$ |
20/47 |
Mathlib.lean,Mathlib/Algebra/GCDMonoid/Nat.lean,Mathlib/Algebra/Group/Int/Units.lean,Mathlib/Algebra/Order/Ring/Abs.lean,Mathlib/Algebra/Ring/Int/Units.lean,Mathlib/Algebra/Ring/NegOnePow.lean,Mathlib/Data/Fintype/Units.lean,Mathlib/Data/Int/AbsoluteValue.lean,Mathlib/Data/Int/Associated.lean,Mathlib/GroupTheory/HNNExtension.lean,Mathlib/NumberTheory/NumberField/Basic.lean,MathlibTest/Zify.lean |
12 |
17 |
['YaelDillies', 'erdOne', 'eric-wieser', 'github-actions', 'j-loreaux', 'leanprover-community-bot-assistant', 'mathlib-bors'] |
eric-wieser assignee:eric-wieser |
1-44947 1 day ago |
190-40810 6 months ago |
275-13830 275 days |
| 31667 |
gasparattila author:gasparattila |
feat: add `WithLp.map` and variants |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
83/4 |
Mathlib/Analysis/Normed/Lp/WithLp.lean |
1 |
6 |
['eric-wieser', 'gasparattila', 'github-actions', 'j-loreaux'] |
nobody |
1-34950 1 day ago |
2-6283 2 days ago |
5-16094 5 days |
| 30827 |
dagurtomas author:dagurtomas |
feat(Condensed): constructions for light condensed objects can be done in an equivalent small category |
---
[](https://gitpod.io/from-referrer/)
|
t-condensed |
39/3 |
Mathlib/CategoryTheory/Sites/Equivalence.lean,Mathlib/Condensed/Light/Module.lean,Mathlib/Condensed/Light/Small.lean |
3 |
5 |
['dagurtomas', 'github-actions', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
joneugster assignee:joneugster |
1-34040 1 day ago |
1-34048 1 day ago |
24-74109 24 days |
| 31556 |
kebekus author:kebekus |
feat: behavior of the proximity function under addition |
Establish the behavior of the "Proximity Function" of Value Distribution theory with respect to addition.
This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. The formula established here is part of a larger package discussing the behavior of the Nenvanlinna height under algebraic manipulations of the functions.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
102/23 |
Mathlib/Analysis/Complex/ValueDistribution/ProximityFunction.lean,Mathlib/MeasureTheory/Integral/CircleAverage.lean,Mathlib/MeasureTheory/Integral/CircleIntegral.lean |
3 |
16 |
['github-actions', 'j-loreaux', 'kebekus'] |
sgouezel assignee:sgouezel |
1-33404 1 day ago |
1-33404 1 day ago |
7-46292 7 days |
| 26710 |
metakunt author:metakunt |
feat(Data/Nat/Digits/Lemmas): add digits_getD |
Adds digits_getD, an explicit computation of the i-th digits of n in base b representation. |
t-data
new-contributor
|
14/0 |
Mathlib/Data/Nat/Digits/Lemmas.lean |
1 |
21 |
['Ruben-VandeVelde', 'github-actions', 'metakunt', 'pechersky', 'plp127'] |
nobody |
1-32903 1 day ago |
12-65828 12 days ago |
69-59922 69 days |
| 30246 |
dwrensha author:dwrensha |
refactor: make Nat.digits use well-founded recursion once again |
#25864 made `Nat.digits` structurally recursive, which has some benefits. In doing so, however, it added significant complexity. As brought up in [this zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/structural.20recursion.20instead.20of.20well.20founded/near/543172385), on the balance that PR might not be considered an improvement.
The present PR reverts that change (but keeps a code golf that was bundled with it).
Note that recent improvements to core Lean mean that `simp` can handle the structurally recursive version without a problem:
```lean
example : digits 10 123456789 = [9,8,7,6,5,4,3,2,1] := by
simp [digits, digitsAux]
```
---
[](https://gitpod.io/from-referrer/)
|
t-data |
7/45 |
Mathlib/Data/Nat/Digits/Defs.lean |
1 |
8 |
['alreadydone', 'dwrensha', 'github-actions', 'j-loreaux', 'plp127'] |
TwoFX assignee:TwoFX |
1-32545 1 day ago |
46-27308 1 month ago |
46-27337 46 days |
| 30041 |
josephmckinsey author:josephmckinsey |
feat(Algebra/Order/Floor): generalize mul_floor_div theorems to rings and semirings |
Generalize `mul_cast_floor_div_cancel` from `Field` and `Semifield` to `Ring` and `Semiring`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
43/31 |
Mathlib/Algebra/Order/Floor/Ring.lean,Mathlib/Algebra/Order/Floor/Semifield.lean,Mathlib/Algebra/Order/Floor/Semiring.lean,Mathlib/Analysis/Real/OfDigits.lean |
4 |
12 |
['Ruben-VandeVelde', 'github-actions', 'josephmckinsey', 'mathlib4-merge-conflict-bot'] |
joneugster assignee:joneugster |
1-32449 1 day ago |
1-32468 1 day ago |
39-83179 39 days |
| 31648 |
bjornsolheim author:bjornsolheim |
feat(Geometry/Convex/Cone): characterize salient pointed cones |
Prove two lemmas characterizing salient pointed cones by the intersection of the cone and its negative.
These characterizations are often used as definitions in presentations where convex cones are by default pointed.
---
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
new-contributor
|
20/0 |
Mathlib/Geometry/Convex/Cone/Pointed.lean |
1 |
6 |
['bjornsolheim', 'github-actions', 'j-loreaux', 'mathlib4-merge-conflict-bot'] |
nobody |
1-31485 1 day ago |
1-31485 1 day ago |
4-60525 4 days |
| 25825 |
yuma-mizuno author:yuma-mizuno |
feat(CategoryTheory/Bicategory): define lax transformations between oplax functors |
and also define oplax transformations between lax functors.
- [ ] depends on: #25779
---
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #25672.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/25672* |
t-category-theory |
272/23 |
Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Lax.lean,Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean,scripts/noshake.json |
3 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-30645 1 day ago |
1-34715 1 day ago |
1-36222 1 day |
| 31514 |
staroperator author:staroperator |
feat(Order): reprove Dickson's lemma |
Reprove Dickson's lemma `Pi.wellQuasiOrderedLE` under assumption of preorder and well-quasi-order, and generalize it to any relation and/or product of well-quasi-ordered sets. Also add an instance of `WellQuasiOrderedLE` from `LinearOrder` and `WellFoundedLT`.
`Pi.isPWO` and `Finsupp.isPWO` are deprecated since they are superseded by `isPWO_of_wellQuasiOrderedLE` and instances.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
89/34 |
Mathlib/Data/Finsupp/PWO.lean,Mathlib/Order/Preorder/Finsupp.lean,Mathlib/Order/WellFoundedSet.lean,Mathlib/Order/WellQuasiOrder.lean,Mathlib/RingTheory/HahnSeries/PowerSeries.lean |
5 |
8 |
['github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] |
bryangingechen assignee:bryangingechen |
1-30508 1 day ago |
1-30526 1 day ago |
9-5516 9 days |
| 26110 |
YaelDillies author:YaelDillies |
feat(Algebra): more instances of subsingleton units |
Add some missing instances of `Subsingleton Mˣ`.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
28/13 |
Mathlib/Algebra/Group/Pi/Units.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Group/Submonoid/Units.lean,Mathlib/Algebra/Group/Units/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/Data/ZMod/Basic.lean,Mathlib/NumberTheory/DirichletCharacter/Basic.lean |
8 |
21 |
['YaelDillies', 'b-mehta', 'erdOne', 'github-actions', 'kckennylau', 'leanprover-community-bot-assistant', 'mathlib4-merge-conflict-bot', 'vihdzp'] |
b-mehta assignee:b-mehta |
1-28712 1 day ago |
70-26342 2 months ago |
154-26380 154 days |
| 30120 |
FernandoChu author:FernandoChu |
feat(CategoryTheory): Pullback of equalizer is an equalizer |
We show that the pullback of an equalizer (seen as a subobject) along some morphism `h` is the subobject that comes from the equalizer of the two original arrows precomposed with `h`. A `TODO` was completed in the process.
This is a prerequisite of the [MTT project](https://github.com/kyoDralliam/model-theory-topos), which aims to use the internal language of toposes to reason about e.g. sheaves. |
t-category-theory |
111/2 |
Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Limits.lean |
5 |
20 |
['FernandoChu', 'dagurtomas', 'github-actions', 'joelriou', 'mathlib4-merge-conflict-bot'] |
joneugster assignee:joneugster |
1-28622 1 day ago |
1-28630 1 day ago |
37-33315 37 days |
| 31364 |
YaelDillies author:YaelDillies |
feat: binomial random graphs |
From LeanCamCombi and formal-conjectures
---
- [x] depends on: #31391
- [x] depends on: #31392
- [x] depends on: #31393
- [x] depends on: #31394
- [x] depends on: #31396
- [x] depends on: #31397
- [x] depends on: #31398
- [x] depends on: #31442
- [x] depends on: #31443
- [x] depends on: #31445
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
t-combinatorics
|
268/0 |
Mathlib.lean,Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean,Mathlib/MeasureTheory/Measure/Dirac.lean,Mathlib/Probability/Combinatorics/BinomialRandomGraph/Defs.lean,Mathlib/Probability/Combinatorics/README.md,Mathlib/Probability/Distributions/BinomialRandom.lean |
6 |
9 |
['LibertasSpZ', 'YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
EtienneC30 assignee:EtienneC30 |
1-27964 1 day ago |
1-52520 1 day ago |
5-23762 5 days |
| 28141 |
YaelDillies author:YaelDillies |
chore: deprecate `BialgHom.coe_toLinearMap` |
`BialgHom.toLinearMap` is a fake projection.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
toric
|
5/11 |
Mathlib/RingTheory/Bialgebra/Hom.lean |
1 |
12 |
['YaelDillies', 'erdOne', 'eric-wieser', 'github-actions'] |
alreadydone assignee:alreadydone |
1-27361 1 day ago |
1-27361 1 day ago |
99-52286 99 days |
| 30618 |
wwylele author:wwylele |
feat(Combinatorics): Glaisher's theorem |
This proves Glaisher's theorem, one of the 1000+ theorems. It is also a generalization of [Euler's partition theorem](https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/Partition.lean), which can be rewritten as a collorary of this (will be in a different PR)
---
- [ ] depends on: #30599
- [ ] depends on #30567
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
194/9 |
Archive/Wiedijk100Theorems/Partition.lean,Mathlib.lean,Mathlib/Combinatorics/Enumerative/Partition/Basic.lean,Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean,Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean,Mathlib/RingTheory/PowerSeries/PiTopology.lean,docs/1000.yaml |
7 |
12 |
['b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'wwylele'] |
b-mehta assignee:b-mehta |
1-26541 1 day ago |
1-37788 1 day ago |
11-16550 11 days |
| 30800 |
dagurtomas author:dagurtomas |
feat(Condensed): cartesian monoidal functor LightProfinite -> LightCondSet |
---
[](https://gitpod.io/from-referrer/)
|
|
145/4 |
Mathlib.lean,Mathlib/Condensed/Light/Functors.lean,Mathlib/Topology/Category/CompHausLike/Cartesian.lean,Mathlib/Topology/Category/LightProfinite/Cartesian.lean |
4 |
7 |
['dagurtomas', 'github-actions', 'mathlib4-merge-conflict-bot'] |
adamtopaz assignee:adamtopaz |
1-25535 1 day ago |
1-34124 1 day ago |
28-77586 28 days |
| 31568 |
joelriou author:joelriou |
feat(CategoryTheory/Triangulated): truncation functors for t-structures |
In this PR, we introduce the truncation functors `< n` and ` ≥ n` for a `t`-structure.
---
- [x] depends on: #31536
- [x] depends on: #31539
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
278/0 |
Mathlib.lean,Mathlib/CategoryTheory/Triangulated/Basic.lean,Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-24334 1 day ago |
1-24353 1 day ago |
3-16860 3 days |
| 31231 |
Jlh18 author:Jlh18 |
refactor: MorphismProperty.HasPullbacksAlong |
Fix a morphism `f : X -> Y` in a category `C` with two morphism properties `P` and `Q`. To define a pullback functor between the subcategories of the slice categories `P.Over Q Y ⥤ P.Over Q X` one does not need the existence of all pullbacks along `f`. This refactor requires only that `f` has pullbacks of `P`-morphisms.
This property of "`f` has pullbacks of `P`-morphisms is defined as a typeclass. Note that it cannot simply be an `abbrev` like `Limits.HasPullbacksAlong` because the typeclass inference system will not be able to infer `P` that way.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
72/34 |
Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean,Mathlib/CategoryTheory/MorphismProperty/Limits.lean,Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean |
3 |
11 |
['Jlh18', 'chrisflav', 'github-actions', 'joelriou'] |
joelriou assignee:joelriou |
1-24168 1 day ago |
9-25948 9 days ago |
17-16957 17 days |
| 30132 |
callesonne author:callesonne |
feat(Bicategory/Functor/Strict): add `StrictPseudofunctor` |
This PR adds the notion of a strict pseudofunctor, where the coherence isomorphisms are equalities. This will be useful for #25561 where I define the bicategory of groupoids.
---
- [x] depends on: #30134
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-category-theory
|
181/0 |
Mathlib.lean,Mathlib/CategoryTheory/Bicategory/Functor/StrictPseudofunctor.lean |
2 |
17 |
['callesonne', 'dagurtomas', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
1-24077 1 day ago |
9-45566 9 days ago |
20-47736 20 days |
| 30069 |
IvanRenison author:IvanRenison |
feat(Combinatorics/SimpleGraph): add lemma `IsTree.dist_ne_of_adj` and necessary lemmas |
This contribution was created as part of the Utrecht Summerschool "Formalizing Mathematics in Lean" in July 2025.
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
34/0 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean |
1 |
9 |
['github-actions', 'mathlib4-merge-conflict-bot', 'themathqueen', 'vlad902'] |
kmill assignee:kmill |
1-23446 1 day ago |
1-23462 1 day ago |
50-73711 50 days |
| 31559 |
joelriou author:joelriou |
feat(Algebra/Homology): a factorization of morphisms of cochain complexes |
Let `C` be an abelian category with enough injectives. We show that any morphism `f : K ⟶ L` between bounded below cochain complexes in `C` can be factored as `i ≫ p` where `i : K ⟶ L'` is a monomorphism (with `L'` bounded below) and `p : L' ⟶ L` a quasi-isomorphism that is an epimorphism with a degreewise injective kernel. (This is part of the factorization axiom CM5 for a model category structure on bounded below cochain complexes.)
(This shall be used in the formalization of right derived functors using injective resolutions.)
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
186/32 |
Mathlib.lean,Mathlib/Algebra/Homology/Embedding/CochainComplex.lean,Mathlib/Algebra/Homology/Factorizations/CM5b.lean,Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean,Mathlib/Algebra/Homology/QuasiIso.lean,Mathlib/CategoryTheory/Preadditive/Injective/Basic.lean |
6 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
robin-carlier assignee:robin-carlier |
1-23031 1 day ago |
1-54347 1 day ago |
6-58772 6 days |
| 31307 |
euprunin author:euprunin |
chore: golf using the combination `ext` and `grind`. add `grind` annotations. |
---
[](https://gitpod.io/from-referrer/)
|
|
76/140 |
Mathlib/Algebra/Polynomial/Coeff.lean,Mathlib/Algebra/Polynomial/Reverse.lean,Mathlib/Data/DFinsupp/Defs.lean,Mathlib/Data/Finset/Pi.lean,Mathlib/Data/PFun.lean,Mathlib/Data/Part.lean,Mathlib/Order/Interval/Finset/Basic.lean,Mathlib/Order/Interval/Finset/Defs.lean,Mathlib/Topology/EMetricSpace/BoundedVariation.lean |
9 |
8 |
['euprunin', 'github-actions', 'j-loreaux', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
eric-wieser assignee:eric-wieser |
1-22474 1 day ago |
5-14230 5 days ago |
10-58551 10 days |
| 31421 |
joelriou author:joelriou |
feat(CategoryTheory): HasCardinalLT for MorphismProperty and ObjectProperty |
This PR introduces abbreviations to say that the type of objects or morphisms satisfying a certain property is of cardinality `< κ`.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-category-theory
|
122/0 |
Mathlib.lean,Mathlib/CategoryTheory/MorphismProperty/Basic.lean,Mathlib/CategoryTheory/MorphismProperty/HasCardinalLT.lean,Mathlib/CategoryTheory/ObjectProperty/HasCardinalLT.lean |
4 |
2 |
['github-actions', 'joelriou'] |
TwoFX assignee:TwoFX |
1-22435 1 day ago |
11-48326 11 days ago |
11-48302 11 days |
| 31818 |
euprunin author:euprunin |
feat: add `grind` annotations for `Set.mem_toFinset` and `Multiset.mem_toFinset` |
---
Note that the lemmas being annotated are
1. already actively used with `grind` via explicit `grind [lemma]` invocations in Mathlib, and
2. already tagged with `@[simp]`.
---
[](https://gitpod.io/from-referrer/)
|
|
5/5 |
Mathlib/Combinatorics/Enumerative/Partition/Basic.lean,Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean,Mathlib/Data/Finset/Dedup.lean,Mathlib/Data/Fintype/Sets.lean,Mathlib/Topology/Algebra/InfiniteSum/Defs.lean |
5 |
1 |
['github-actions'] |
nobody |
1-22111 1 day ago |
1-22207 1 day ago |
1-22182 1 day |
| 28346 |
joelriou author:joelriou |
feat(AlgebraicTopology/SimplicialSet): rank functions for pairings |
This PR introduces the type of (weak) rank functions for pairings, a notion introduced by Sean Moss, *Another approach to the Kan-Quillen model structure*. Rank functions can be used in order to show that certain pairings are regular (i.e. the ancestrality relation is well founded). In a future PR, it shall be shown that a regular pairing admits a rank function to the natural numbers, which shall be used to show that the corresponding inclusion of simplicial sets is a (strong) anodyne extension.
---
- [x] depends on: #28336
- [x] depends on: #28332
- [x] depends on: #28330
- [x] depends on: #28224
- [x] depends on: #27968
- [x] depends on: #28034
- [x] depends on: #26076
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology |
178/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean,Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Rank.lean |
3 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
1-20101 1 day ago |
unknown |
unknown |
| 30881 |
FlAmmmmING author:FlAmmmmING |
feat(RingTheory/PowerSeries/Schroder.lean): Define the generating function for large and small Schroder number |
Define the generating function for large and small Schroder number.
Main result : Prove some lemmas and the generating function of large Schroder.
Todo : Prove the generating function of small Schroder.
- depends on: #30609
---
[](https://gitpod.io/from-referrer/)
|
new-contributor |
352/1 |
Mathlib.lean,Mathlib/Combinatorics/Enumerative/Catalan.lean,Mathlib/RingTheory/PowerSeries/Schroder.lean |
3 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
dwrensha assignee:dwrensha |
1-19779 1 day ago |
1-40816 1 day ago |
26-28810 26 days |
| 26287 |
mbkybky author:mbkybky |
feat(Data/ENat/Lattice): coercion to `WithBot ℕ∞` commutes with `biSup` |
The coercion from `ℕ∞` to `WithBot ℕ∞` commutes with `biSup` and `biInf`.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
24/0 |
Mathlib/Data/ENat/Lattice.lean |
1 |
5 |
['github-actions', 'kckennylau', 'mbkybky'] |
ericrbg assignee:ericrbg |
1-18478 1 day ago |
50-35701 1 month ago |
130-36920 130 days |
| 31566 |
EtienneC30 author:EtienneC30 |
feat: real Gaussian measures are `gaussianReal` |
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability |
18/0 |
Mathlib/Probability/Distributions/Gaussian/Basic.lean |
1 |
4 |
['EtienneC30', 'RemyDegenne', 'github-actions', 'themathqueen'] |
urkud assignee:urkud |
1-12075 1 day ago |
8-11244 8 days ago |
8-11277 8 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.
Kalle's motivation for this is that he wants the standard portmanteau characterizations of convergence in distribution (weak convergence of probability measures), i.e., TFAE for
(T) The measures μs tend to the measure μ weakly.
(C) For any closed set F, the limsup of the measures of F under μs is at most the measure of F under μ, i.e., limsupᵢ μsᵢ(F) ≤ μ(F).
(O) For any open set G, the liminf of the measures of G under μs is at least the measure of G under μ, i.e., μ(G) ≤ liminfᵢ μsᵢ(G).
(B) For any Borel set B whose boundary carries no mass under μ, i.e. μ(∂B) = 0, the measures of B under μs tend to the measure of B under μ, i.e., limᵢ μsᵢ(B) = μ(B).
Currently, all other implications except those leading to (T) are along general filters, as they should (the four first bullet points in [Portmanteau.lean](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/Portmanteau.html)). The implication leading to (T) is only along sequences, since its proof relies on Fatou's lemma (the fifth bullet point in [Portmanteau.lean](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/Portmanteau.html)). Convergence in distribution (T) is very often what one wants to conclude, and sequences are extremely restrictive (not only for statistical mechanics) (although they can be shown to be in principle sufficient in separable metric spaces by [Lévy-Prokhorov metrizability](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.html#MeasureTheory.instPseudoMetrizableSpaceProbabilityMeasureOfSeparableSpace), but that seems far from a principled approach). To avoid the use of Fatou's lemma, one needs first of all a generalization of limsup results like in #15115, and some way to get left-continuous approximations from above for ENNReal-valued functions --- the ceiling function would be a pretty natural choice for this.
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$ |
237/0 |
Mathlib.lean,Mathlib/Algebra/Order/Floor/Extended.lean |
2 |
26 |
['YaelDillies', 'b-mehta', 'dagurtomas', 'eric-wieser', 'github-actions', 'grunweg', 'kkytola', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'urkud'] |
alreadydone assignee:alreadydone |
1-3168 1 day ago |
1-48923 1 day ago |
240-63727 240 days |
| 22782 |
alreadydone author:alreadydone |
feat(Topology): étalé space associated to a predicate on sections |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
886/160 |
Mathlib.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean,Mathlib/Data/Set/Operations.lean,Mathlib/Geometry/Manifold/Sheaf/Smooth.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/Topology/EtaleSpace.lean,Mathlib/Topology/IsLocalHomeomorph.lean,Mathlib/Topology/Sheaves/LocalPredicate.lean,Mathlib/Topology/Sheaves/Sheafify.lean,Mathlib/Topology/Sheaves/Stalks.lean |
10 |
16 |
['AntoineChambert-Loir', 'alreadydone', 'github-actions', 'jcommelin', 'leanprover-community-bot-assistant', 'mathlib4-merge-conflict-bot'] |
PatrickMassot assignee:PatrickMassot |
1-1901 1 day ago |
107-3617 3 months ago |
30-3459 30 days |
| 31799 |
mcdoll author:mcdoll |
chore: make `CLM.extend` total and define `LM.leftInverse` |
- Make `ContinuousLinearMap.extend` a total function
- Define `LinearMap.leftInverse` as a total function with junk value if the input is not invertible.
Required for #31074
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
144/99 |
Mathlib/Analysis/InnerProductSpace/LinearPMap.lean,Mathlib/Analysis/Normed/Operator/Extend.lean,Mathlib/LinearAlgebra/Basis/VectorSpace.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/MeasureTheory/Function/Holder.lean,Mathlib/MeasureTheory/Integral/Bochner/L1.lean,Mathlib/MeasureTheory/Integral/SetToL1.lean,Mathlib/RepresentationTheory/Maschke.lean |
8 |
3 |
['github-actions', 'j-loreaux', 'mcdoll'] |
nobody |
1-711 1 day ago |
1-711 1 day ago |
1-20207 1 day |
| 31362 |
BeibeiX0 author:BeibeiX0 |
feat(partitions): generalized pentagonal numbers. |
feat(partitions): generalized pentagonal numbers and error term eₙ
Introduce infrastructure around Euler’s pentagonal number theorem:
* Define parity counters for strict partitions:
- `p_even_distinct n`
- `p_odd_distinct n`
- `strict_partitions_parity_diff n := (p_even_distinct n : ℤ) - (p_odd_distinct n : ℤ)`
* Generalized pentagonal numbers:
- `generalizedPentagonalZ : ℤ → ℤ` with basic API (`gpn_nonneg`, `gpn_coe`)
- `generalizedPentagonalNum : ℤ → ℕ`
- parity lemma `even_neg_j_add_three_j_sq` and `even_neg_j_add_three_j_sq'`
- search window equivalence `exists_j_iff_exists_j_in_range`
- `Decidable (∃ j : ℤ, n = generalizedPentagonalZ j)` via a bounded range
* Euler error term:
- `error_term_e n : ℤ` (≔ `(-1)^{|j|}` if `n = generalizedPentagonalZ j` for some `j`,
and `0` otherwise)
* Finite product cut-off of the generating function:
- `E n : PowerSeries ℤ := ∏_{k=1}^{n+1} (1 - X^k)`
- lemma `coeff_E_eq_coeff_cutoff`
Implementation notes:
* Keep the integer-valued version `generalizedPentagonalZ` for arithmetic lemmas and
signs; obtain the natural-number version via `Int.toNat`.
* The bounded search lemma gives a small window `j ∈ [-(n+1), n+1]` for decidability.
Motivation:
* This is groundwork for proofs of Euler’s pentagonal number theorem and parity
identities relating strict partitions to the error term.
References:
* https://en.wikipedia.org/wiki/Pentagonal_number_theorem |
new-contributor
t-combinatorics
|
258/0 |
Mathlib.lean,Mathlib/Combinatorics/Enumerative/PentagonalNumbers.lean |
2 |
8 |
['BeibeiX0', 'dagurtomas', 'github-actions', 'mathlib4-merge-conflict-bot', 'wwylele'] |
awainverse assignee:awainverse |
0-85370 23 hours ago |
1-30229 1 day ago |
9-57797 9 days |
| 31286 |
bryangingechen author:bryangingechen |
ci: make new contributor labeling work for users with a private profile |
The search API we switched to in #30859 returns an error when we try to filter for users with a private profile ([example log](https://github.com/leanprover-community/mathlib4/actions/runs/19093647472/job/54548944242?pr=31272)). We switch to searching for closed issues in the repo, which was working before. We then filter these for closed PRs whose titles start with `[Merged by bors] -`.
We also include a slight optimization so that we don't have to page through all of a user's closed issues but stop when we find enough that count as merged PRs (>5 at the moment).
written with help from Claude
---
[](https://gitpod.io/from-referrer/)
|
CI |
41/16 |
.github/workflows/label_new_contributor.yml |
1 |
8 |
['Ruben-VandeVelde', 'bryangingechen', 'github-actions'] |
joneugster assignee:joneugster |
0-82004 22 hours ago |
15-35858 15 days ago |
15-35894 15 days |
| 22771 |
alreadydone author:alreadydone |
feat(Homotopy/Lifting): monodromy of covering maps and lifting criterion |
Define the monodromy of a covering map: given a path in the base space, lifting it through the covering map induces a bijection between the fibers at the two endpoints of the path. Definition 2.1 in https://ncatlab.org/nlab/show/monodromy.
---
- [ ] depends on: #28234
- [x] depends on: #22649
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology |
193/146 |
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 |
5 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
PatrickMassot assignee:PatrickMassot |
0-81017 22 hours ago |
89-47693 2 months ago |
144-35711 144 days |
| 31133 |
thorimur author:thorimur |
feat(Linter): combinators for linter option boilerplate |
Provides simple combinators `whenLinterOption` and `whenNotLinterOption` to parallel `whenPPOption` and `whenNotPPOption`, and bundles `withSetOptionIn` and `whenLinterOption` into `whenLinterActivated`.
Currently, a typical linter action uses
```lean
run := withSetOptionIn fun stx => do
unless getLinterValue linter.foo (← getLinterOptions) do
return
...
```
This allows us to simply write
```lean
run := whenLinterActivated linter.foo fun stx => do
...
```
Using these combinators in Mathlib's linters is left to a subsequent PR (#31134).
Since this is a utility used in basic linters, including the header linter, we exclude it from `lint-style`.
---
I'm not sure I'm doing the right thing here re: Mathlib.Init. What exactly should happen?
[](https://gitpod.io/from-referrer/)
|
t-linter
t-meta
|
50/0 |
Mathlib.lean,Mathlib/Lean/Linter.lean,scripts/lint-style.lean |
3 |
4 |
['adomani', 'github-actions', 'mathlib4-merge-conflict-bot', 'thorimur'] |
adomani assignee:adomani |
0-80606 22 hours ago |
1-59062 1 day ago |
18-36989 18 days |
| 31725 |
thorimur author:thorimur |
feat: InfoTree API: `InfoTree.findSome`(`M`)`?` and `InfoTree.onHighestNode?` |
This PR adds the following basic `InfoTree` API:
```lean
def findSome? {α} (f : ContextInfo → Info → PersistentArray InfoTree → Option α)
(t : InfoTree) (ctx? : Option ContextInfo := none) : Option α
```
```lean
def findSomeM? {m : Type → Type} [Monad m] {α}
(f : ContextInfo → Info → PersistentArray InfoTree → m (Option α))
(t : InfoTree) (ctx? : Option ContextInfo := none) : m (Option α)
```
```lean
def onHighestNode? {α} (t : InfoTree) (ctx? : Option ContextInfo)
(f : ContextInfo → Info → PersistentArray InfoTree → α) : Option α
```
Note that `onHighestNode?` has an explicit `Option ContextInfo` argument. This is because `onHighestNode?` is more likely to be called in the middle of a larger traversal, during which it is essential to pass the surrounding `ContextInfo`. Making this argument explicit mitigates the increased risk of a footgun here.
This functionality is motivated by use in other PRs.
---
Aside: I wonder if we should have `InfoT`. Then the footguns here would not be present, as all API involved would update the `ContextInfo`. But in the meantime we must manage the infotree context manually during traversal.
[](https://gitpod.io/from-referrer/)
|
t-meta |
55/2 |
Mathlib/Lean/Elab/InfoTree.lean |
1 |
1 |
['github-actions'] |
adamtopaz assignee:adamtopaz |
0-80271 22 hours ago |
4-5075 4 days ago |
4-5066 4 days |
| 31244 |
kim-em author:kim-em |
chore: use generic `map_X` lemmas where possible |
While thinking about grind annotations for homomorphisms, it occurs to me that automation is more likely when we use the generic, rather than namespaced, lemmas where possible. This is some cleanup in that direction. |
|
812/856 |
Archive/Examples/Eisenstein.lean,Archive/Wiedijk100Theorems/Partition.lean,Counterexamples/CliffordAlgebraNotInjective.lean,Counterexamples/DirectSumIsInternal.lean,Counterexamples/Phillips.lean,Mathlib/Algebra/Algebra/Tower.lean,Mathlib/Algebra/Category/Grp/FilteredColimits.lean,Mathlib/Algebra/Category/Grp/Images.lean,Mathlib/Algebra/Category/Grp/ZModuleEquivalence.lean,Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean,Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean,Mathlib/Algebra/Category/ModuleCat/Images.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean,Mathlib/Algebra/Category/MonCat/FilteredColimits.lean,Mathlib/Algebra/CharP/Pi.lean,Mathlib/Algebra/CharP/Subring.lean,Mathlib/Algebra/Colimit/Module.lean,Mathlib/Algebra/Colimit/Ring.lean,Mathlib/Algebra/CubicDiscriminant.lean,Mathlib/Algebra/DirectSum/Algebra.lean,Mathlib/Algebra/DirectSum/Basic.lean,Mathlib/Algebra/DirectSum/Ring.lean,Mathlib/Algebra/Exact.lean,Mathlib/Algebra/FreeAbelianGroup/Finsupp.lean,Mathlib/Algebra/FreeMonoid/Basic.lean,Mathlib/Algebra/GCDMonoid/Basic.lean,Mathlib/Algebra/Group/ForwardDiff.lean,Mathlib/Algebra/Group/Hom/Defs.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Group/Subgroup/Pointwise.lean,Mathlib/Algebra/Group/Submonoid/Pointwise.lean,Mathlib/Algebra/GroupWithZero/Action/End.lean,Mathlib/Algebra/GroupWithZero/Subgroup.lean,Mathlib/Algebra/GroupWithZero/Submonoid/Pointwise.lean,Mathlib/Algebra/Homology/ComplexShapeSigns.lean,Mathlib/Algebra/Homology/Homotopy.lean,Mathlib/Algebra/Lie/BaseChange.lean,Mathlib/Algebra/Lie/Basic.lean,Mathlib/Algebra/Lie/Character.lean,Mathlib/Algebra/Lie/DirectSum.lean,Mathlib/Algebra/Lie/Free.lean,Mathlib/Algebra/Lie/TensorProduct.lean,Mathlib/Algebra/Lie/TraceForm.lean,Mathlib/Algebra/Lie/Weights/Basic.lean,Mathlib/Algebra/Lie/Weights/Cartan.lean,Mathlib/Algebra/Module/Equiv/Basic.lean,Mathlib/Algebra/Module/Injective.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/Module/LinearMap/End.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Module/LocalizedModule/Exact.lean,Mathlib/Algebra/Module/Submodule/Bilinear.lean,Mathlib/Algebra/Module/Submodule/Ker.lean,Mathlib/Algebra/Module/Submodule/LinearMap.lean,Mathlib/Algebra/Module/ZLattice/Covolume.lean,Mathlib/Algebra/MonoidAlgebra/Grading.lean,Mathlib/Algebra/MvPolynomial/CommRing.lean,Mathlib/Algebra/MvPolynomial/Derivation.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Algebra/MvPolynomial/Eval.lean,Mathlib/Algebra/MvPolynomial/Funext.lean,Mathlib/Algebra/MvPolynomial/Monad.lean,Mathlib/Algebra/Order/CompleteField.lean,Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Algebra/Polynomial/Coeff.lean,Mathlib/Algebra/Polynomial/Degree/Lemmas.lean,Mathlib/Algebra/Polynomial/DenomsClearable.lean,Mathlib/Algebra/Polynomial/Derivative.lean,Mathlib/Algebra/Polynomial/Eval/Coeff.lean,Mathlib/Algebra/Polynomial/Eval/Defs.lean,Mathlib/Algebra/Polynomial/FieldDivision.lean,Mathlib/Algebra/Polynomial/Lifts.lean,Mathlib/Algebra/Polynomial/Monic.lean,Mathlib/Algebra/Polynomial/Roots.lean,Mathlib/Algebra/Quandle.lean,Mathlib/Algebra/Ring/Action/Basic.lean,Mathlib/Algebra/Ring/Action/End.lean,Mathlib/Algebra/RingQuot.lean,Mathlib/Algebra/Star/TensorProduct.lean,Mathlib/Algebra/TrivSqZeroExt.lean,Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean,Mathlib/AlgebraicGeometry/Modules/Tilde.lean,Mathlib/AlgebraicGeometry/Properties.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/Analysis/BoxIntegral/Basic.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean,Mathlib/Analysis/CStarAlgebra/Matrix.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/Deriv/Basic.lean,Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean,Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean,Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Complex/Harmonic/Analytic.lean,Mathlib/Analysis/Complex/Isometry.lean,Mathlib/Analysis/Complex/Norm.lean,Mathlib/Analysis/Complex/Polynomial/Basic.lean,Mathlib/Analysis/Complex/Trigonometric.lean,Mathlib/Analysis/Convolution.lean,Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean |
334 |
21 |
['github-actions', 'j-loreaux', 'kim-em', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot', 'tb65536'] |
tb65536 assignee:tb65536 |
0-77712 21 hours ago |
0-77729 21 hours ago |
9-63387 9 days |
| 31836 |
hanwenzhu author:hanwenzhu |
chore(MeasureTheory/IntervalIntegral): generalize fundamental theorem of calculus to `HasDerivWithinAt` instead of `HasDerivAt` |
This PR generalizes `HasDerivAt` to `HasDerivWithinAt`, and `DifferentiableAt` to `DifferentiableOn`, for the fundamental theorem of calculus for interval integrals.
I found this during trying to state a skeleton of a proof of a higher-dimensional Taylor's theorem. There, the correct assumption is something like `ContDiffOn n f [[a, b]]`, rather than `∀ x ∈ [[a, b]], ContDiffAt 𝕜 n f [[a, b]] x`, which traces back to this issue.
---
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
t-analysis
|
87/56 |
Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean,Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean,Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean,Mathlib/MeasureTheory/Measure/IntegralCharFun.lean,Mathlib/NumberTheory/AbelSummation.lean,Mathlib/NumberTheory/LSeries/SumCoeff.lean |
8 |
2 |
['github-actions', 'hanwenzhu'] |
nobody |
0-74762 20 hours ago |
0-76335 21 hours ago |
0-77189 21 hours |
| 31176 |
mcdoll author:mcdoll |
feat(Analysis): Taylor's theorem with the integral remainder |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
169/2 |
Mathlib.lean,Mathlib/Analysis/Calculus/TaylorIntegral.lean,Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean,docs/100.yaml,docs/undergrad.yaml |
5 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
0-72524 20 hours ago |
0-75776 21 hours ago |
4-2763 4 days |
| 31062 |
zcyemi author:zcyemi |
feat(Geometry/Euclidean/Similarity): add triangle similarity |
---
Add theorems about similarity of triangles.
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
279/0 |
Mathlib.lean,Mathlib/Geometry/Euclidean/Similarity.lean,Mathlib/Topology/MetricSpace/Similarity.lean |
3 |
24 |
['github-actions', 'jsm28', 'mathlib4-merge-conflict-bot', 'zcyemi'] |
jsm28 assignee:jsm28 |
0-64929 18 hours ago |
0-67769 18 hours ago |
7-67362 7 days |
| 31500 |
zcyemi author:zcyemi |
feat(Analysis/Convex/Between): add lemmas on affine independence under strict betweenness |
---
Add lemmas showing that affine independence is preserved when replacing a vertex
by a point strictly between two others, and related results for triangles.
deps:
- [ ] depends on: #31498
- [ ] depends on: #31499
|
|
101/0 |
Mathlib/Analysis/Convex/Between.lean,Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'zcyemi'] |
nobody |
0-64302 17 hours ago |
0-64303 17 hours ago |
0-64394 17 hours |
| 26388 |
jjdishere author:jjdishere |
feat(RingTheory/Perfectoid): Fontaine's theta map and the de Rham period rings |
This PR continues the work from #21564.
Original PR: https://github.com/leanprover-community/mathlib4/pull/21564
In this PR, we define Fontaine's theta map and the period ring B_dR.
---
- [x] depends on: #31298 [APIs lifting `W(O^\flat) -> O/p^n` to `W(O^\flat) -> O`]
- [x] depends on: #26386 [APIs for Frobenius]
|
t-ring-theory
t-algebra
t-number-theory
label:t-algebra$ |
324/0 |
Mathlib.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/Perfectoid/BDeRham.lean,Mathlib/RingTheory/Perfectoid/FontaineTheta.lean,docs/references.bib |
5 |
n/a |
['github-actions', 'jjdishere', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'riccardobrasca'] |
riccardobrasca assignee:riccardobrasca |
0-62972 17 hours ago |
unknown |
unknown |
| 31841 |
joelriou author:joelriou |
feat(CategoryTheory): orthogonal of a property of objects |
Let `P` be a triangulated subcategory of a pretriangulated category `C`. We show that `P.rightOrthogonal` (which consists of objects `Y` with no nonzero map `X ⟶ Y` with `X` satisfying `P`) is a triangulated. The dual result for `P.leftOrthogonal` is also obtained.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
139/0 |
Mathlib.lean,Mathlib/CategoryTheory/ObjectProperty/Orthogonal.lean,Mathlib/CategoryTheory/Triangulated/Orthogonal.lean |
3 |
1 |
['github-actions'] |
nobody |
0-58900 16 hours ago |
0-58965 16 hours ago |
0-58942 16 hours |
| 29937 |
Thmoas-Guan author:Thmoas-Guan |
feat(RingTheory): `ringKrullDim` of quotient via supportDim |
In this PR, we establish some lemma about `ringKrullDim` of quotient via lemmas of `supportDim`.
Co-authored-by: Yongle Hu @mbkybky
---
- [ ] depends on: #26219
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
290/15 |
Mathlib.lean,Mathlib/LinearAlgebra/Quotient/Basic.lean,Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean,Mathlib/RingTheory/Jacobson/Ideal.lean,Mathlib/RingTheory/KrullDimension/Module.lean,Mathlib/RingTheory/KrullDimension/Regular.lean,Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean,Mathlib/RingTheory/Support.lean |
8 |
4 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-58275 16 hours ago |
10-30914 10 days ago |
0-8336 2 hours |
| 30895 |
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).
This is a migration of #18254 to a fork.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
334/46 |
Mathlib.lean,Mathlib/CategoryTheory/Bicategory/FunctorBicategory/Oplax.lean,Mathlib/CategoryTheory/Bicategory/Modification/Oplax.lean,Mathlib/CategoryTheory/Bicategory/Modification/Pseudo.lean,Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean,Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Pseudo.lean |
6 |
12 |
['callesonne', 'github-actions', 'joelriou', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
joelriou assignee:joelriou |
0-57633 16 hours ago |
9-45913 9 days ago |
19-38010 19 days |
| 30236 |
luigi-massacci author:luigi-massacci |
feat(Analysis/Distribution/ContDiffMapSupportedIn): add withSeminorms statement |
Add `withSeminorms` instance to `ContDiffMapSupportedIn`, where the seminorm familiy is given by the sup-norm on the i-th derivative.
Co-authored by: @ADedecker
---
- [x] depends on: #30202
- [x] depends on: #30201
- [x] depends on: #30199
- [x] depends on: #30198
- [x] depends on: #30197
[](https://gitpod.io/from-referrer/)
|
t-analysis |
144/14 |
Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean |
1 |
12 |
['ADedecker', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-56457 15 hours ago |
2-9057 2 days ago |
2-31689 2 days |
| 31294 |
erdOne author:erdOne |
feat(Analysis): Weierstrass ℘ functions |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
274/0 |
Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean |
2 |
3 |
['github-actions', 'grunweg', 'mathlib4-merge-conflict-bot'] |
urkud assignee:urkud |
0-55685 15 hours ago |
1-58091 1 day ago |
15-22059 15 days |
| 31358 |
erdOne author:erdOne |
feat(RingTheory): universal factorization map of polynomials |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
229/0 |
Mathlib.lean,Mathlib/Algebra/Polynomial/Monic.lean,Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean,Mathlib/RingTheory/TensorProduct/Maps.lean |
4 |
4 |
['github-actions', 'jcommelin', 'mathlib4-merge-conflict-bot'] |
dwrensha assignee:dwrensha |
0-51814 14 hours ago |
0-52591 14 hours ago |
11-34685 11 days |
| 31449 |
kim-em author:kim-em |
feat(SemilocallySimplyConnected): definition and alternative formulation |
Note: Proofs in this PR were developed with assistance from Claude. |
|
114/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/SemilocallySimplyConnected.lean,Mathlib/Topology/Path.lean |
3 |
3 |
['ADedecker', 'github-actions', 'mathlib4-merge-conflict-bot'] |
ADedecker assignee:ADedecker |
0-51531 14 hours ago |
0-84731 23 hours ago |
10-35690 10 days |
| 31455 |
kim-em author:kim-em |
feat: products of locally contractible spaces |
---
- [ ] depends on: #31453
- [x] depends on: #31454
Note: Proofs in this PR were developed with assistance from Claude. |
t-topology |
31/10 |
Mathlib/Topology/Homotopy/LocallyContractible.lean |
1 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-51332 14 hours ago |
0-85019 23 hours ago |
4-38169 4 days |
| 31561 |
EtienneC30 author:EtienneC30 |
feat: monotonicity of Holderianity |
Prove many results related to the following two:
- If a function is `r`-Hölder over a bounded space, then it is also `s`-Hölder when `s ≤ r`.
- If a function is `r`-Hölder and `t`-Hölder, then it is `s`-Hölder for `r ≤ s ≤ t`.
---
- [ ] depends on: #31555
[](https://gitpod.io/from-referrer/)
|
t-topology |
75/0 |
Mathlib/Topology/MetricSpace/HolderNorm.lean |
1 |
5 |
['ADedecker', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
ADedecker assignee:ADedecker |
0-50419 14 hours ago |
3-16496 3 days ago |
0-62487 17 hours |
| 29969 |
smmercuri author:smmercuri |
refactor: use isometry extensions for completions at infinite places of number fields |
The API for `InfinitePlace.Completion` currently makes use of abstract results defined on absolute values, which all depend on the hypothesis of the form `∀ x, ‖f x‖ = v x`. This is equivalent to `f` being an isometry, and so many of these results can be bypassed and deprecated by using `Isometry.completion_extension`
---
[](https://gitpod.io/from-referrer/)
|
|
73/48 |
Mathlib/Analysis/Normed/Field/WithAbs.lean,Mathlib/NumberTheory/NumberField/AdeleRing.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean,Mathlib/Topology/MetricSpace/Completion.lean |
4 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
TwoFX assignee:TwoFX |
0-50326 13 hours ago |
31-61404 1 month ago |
54-84266 54 days |
| 31571 |
erdOne author:erdOne |
feat(RingTheory): existence of local algebra with given residue field |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
225/0 |
Mathlib.lean,Mathlib/RingTheory/LocalRing/SeparableResidueField.lean |
2 |
3 |
['github-actions', 'jcommelin', 'mathlib4-merge-conflict-bot'] |
chrisflav assignee:chrisflav |
0-50228 13 hours ago |
0-50247 13 hours ago |
7-3239 7 days |
| 31219 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): lemma about `IsBaseChange` under exact sequence |
In this lemma, we proved cokernel preserve `IsBaseChange S` and kernel preserve `IsBaseChange S` when `S` is flat.
Co-authored-by: Wang Jingting
---
[](https://gitpod.io/from-referrer/)
|
|
104/0 |
Mathlib.lean,Mathlib/RingTheory/Flat/IsBaseChange.lean |
2 |
6 |
['Thmoas-Guan', 'github-actions', 'mathlib4-merge-conflict-bot', 'urkud'] |
nobody |
0-47213 13 hours ago |
0-47749 13 hours ago |
14-48517 14 days |
| 31846 |
smmercuri author:smmercuri |
feat: `RingEquiv.restrict` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
13/0 |
Mathlib/Algebra/Ring/Subring/Basic.lean |
1 |
1 |
['github-actions'] |
nobody |
0-46452 12 hours ago |
0-46452 12 hours ago |
0-46491 12 hours |
| 31845 |
smmercuri author:smmercuri |
feat: `UniformSpace.Completion.mapRingEquiv` |
lifts a ring isomorphism between uniform rings to a ring isomorphism between their uniform space completions
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
14/4 |
Mathlib/Topology/Algebra/UniformRing.lean |
1 |
1 |
['github-actions'] |
nobody |
0-46212 12 hours ago |
0-47328 13 hours ago |
0-47370 13 hours |
| 30833 |
kckennylau author:kckennylau |
feat(Data): IsScalarTower for ZMod |
---
[](https://gitpod.io/from-referrer/)
|
t-data |
28/0 |
Mathlib/Algebra/Algebra/ZMod.lean,Mathlib/Data/ZMod/Basic.lean |
2 |
10 |
['erdOne', 'github-actions', 'kckennylau', 'leanprover-bot', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
0-45981 12 hours ago |
16-39921 16 days ago |
11-65110 11 days |
| 29362 |
stepanholub author:stepanholub |
feat(Data/List): period of a lists; prove the Periodicity Lemma |
Add the concept of the period of a List (word, sequence) which is missing, and prove its basic nontrivial property describing under which conditions list can have two periods known as the Periodicity Lemma (aka Fine-Wilf Theorem).
---
|
t-data
new-contributor
|
7127/0 |
Mathlib.lean,Mathlib/Data/List/PeriodicityLemma.lean |
2 |
126 |
['Ruben-VandeVelde', 'Timeroot', 'fpvandoorn', 'github-actions', 'madvorak', 'mathlib4-merge-conflict-bot', 'plp127', 'stepanholub', 'wwylele'] |
pechersky assignee:pechersky |
0-45905 12 hours ago |
1-57172 1 day ago |
75-13566 75 days |
| 26039 |
tsuki8 author:tsuki8 |
feat(RingTheory/MvPolynomial/{MonomialOrder,Ideal}): leadingTerm |
define the leadingTerm and prove some lemmas related to the def
`leadingTerm`: the leading term of `f` for the monomial ordering `m`
some basic lemmas about leadingTerm including:
1. `leadingTerm_eq_zero_iff`
2. `leadingTerm_image_sdiff_singleton_zero`
3. `leadingTerm_image_insert_zero`
4. `leadingTerm_zero`
5. `leadingTerm_degree_eq`
6. `leadingTerm_degree_eq'`
some lemmas about the degree of `f - m.leadingTerm f`:
1. `degree_sub_leadingTerm`
2. `degree_sub_leadingTerm_lt_degree`
3. `degree_sub_leadingTerm_lt_iff`
also some lemmas about leading terms and ideals：
1. `span_leadingTerm_sdiff_singleton_zero`
2. `span_leadingTerm_insert_zero`
3. `span_leadingTerm_eq_span_monomial`
4. `span_leadingTerm_eq_span_monomial'`
Co-authored-by: Junyu Guo @Hagb
---
- [x] depends on: #24361
- [x] depends on: #26148
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
new-contributor
|
150/1 |
Mathlib/RingTheory/MvPolynomial/Ideal.lean,Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean |
2 |
51 |
['Hagb', 'chrisflav', 'dagurtomas', 'erdOne', 'github-actions', 'kim-em', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
chrisflav assignee:chrisflav |
0-45003 12 hours ago |
0-45011 12 hours ago |
31-21918 31 days |
| 31707 |
Thmoas-Guan author:Thmoas-Guan |
feat(Homology): map between `Ext` induced by exact functor |
In this PR, we developed the additive map `Ext(M,N) => Ext(F(M), F(N))` when `F` is exact functor between abelian category. We also developed its linear version when `F` is linear.
Co-authored-by: Wang Jingting
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
183/0 |
Mathlib.lean,Mathlib/Algebra/Homology/DerivedCategory/ExactFunctor.lean,Mathlib/Algebra/Homology/DerivedCategory/Ext/Map.lean,Mathlib/Algebra/Homology/HomotopyCategory.lean |
4 |
18 |
['Thmoas-Guan', 'github-actions', 'joelriou', 'mathlib4-merge-conflict-bot'] |
nobody |
0-44933 12 hours ago |
0-44954 12 hours ago |
2-82227 2 days |
| 31803 |
grunweg author:grunweg |
chore(Tactic/Linters): remove `public section` |
Mostly as a learning exercise for me to understand the module system better.
---
- [x] depends on: #31823 (to make visibility changes just for tests a conscious choice)
[](https://gitpod.io/from-referrer/)
|
t-linter |
104/92 |
Mathlib/Tactic/Linter/CommandRanges.lean,Mathlib/Tactic/Linter/CommandStart.lean,Mathlib/Tactic/Linter/DeprecatedModule.lean,Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean,Mathlib/Tactic/Linter/DocPrime.lean,Mathlib/Tactic/Linter/DocString.lean,Mathlib/Tactic/Linter/FindDeprecations.lean,Mathlib/Tactic/Linter/FlexibleLinter.lean,Mathlib/Tactic/Linter/GlobalAttributeIn.lean,Mathlib/Tactic/Linter/HashCommandLinter.lean,Mathlib/Tactic/Linter/HaveLetLinter.lean,Mathlib/Tactic/Linter/Header.lean,Mathlib/Tactic/Linter/Lint.lean,Mathlib/Tactic/Linter/MinImports.lean,Mathlib/Tactic/Linter/Multigoal.lean,Mathlib/Tactic/Linter/OldObtain.lean,Mathlib/Tactic/Linter/PPRoundtrip.lean,Mathlib/Tactic/Linter/Style.lean,Mathlib/Tactic/Linter/TextBased.lean,Mathlib/Tactic/Linter/UnusedTactic.lean,Mathlib/Tactic/Linter/UnusedTacticExtension.lean,Mathlib/Tactic/Linter/UpstreamableDecl.lean |
23 |
10 |
['github-actions', 'grunweg', 'leanprover-bot', 'leanprover-radar', 'mathlib4-dependent-issues-bot'] |
nobody |
0-43153 11 hours ago |
0-43155 11 hours ago |
1-18055 1 day |
| 30755 |
joelriou author:joelriou |
feat(CategoryTheory): presentable objects form a dense subcategory |
In a `κ`-accessible category `C`, `isCardinalPresentable C κ` is a dense subcategory.
WIP
---
- [ ] depends on: #30464
- [ ] depends on: #30459
- [ ] depends on: #29565
- [ ] depends on: #30269
- [x] depends on: #29556
- [ ] depends on: #29519
- [ ] depends on: #29543
- [ ] depends on: #29854
- [ ] depends on: #29881
- [x] depends on: #29903
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
1829/548 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/AB.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean,Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean,Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean,Mathlib/CategoryTheory/Generator/Basic.lean,Mathlib/CategoryTheory/Generator/HomologicalComplex.lean,Mathlib/CategoryTheory/Generator/Indization.lean,Mathlib/CategoryTheory/Generator/Preadditive.lean,Mathlib/CategoryTheory/Generator/Presheaf.lean,Mathlib/CategoryTheory/Generator/Sheaf.lean,Mathlib/CategoryTheory/Generator/StrongGenerator.lean,Mathlib/CategoryTheory/Limits/FullSubcategory.lean,Mathlib/CategoryTheory/Limits/Indization/Category.lean,Mathlib/CategoryTheory/Limits/Indization/Equalizers.lean,Mathlib/CategoryTheory/Limits/MorphismProperty.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean,Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean,Mathlib/CategoryTheory/ObjectProperty/ColimitsOfShape.lean,Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean,Mathlib/CategoryTheory/ObjectProperty/LimitsClosure.lean,Mathlib/CategoryTheory/ObjectProperty/LimitsOfShape.lean,Mathlib/CategoryTheory/ObjectProperty/Retract.lean,Mathlib/CategoryTheory/ObjectProperty/Small.lean,Mathlib/CategoryTheory/Presentable/Basic.lean,Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean,Mathlib/CategoryTheory/Presentable/Dense.lean,Mathlib/CategoryTheory/Presentable/LocallyPresentable.lean,Mathlib/CategoryTheory/Presentable/Retracts.lean,Mathlib/CategoryTheory/Subobject/MonoOver.lean |
33 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-42598 11 hours ago |
unknown |
unknown |
| 30507 |
joelriou author:joelriou |
feat(CategoryTheory): MorphismProperty.isLocal is closed under `κ`-filtered colimits |
... when the domains and codomains of the `MorphismProperty` are `κ`-presentable.
(We also show that it is always closed under all limits.)
---
- [x] depends on: #29881
- [x] depends on: #30492
- [x] depends on: #30472
- [ ] depends on: #30464
- [ ] depends on: #30459
- [ ] depends on: #29565
- [x] depends on: #30269
- [x] depends on: #29556
- [x] depends on: #29519
- [ ] depends on: #29543
- [x] depends on: #29854
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
432/85 |
Mathlib.lean,Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean,Mathlib/CategoryTheory/Limits/Presentation.lean,Mathlib/CategoryTheory/ObjectProperty/Local.lean,Mathlib/CategoryTheory/ObjectProperty/Retract.lean,Mathlib/CategoryTheory/Presentable/Basic.lean,Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean,Mathlib/CategoryTheory/Presentable/LocallyPresentable.lean,Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean,Mathlib/CategoryTheory/Presentable/Retracts.lean |
10 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-42557 11 hours ago |
12-13435 12 days ago |
0-1 1 second |
| 31806 |
ADedecker author:ADedecker |
feat: endow test functions with the natural LF topology |
This code comes from #30325 by @luigi-massacci, who is the main author of this file. I am just opening another stream of PRs in order to parallelize the review work, and adding some touches along the way.
Co-authored-by: @luigi-massacci
---
- [x] depends on: #31533
[](https://gitpod.io/from-referrer/)
|
t-analysis |
113/5 |
Mathlib/Analysis/Distribution/TestFunction.lean |
1 |
3 |
['ADedecker', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-41531 11 hours ago |
0-47492 13 hours ago |
0-47535 13 hours |
| 31706 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra/ModuleCat): `ModuleCat.uliftFunctor` |
Add `ModuleCat.uliftFunctor`
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
104/0 |
Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Ulift.lean |
2 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
0-41249 11 hours ago |
0-41268 11 hours ago |
3-29721 3 days |
| 30533 |
joelriou author:joelriou |
feat(CategoryTheory): presentable objects and adjunctions |
If `adj : F ⊣ G` and `G` is `κ`-accessible for a regular cardinal `κ`, then `F` preserves `κ`-presentable objects.
Moreover, if `G : D ⥤ C` is fully faithful, then `D` is locally `κ`-presentable (resp `κ`-accessible) if `D` is.
---
- [ ] depends on: #30464
- [ ] depends on: #30459
- [ ] depends on: #29565
- [x] depends on: #30269
- [x] depends on: #29556
- [x] depends on: #29519
- [x] depends on: #29543
- [x] depends on: #29854
- [x] depends on: #29881
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
576/88 |
Mathlib.lean,Mathlib/CategoryTheory/Adjunction/Basic.lean,Mathlib/CategoryTheory/Adjunction/ReflectiveLimits.lean,Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean,Mathlib/CategoryTheory/ObjectProperty/Retract.lean,Mathlib/CategoryTheory/ObjectProperty/Small.lean,Mathlib/CategoryTheory/Presentable/Adjunction.lean,Mathlib/CategoryTheory/Presentable/Basic.lean,Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean,Mathlib/CategoryTheory/Presentable/LocallyPresentable.lean,Mathlib/CategoryTheory/Presentable/Retracts.lean |
11 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-40774 11 hours ago |
12-13787 12 days ago |
0-1 1 second |
| 31850 |
jsm28 author:jsm28 |
refactor(Geometry/Euclidean/Sphere/Tangent): split out `orthRadius` |
Split the definition and lemmas for `orthRadius` out of `Mathlib.Geometry.Euclidean.Sphere.Tangent` into a separate `Mathlib.Geometry.Euclidean.Sphere.OrthRadius`, in preparation for setting up a further `Mathlib.Geometry.Euclidean.Sphere.PolePolar` (which will import `OrthRadius` and be imported by `Tangent`).
There are no changes to definitions, statements or proofs. The doc string for `orthRadius` (and corresponding description in the module doc string) is updated to reflect that this definition is not just useful at points on the sphere to define tangents but also more generally for defining polars.
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
129/92 |
Mathlib.lean,Mathlib/Geometry/Euclidean/Sphere/OrthRadius.lean,Mathlib/Geometry/Euclidean/Sphere/Tangent.lean |
3 |
1 |
['github-actions'] |
nobody |
0-39745 11 hours ago |
0-39808 11 hours ago |
0-39784 11 hours |
| 31733 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Incenter): `orthRadius` lemmas |
Add lemmas, in the case where the dimensions are such that the simplex spans the whole space, exspheres are not merely tangent to the faces but the faces are the full tangent spaces (`orthRadius`).
---
- [ ] depends on: #31727
- [ ] depends on: #31728
- [ ] depends on: #31731
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
101/0 |
Mathlib/Geometry/Euclidean/Incenter.lean,Mathlib/Geometry/Euclidean/Sphere/Tangent.lean |
2 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-39329 10 hours ago |
1-54295 1 day ago |
0-862 14 minutes |
| 31810 |
xroblot author:xroblot |
chore(TotallyReal/TotallyComplex): remove the `NumberField` hypothesis |
We remove the`NumberField` hypothesis in the definitions and most of the results. In general, it can be replaced by the hypothesis that the field is of characteristic zero and some integrality hypothesis.
---
[](https://gitpod.io/from-referrer/)
|
t-number-theory |
66/33 |
Mathlib/NumberTheory/NumberField/CMField.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean |
2 |
2 |
['github-actions', 'jcommelin'] |
nobody |
0-38145 10 hours ago |
1-31832 1 day ago |
1-31928 1 day |
| 31842 |
joelriou author:joelriou |
chore(CategoryTheory): rename LeftBousfield.W as ObjectProperty.isLocal |
This is more consistent with the dual construction `MorphismProperty.isLocal`.
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
107/78 |
Mathlib/CategoryTheory/Abelian/SerreClass/Bousfield.lean,Mathlib/CategoryTheory/Localization/Bousfield.lean,Mathlib/CategoryTheory/Localization/BousfieldTransfiniteComposition.lean,Mathlib/CategoryTheory/ObjectProperty/Local.lean,Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean,Mathlib/CategoryTheory/Sites/Equivalence.lean,Mathlib/CategoryTheory/Sites/Localization.lean,Mathlib/CategoryTheory/Sites/PreservesSheafification.lean |
8 |
3 |
['github-actions', 'jcommelin'] |
nobody |
0-37731 10 hours ago |
0-57394 15 hours ago |
0-57371 15 hours |
| 30525 |
515801431 author:515801431 |
feat(Mathlib/Combinatorics/Enumerative/Polya): Add Polya Counting |
This PR introduces basic definitions and results about colorings under permutation group actions.
A coloring is defined as a function X → Y, and the permutation group Equiv.Perm X acts on colorings by precomposition:
(g • c) x = c (g⁻¹ • x)
This formalizes the natural action of relabeling the elements of X.
Main definitions
MulAction (Equiv.Perm X) (X → Y):
The action of the permutation group on colorings via precomposition.
coloringEquiv (c₁ c₂ : X → Y) : Prop:
Two colorings are equivalent if they lie in the same orbit under this action, i.e.
∃ f : Equiv.Perm X, f • c₁ = c₂.
Main results
smul_eq_iff_mem_stabilizer:
Characterizes when two group actions on the same coloring are equal, showing that
g • c = f • c ↔ f⁻¹ * g ∈ stabilizer c.
coloringEquiv_equivalence:
Proves that coloringEquiv defines an equivalence relation on X → Y.
orbit_size_eq_index:
Reformulates the orbit–stabilizer theorem in the context of colorings:
|orbit c| = |Perm X| / |stabilizer c|
Motivation
These results provide foundational infrastructure for studying Burnside’s lemma and Pólya’s enumeration theorem in Mathlib, where the enumeration of distinct colorings up to symmetry plays a central role. |
new-contributor
t-combinatorics
|
108/0 |
Mathlib/Combinatorics/Enumerative/Polya.lean |
1 |
3 |
['IvanRenison', 'github-actions', 'mathlib4-merge-conflict-bot'] |
awainverse assignee:awainverse |
0-37675 10 hours ago |
1-41268 1 day ago |
34-27624 34 days |
| 31852 |
JovanGerb author:JovanGerb |
chore(Order/Basic): use `@[to_dual]` for `Preorder`/`PartialOrder` |
This PR tags some part of `Mathlib.Order.Basic` with `@[to_dual]`. This PR adds a lot of new declarations in cases where there used to not be a dual declaration (and even a new simp lemma `ne_iff_gt_iff_ge`).
The sections for pure `LE`/`LT`, and `LinearOrder` in this file are left to be tagged for future PRs.
---
[](https://gitpod.io/from-referrer/)
|
t-order |
67/91 |
Mathlib/Order/Basic.lean |
1 |
1 |
['github-actions'] |
bryangingechen assignee:bryangingechen |
0-36733 10 hours ago |
0-39212 10 hours ago |
0-39252 10 hours |
| 27258 |
JovanGerb author:JovanGerb |
feat: Imo2020 q6 |
Original PR: #23431
This PR adds a solution to IMO 2020 Q6. It follows the solution that I found when I was participating in the IMO. I used the statement formalization that was given by @jsm28.
---
- [x] depends on: #27257
[](https://gitpod.io/from-referrer/)
|
IMO |
335/0 |
Archive.lean,Archive/Imo/Imo2020Q6.lean |
2 |
10 |
['JovanGerb', 'dwrensha', 'github-actions', 'mathlib4-dependent-issues-bot'] |
dwrensha assignee:dwrensha |
0-35823 9 hours ago |
59-31062 1 month ago |
59-32339 59 days |
| 30736 |
alreadydone author:alreadydone |
feat(RingTheory): Picard group of a domain is isomorphic to ClassGroup |
---
- [ ] depends on: #30657
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
411/115 |
Mathlib/Algebra/Algebra/Bilinear.lean,Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Data/Set/Semiring.lean,Mathlib/LinearAlgebra/Span/Defs.lean,Mathlib/RingTheory/ClassGroup.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean,Mathlib/RingTheory/FractionalIdeal/Operations.lean,Mathlib/RingTheory/Localization/Defs.lean,Mathlib/RingTheory/PicardGroup.lean,docs/references.bib |
10 |
5 |
['alreadydone', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-34922 9 hours ago |
16-34904 16 days ago |
0-1 1 second |
| 31489 |
alreadydone author:alreadydone |
feat(FieldTheory): fg extension over perfect field is separably generated |
Co-authored-by: Christian Merten
Co-authored-by: Andrew Yang
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
446/22 |
Mathlib.lean,Mathlib/FieldTheory/IntermediateField/Algebraic.lean,Mathlib/FieldTheory/Normal/Closure.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableClosure.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/FieldTheory/SeparablyGenerated.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/RingTheory/AlgebraicIndependent/Defs.lean,Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean |
11 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
riccardobrasca assignee:riccardobrasca |
0-34840 9 hours ago |
0-41494 11 hours ago |
8-80212 8 days |
| 31215 |
ScottCarnahan author:ScottCarnahan |
feat (RingTheory/HahnSeries): introduce binomialFamily and generalized powers. |
We introduce a way to take generalized powers of Hahn series whose leading term is 1. The powers take values in a binomial ring.
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
303/20 |
Mathlib.lean,Mathlib/RingTheory/HahnSeries/Addition.lean,Mathlib/RingTheory/HahnSeries/Basic.lean,Mathlib/RingTheory/HahnSeries/Binomial.lean,Mathlib/RingTheory/HahnSeries/Multiplication.lean,Mathlib/RingTheory/HahnSeries/Summable.lean |
6 |
20 |
['ScottCarnahan', 'erdOne', 'github-actions', 'mathlib4-merge-conflict-bot'] |
erdOne assignee:erdOne |
0-34424 9 hours ago |
0-34442 9 hours ago |
13-63896 13 days |
| 30989 |
kckennylau author:kckennylau |
feat(RingTheory): Teichmuller map |
Let `R` be an `I`-adically complete ring, and `p` be a prime number with `p ∈ I`. This PR constructs the Teichmüller map `Perfection (R ⧸ I) p →*₀ R` such that it composed with the quotient map `R →+* R ⧸ I` is the "0-th coefficient" map `Perfection (R ⧸ I) p →+* R ⧸ I`.
This generalises the existing [PreTilt.untilt](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Perfectoid/Untilt.html#PreTilt.untilt).
I have also moved `Mathlib/LinearAlgebra/SModEq` to a folder to be `/SModEq/Basic.lean`, because I needed to add some lemmas to `/SModEq/Prime.lean`; I also added a lemma to the end of `/Basic.lean` called `ideal`.
---
In order to try to artificially minimise the diff count, I have made #30990 which only moves the file `SModEq`.
- [x] depends on: #30990
- [x] depends on: #31193
- [x] depends on: #31195
[](https://gitpod.io/from-referrer/)
|
|
207/112 |
Mathlib.lean,Mathlib/LinearAlgebra/SModEq/Basic.lean,Mathlib/LinearAlgebra/SModEq/Prime.lean,Mathlib/RingTheory/Perfectoid/Untilt.lean,Mathlib/RingTheory/Teichmuller.lean |
5 |
33 |
['erdOne', 'github-actions', 'kbuzzard', 'kckennylau', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'pechersky'] |
nobody |
0-32872 9 hours ago |
0-46142 12 hours ago |
16-61617 16 days |
| 31152 |
FernandoChu author:FernandoChu |
feat(CategoryTheory): regular categories have strong-epi-mono factorisations |
This PR defines regular categories and shows that these have strong-epi-mono factorisations. A follow up PR will prove frobenius reciprocity.
- [x] depends on: https://github.com/leanprover-community/mathlib4/pull/31145
---
This is a prerequisite of the [MTT project](https://github.com/kyoDralliam/model-theory-topos), which aims to use the internal language of toposes to reason about e.g. sheaves. |
t-category-theory |
223/0 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean,Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean,Mathlib/CategoryTheory/RegularCategory/Basic.lean,docs/references.bib |
5 |
14 |
['FernandoChu', 'dagurtomas', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
dagurtomas assignee:dagurtomas |
0-32859 9 hours ago |
0-60211 16 hours ago |
1-34133 1 day |
| 31688 |
themathqueen author:themathqueen |
feat(LinearAlgebra/Eigenspace): `mem_eigenspace_intrinsicStar_iff` and `spectrum_intrinsicStar` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
54/1 |
Mathlib.lean,Mathlib/Algebra/Star/LinearMap.lean,Mathlib/LinearAlgebra/Eigenspace/IntrinsicStar.lean |
3 |
2 |
['github-actions', 'themathqueen'] |
nobody |
0-32791 9 hours ago |
4-64896 4 days ago |
4-64932 4 days |
| 30936 |
themathqueen author:themathqueen |
feat(Data/Int): define `Int.fib`, the Fibonacci numbers on the integers |
We define `Int.fib`, the integer version of `Nat.fib`, which satisfies `Int.fib 0 = 0`, `Int.fib 1 = 1`, and `Int.fib (n + 2) = Int.fib n + Int.fib (n + 1)`.
---
[](https://gitpod.io/from-referrer/)
|
t-data |
175/0 |
Mathlib.lean,Mathlib/Data/Int/Fib.lean |
2 |
12 |
['Ruben-VandeVelde', 'github-actions', 'mathlib4-merge-conflict-bot', 'themathqueen', 'vihdzp'] |
nobody |
0-32746 9 hours ago |
1-58697 1 day ago |
25-28949 25 days |
| 30882 |
themathqueen author:themathqueen |
feat(Data/Nat/Fib): the Cassini and Catalan identities |
The [Cassini and Catalan identities](https://en.wikipedia.org/wiki/Cassini_and_Catalan_identities) are identities for the Fibonacci numbers.
* Cassini's identity: `fib (n + 1) * fib (n - 1) - fib n ^ 2 = (-1) ^ n` for nonzero `n`.
* Catalan's identity: `fib (x + a) ^ 2 - fib (x + 2 * a) * fib x = fib a ^ 2 * (-1) ^ x` for nonzero `x` and `a`.
---
[](https://gitpod.io/from-referrer/)
|
t-data
t-algebra
label:t-algebra$ |
92/0 |
Mathlib.lean,Mathlib/Data/Matrix/Basic.lean,Mathlib/Data/Nat/Fib/Lemmas.lean |
3 |
16 |
['github-actions', 'jcommelin', 'mathlib4-merge-conflict-bot', 'themathqueen', 'vihdzp'] |
nobody |
0-32725 9 hours ago |
1-58592 1 day ago |
25-82012 25 days |
| 30880 |
themathqueen author:themathqueen |
feat(Analysis/InnerProductSpace): finite-dimensional inner product space with coalgebra implies an algebra structure |
A finite-dimensional inner product space with a coalgebra structure also has an algebra structure by taking adjoints of the comultiplication map and counit map, i.e., `x * y = (adjoint comul) (x ⊗ₜ y)` and `algebraMap = adjoint counit`.
There is also the opposite implication, i.e., a finite-dimensional inner product space with an algebra structure implies a coalgebra where `counit = adjoint Algebra.linearMap` and `comul = adjoint mul'`.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
158/0 |
Mathlib.lean,Mathlib/Analysis/InnerProductSpace/Coalgebra.lean,Mathlib/Analysis/InnerProductSpace/TensorProduct.lean |
3 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
urkud assignee:urkud |
0-32711 9 hours ago |
1-58481 1 day ago |
26-47306 26 days |
| 28100 |
themathqueen author:themathqueen |
feat(LinearAlgebra/GeneralLinearGroup): algebra automorphisms in endomorphisms are inner |
Characterization of automorphisms in endomorphisms of vector spaces: for any algebra automorphism `f : End R V ≃ₐ[R] End R V`, there exists a linear isomorphism `T` such that `f a = T.conj a = T ∘ a ∘ T.symm` for all `a`. This does not suppose finite-dimensionality.
Also adds an instance for `Algebra.IsCentral K (Module.End K V)`.
---
Technically used Aristotle for showing that `T` is injective (out of curiosity) :) (added as co-author)
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
130/3 |
Mathlib.lean,Mathlib/Algebra/Central/End.lean,Mathlib/FieldTheory/SplittingField/Construction.lean,Mathlib/LinearAlgebra/FreeModule/Basic.lean,Mathlib/LinearAlgebra/FreeModule/Norm.lean,Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean,Mathlib/RingTheory/LocalRing/Module.lean |
7 |
42 |
['Whysoserioushah', 'eric-wieser', 'github-actions', 'hrmacbeth', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
Vierkantor assignee:Vierkantor |
0-32655 9 hours ago |
1-59068 1 day ago |
53-51226 53 days |
| 27493 |
themathqueen author:themathqueen |
feat(RingTheory/Coalgebra): define Frobenius algebra |
A Frobenius algebra `A` has the structure of both an algebra and a coalgebra such that:
`(mul ⊗ id) ∘ assoc.symm ∘ (id ⊗ comul) = comul ∘ mul = (id ⊗ mul) ∘ assoc ∘ (comul ⊗ id)`.
In diagrams this law looks like:
It suffices to show that
`(mul ⊗ id) ∘ assoc.symm ∘ (id ⊗ comul) = (id ⊗ mul) ∘ assoc ∘ (comul ⊗ id)`
(the proof of this is ugly).
---
- [x] depends on: #27567
- [x] depends on: #27569
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
163/0 |
Mathlib.lean,Mathlib/RingTheory/Coalgebra/Frobenius.lean |
2 |
12 |
['YaelDillies', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
alreadydone assignee:alreadydone |
0-32633 9 hours ago |
1-59786 1 day ago |
21-60429 21 days |
| 31588 |
joelriou author:joelriou |
feat(CategoryTheory/ComposableArrows): compositions of 1 or 2 morphisms |
---
- [x] depends on: #31584
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-category-theory
|
112/0 |
Mathlib.lean,Mathlib/CategoryTheory/ComposableArrows/One.lean,Mathlib/CategoryTheory/ComposableArrows/Two.lean |
3 |
10 |
['dagurtomas', 'github-actions', 'joelriou', 'kim-em', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-32575 9 hours ago |
0-69314 19 hours ago |
3-58960 3 days |
| 31817 |
kckennylau author:kckennylau |
chore: remove extra monic hypotheses from divByMonic and modByMonic lemmas |
---
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/modByMonic_add_div/with/556964888)
[](https://gitpod.io/from-referrer/)
|
t-ring-theory
t-algebra
label:t-algebra$ |
85/88 |
Mathlib/Algebra/Polynomial/CoeffMem.lean,Mathlib/Algebra/Polynomial/Div.lean,Mathlib/Algebra/Polynomial/FieldDivision.lean,Mathlib/Algebra/Polynomial/PartialFractions.lean,Mathlib/Algebra/Polynomial/RingDivision.lean,Mathlib/FieldTheory/Minpoly/Basic.lean,Mathlib/FieldTheory/Minpoly/Field.lean,Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean,Mathlib/LinearAlgebra/Charpoly/Basic.lean,Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean,Mathlib/RingTheory/Adjoin/PowerBasis.lean,Mathlib/RingTheory/AdjoinRoot.lean,Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean,Mathlib/RingTheory/IntegralDomain.lean,Mathlib/RingTheory/IsAdjoinRoot.lean,Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean,Mathlib/RingTheory/Polynomial/Nilpotent.lean,Mathlib/RingTheory/PowerBasis.lean,Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean,Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean |
20 |
11 |
['artie2000', 'github-actions', 'kbuzzard', 'kckennylau'] |
jcommelin assignee:jcommelin |
0-31543 8 hours ago |
0-31543 8 hours ago |
1-13248 1 day |
| 31859 |
joelriou author:joelriou |
feat(CategoryTheory/Sites): points of a site |
The main definition in this PR is `GrothendieckTopology.Point` which is a notion of point for a site `(C, J)` where `J` is a Grothendieck topology on a category `C`. The main data in a point consists in a functor `fiber : C ⥤ Type w` (e.g. if `S` is a scheme, `s` a geometry point of `S`, and `C` is the category of étale schemes over `S`, `fiber` could be the functor which sends an étale scheme `X` over `S` to the geometric fiber `X(s)`). One of the important condition on `fiber` is that it is a type-valued flat functor (which means that the category of elements of this functor is cofiltered): we show that when `C` has finite limits, it suffices to check that the functor commutes with finite limits.
The properties of the fiber functors on categories of presheaves and sheaves attached to a point of a site will be studied further in #31710.
---
In another draft branch, it is shown that a point of a topological space gives a point of the associated site https://github.com/joelriou/mathlib4/blob/fiber-functor/Mathlib/Topology/Sheaves/Point.lean
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
206/3 |
Mathlib.lean,Mathlib/CategoryTheory/Elements.lean,Mathlib/CategoryTheory/Functor/Flat.lean,Mathlib/CategoryTheory/Functor/TypeValuedFlat.lean,Mathlib/CategoryTheory/Limits/FunctorCategory/Finite.lean,Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean,Mathlib/CategoryTheory/Sites/Limits.lean,Mathlib/CategoryTheory/Sites/Point/Basic.lean,Mathlib/CategoryTheory/Sites/Sheaf.lean,Mathlib/CategoryTheory/Sites/Sheafification.lean |
10 |
2 |
['github-actions'] |
nobody |
0-30886 8 hours ago |
0-34429 9 hours ago |
0-1 1 second |
| 31713 |
jsm28 author:jsm28 |
feat(Geometry/Euclidean/Angle/Oriented/Affine): equal angles between parallel lines |
We have an existing lemma that angles are equal mod π when corresponding lines in those angles are parallel. Add a stronger lemma giving equality mod 2π when all four endpoints of the angles lie on the same line (excluding the degenerate case of collinear points where it's possible one angle is 0 and the other is π).
---
- [ ] depends on: #31712
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry |
57/0 |
Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
0-30849 8 hours ago |
4-21951 4 days ago |
0-1767 29 minutes |
| 31274 |
joelriou author:joelriou |
feat(AlgebraicTopology): edges and "triangles" in the nerve of a category |
We study `Edge` and `Edge.CompStruct` in the case of the nerve of a category. In particular, `Edge.CompStruct` are related to commutative triangles.
---
- [x] depends on: #31254
- [x] depends on: #31265
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology |
189/22 |
Mathlib/AlgebraicTopology/SimplicialNerve.lean,Mathlib/AlgebraicTopology/SimplicialSet/CompStruct.lean,Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean,Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean,Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean,Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean,Mathlib/CategoryTheory/ComposableArrows/Basic.lean |
7 |
7 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-27067 7 hours ago |
1-24292 1 day ago |
5-40611 5 days |
| 24912 |
YaelDillies author:YaelDillies |
feat: affine monoids |
Define affine monoids as finitely generated cancellative torsion-free commutative monoids and prove a few of their basic properties:
* An affine monoid with no non-trivial unit is generated by its irreducible elements
* An affine monoid embeds into `ℤⁿ` for some `n`
* Let `M` be an affine monoid. If `R` is a domain, then so is `R[M]`.
From Toric
Co-authored-by: Patrick Luo
---
- [x] depends on: #24913
- [x] depends on: #24914
- [ ] depends on: #26110
[](https://gitpod.io/from-referrer/)
|
toric
t-algebra
label:t-algebra$ |
214/0 |
Mathlib.lean,Mathlib/Algebra/AffineMonoid/Basic.lean,Mathlib/Algebra/AffineMonoid/Embedding.lean,Mathlib/Algebra/AffineMonoid/Irreducible.lean,Mathlib/Algebra/AffineMonoid/UniqueSums.lean |
5 |
16 |
['YaelDillies', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'smorel394'] |
nobody |
0-25415 7 hours ago |
1-50629 1 day ago |
7-26907 7 days |
| 25797 |
dagurtomas author:dagurtomas |
feat(Condensed): closed symmetric monoidal structure on light condensed modules |
---
- [x] depends on: #31750
- [x] depends on: #31345
- [x] depends on: #25794
- [x] depends on: #24490
- [x] depends on: #24522
[](https://gitpod.io/from-referrer/)
---
*This PR continues the work from #24523.*
*Original PR: https://github.com/leanprover-community/mathlib4/pull/24523* |
t-condensed |
80/2 |
Mathlib.lean,Mathlib/CategoryTheory/Equivalence.lean,Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean,Mathlib/Condensed/Light/Monoidal.lean |
4 |
8 |
['github-actions', 'joelriou', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-24167 6 hours ago |
1-34287 1 day ago |
3-3359 3 days |
| 31854 |
erdOne author:erdOne |
chore(AlgebraicGeometry): API for `𝒪ₓ`-modules |
---
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry |
475/15 |
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean,Mathlib/Algebra/Category/ModuleCat/Sheaf/Colimits.lean,Mathlib/Algebra/Category/ModuleCat/Sheaf/PullbackContinuous.lean,Mathlib/Algebra/Category/ModuleCat/Sheaf/PushforwardContinuous.lean,Mathlib/AlgebraicGeometry/Modules/Sheaf.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean |
8 |
3 |
['erdOne', 'github-actions', 'joelriou'] |
nobody |
0-24121 6 hours ago |
0-34936 9 hours ago |
0-34959 9 hours |
| 31819 |
j-loreaux author:j-loreaux |
perf: de-instance some WithLp norm structures used for type synonyms |
The recent refactor of `WithLp` into a one-field structure caused an unexpected slowdown in completely unrelated files. Some sleuthing by @kbuzzard revealed that this was caused by Lean performing unification on some new instances which are only intended for type synonyms.
Because these are only intended for synonyms, we de-instance them here, and they can be copied over when a user creates a synonym.
During the investigation, we also uncovered that one of the statements (`normSMulClassSeminormedAddCommGroupToProd`) for the `Prod` synonyms was using the wrong norm, and Lean had secretly elaborated the statement using `Prod.toNorm` instead. We fix this error and prevent stray elaboration by locally disabling the usual `Prod`/`Pi` norm instances.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
24/10 |
Mathlib/Analysis/Matrix/Normed.lean,Mathlib/Analysis/Normed/Lp/PiLp.lean,Mathlib/Analysis/Normed/Lp/ProdLp.lean |
3 |
9 |
['github-actions', 'grunweg', 'j-loreaux', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'leanprover-radar', 'mcdoll', 'ocfnash'] |
nobody |
0-21298 5 hours ago |
0-70890 19 hours ago |
0-82842 23 hours |
| 31634 |
wwylele author:wwylele |
feat(Algebra/Polynomial): misc lemma about mod |
Added the following
- `degree_mod_lt`, `add_mod`, `sub_mod`, `mod_eq_of_dvd_sub`: corresponding to existing lemma on `modByMonic`
- `mul_mod`, `mul_modByMonic`: similar to [Nat.mul_mod](https://leanprover-community.github.io/mathlib4_docs/Init/Data/Nat/Lemmas.html#Nat.mul_mod)
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebra
label:t-algebra$ |
34/0 |
Mathlib/Algebra/Polynomial/Div.lean,Mathlib/Algebra/Polynomial/FieldDivision.lean |
2 |
2 |
['Ruben-VandeVelde', 'github-actions'] |
erdOne assignee:erdOne |
0-18789 5 hours ago |
0-18789 5 hours ago |
6-20061 6 days |
| 31548 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(Analysis/Convex/Quasiconvex): properties of quasiconcave functions |
Prove properties of quasiconcave/quasiconvex functions:
* monotony
* restriction
* connectedness of preimages
Co-authored with: @ADedecker
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
107/1 |
Mathlib/Analysis/Convex/Quasiconvex.lean,Mathlib/Data/Set/Basic.lean |
2 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
0-17615 4 hours ago |
1-54592 1 day ago |
6-74848 6 days |
| 27107 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(GroupTheory/GroupAction/SubMulAction/Combination): combinations and group actions |
`Nat.Combination X n` is the type all `s : Finset X` such that `s.card = n`.
This PR provides some API for this subtype and the `SubMulAction` it inherits when a group acts on `X`.
It will be used in conjunction with the description of some maximal subgroups of `Equiv.Perm X` to construct primitive actions.
Question on the names: when `X` is a fintype, there is `Finset.powersetCard` that gives the same object, as a `Finset`. But the present PR also applies when `X` is infinite. Then maybe `Nat.Combination` should be renamed as `Set.powersetCard`?
---
[](https://gitpod.io/from-referrer/)
|
t-group-theory |
338/0 |
Mathlib.lean,Mathlib/Data/Fintype/EquivFin.lean,Mathlib/Data/Nat/Choose/Basic.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean |
4 |
41 |
['AntoineChambert-Loir', 'alreadydone', 'github-actions', 'mathlib4-merge-conflict-bot', 'tb65536'] |
alreadydone assignee:alreadydone |
0-15480 4 hours ago |
1-58563 1 day ago |
129-29917 129 days |
| 29437 |
SnirBroshi author:SnirBroshi |
feat(Data/Seq): add Seq.subsequence and prove basic theorems about it |
I added `Seq.subsequence` to compose a sequence with a monotone function, creating a subsequence. Aliased to `Seq.comp` since it's a composition.
I also added `Nat.le_induction_step_iff` which is needed to prove a subsequence is a sequence. This proves the comment at the top of `Defs.lean` that says "if `f n = none`, then `f m = none` for all `m ≥ n`" while `IsSeq` only talks about `n+1`.
For completion I added the same statement for `Int`.
---
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
|
102/0 |
Mathlib/Data/Int/Init.lean,Mathlib/Data/Nat/Init.lean,Mathlib/Data/Seq/Basic.lean,Mathlib/Data/Seq/Defs.lean |
4 |
6 |
['SnirBroshi', 'github-actions', 'kim-em', 'mathlib4-merge-conflict-bot'] |
pechersky assignee:pechersky |
0-15453 4 hours ago |
0-15461 4 hours ago |
71-75329 71 days |
| 30757 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph/Acyclic): `singletonGraph` and `subgraphOfAdj` are trees |
---
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
30/1 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean |
3 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
kmill assignee:kmill |
0-14452 4 hours ago |
0-14476 4 hours ago |
28-61090 28 days |
| 31839 |
kim-em author:kim-em |
feat: updates to downstream repos scripts |
Adds repos, improves the output for `scripts/downstream-tags.py`, and adds flags to `scripts/downstream_dashboard.py` to we can query particular defect types. |
CI |
360/86 |
scripts/downstream-tags.py,scripts/downstream_dashboard.py,scripts/downstream_repos.yml |
3 |
1 |
['github-actions'] |
nobody |
0-14204 3 hours ago |
0-71456 19 hours ago |
0-71491 19 hours |
| 26831 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(GroupTheory/SpecificGroups/Alternating/MaximalSubgroups): maximal subgroups of the alternating group |
This proves the first case (intransitive) of the O'Nan-Scott classification of maximal subgroups of the alternating group.
---
- [x] depends on: #26457
- [x] depends on: #26282
- [x] depends on: #26281
- [x] depends on: #26280
- [x] depends on: #26279
[](https://gitpod.io/from-referrer/)
|
t-group-theory |
568/20 |
Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/Perm/MaximalSubgroups.lean,Mathlib/GroupTheory/SpecificGroups/Alternating.lean,Mathlib/GroupTheory/SpecificGroups/Alternating/MaximalSubgroups.lean |
5 |
n/a |
['AntoineChambert-Loir', 'adomani', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-13792 3 hours ago |
unknown |
unknown |
| 31858 |
euprunin author:euprunin |
chore: remove use of `erw` in `LinearAlgebra.TensorAlgebra.Basic` |
---
[](https://gitpod.io/from-referrer/)
|
tech debt
t-algebra
label:t-algebra$ |
1/1 |
Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean |
1 |
15 |
['bryangingechen', 'euprunin', 'github-actions', 'mathlib-bors', 'mattrobball'] |
nobody |
0-13483 3 hours ago |
0-26941 7 hours ago |
0-32272 8 hours |
| 31462 |
ScottCarnahan author:ScottCarnahan |
feat(Algebra/Lie/Extension): 2-cocycle from a Lie algebra extension with abelian kernel and a linear splitting |
This PR defines the Lie algebra 2-cocycle of a Lie algebra extension with abelian kernel equipped with a linear splitting.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra label:t-algebra$ |
224/13 |
Mathlib/Algebra/Lie/Abelian.lean,Mathlib/Algebra/Lie/Extension.lean |
2 |
26 |
['ScottCarnahan', 'github-actions', 'mathlib4-merge-conflict-bot', 'ocfnash'] |
ocfnash assignee:ocfnash |
0-11089 3 hours ago |
1-54612 1 day ago |
7-39209 7 days |
| 31573 |
SnirBroshi author:SnirBroshi |
feat(Combinatorics/SimpleGraph): split `Walk.lean` into 4 files |
Split into 4 files in a new `Walks` subfolder:
- `Basic.lean`: basic definitions and theorems about them, without modifying the walks: `Walk`, `Nil`, `length`, `getVert`, `support`, `darts`, `edges`, `edgeSet`, `snd`, `penultimate`, `firstDart`, `lastDart`
- `Operations.lean`: similar to the existing `WalkDecomp.lean`, this file defines operations on walks: `copy`, `append`, `concat`, `reverse`, `drop`, `take`, `tail`, `dropLast`. The name of the file matches `SimpleGraph/Operations.lean` which defines operations on graphs.
- `Maps.lean`: operations that map the walk to another graph: `map`, `mapLe`, `transfer`, `induce`, `toDeleteEdges`, `toDeleteEdge`. The name of the file matches `SimpleGraph/Maps.lean` which defines maps on graphs.
- `Subwalks.lean`: the definition of `IsSubwalk` and theorems about it
Deprecates the original `Walk.lean` module.
---
`Walk.lean` has been [around 1500 lines](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/long.20files/near/554617597) for a while, so this PR splits it into 4 files.
Fixes [this TODO](https://github.com/leanprover-community/mathlib4/blob/4055dfea0311fa984f3b4eaa629c12220ff0a03a/Mathlib/Combinatorics/SimpleGraph/Walk.lean#L36).
**What changed:**
I haven't changed any of the declarations, nor their relative order, just partitioned the contents of the original module.
But I *did* modify `namespace`/`end`/`variable`/`universe`/`open` commands, while attempting to not cause modifications to variable names/order/binder-info (can the bot verify that or does it only check name changes?).
Also I modified the module docstrings to include the definitions in each file, and a few heading comments (comments that begin with pound symbols).
I'll move the existing `Paths.lean` and `WalkDecomp.lean` to `Walks/` in a later PR, perhaps with a rename as well.
If it helps I can try to split this into 4 commits (or 4 separate PRs) doing the following in-order:
- move `Walk.lean` to `Walks/Basic.lean`
- split off a chunk to a new `Subwalks.lean`
- split off a chunk to a new `Maps.lean`
- split off a chunk to a new `Operations.lean`
I'm planning to PR a few more definitions to `Basic` soon, namely `nextDart`/`prevDart`/`containingEdge`, so if you prefer we can split `getVert`/`snd`/`penultimate`/`firstDart`/`lastDart` now to a new `Navigation.lean`, or keep it in `Basic`.
I think this split is pretty good, though it's worth noting 9 theorems are in `Operations` and not `Basic` because their proof relies on operations even though their statement doesn't:
- `support_eq_concat`
- `dart_snd_mem_support_of_mem_darts`
- `fst_mem_support_of_mem_edges`
- `snd_mem_support_of_mem_edges`
- `edges_nodup_of_support_nodup`
- `ext_support`
- `support_injective`
- `ext_getVert_le_length`
- `ext_getVert`
Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Splitting.20.60Walk.2Elean.60/
[](https://gitpod.io/from-referrer/)
|
t-combinatorics |
1593/1494 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean,Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Combinatorics/SimpleGraph/Walk.lean,Mathlib/Combinatorics/SimpleGraph/Walks/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean,Mathlib/Combinatorics/SimpleGraph/Walks/Operations.lean,Mathlib/Combinatorics/SimpleGraph/Walks/Subwalks.lean |
8 |
3 |
['github-actions', 'jt496', 'mathlib4-merge-conflict-bot'] |
bryangingechen assignee:bryangingechen |
0-10969 3 hours ago |
1-54342 1 day ago |
6-37616 6 days |
| 31865 |
euprunin author:euprunin |
fix: adjust `abel`'s `hint` prio to avoid suggesting `abel` on trivial goals |
---
`hint` before this change:
```lean
import Mathlib
def f (p : Nat × Nat) := (p.fst, p.snd)
example : f = id := by hint -- suggests `abel`
```
`hint` after this change:
```lean
import Mathlib
def f (p : Nat × Nat) := (p.fst, p.snd)
example : f = id := by hint -- suggests `trivial`
```
---
[](https://gitpod.io/from-referrer/)
|
t-meta |
14/6 |
Mathlib/Tactic/Abel.lean,MathlibTest/hintAll.lean |
2 |
1 |
['github-actions'] |
nobody |
0-10051 2 hours ago |
0-10150 2 hours ago |
0-10192 2 hours |
| 31558 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(Topology/Sublevel): sublevels and overlevels, relation with semicontinuity |
Define sublevels and overlevels of a function, in various sorts (`LE` or LT`, relative to a set).
Relation with semicontinuity.
`Set.inter_leSublevelOn_empty_iff_exists_finset_inter`, an intersection of sublevels of a lower semicontinuous function on a compact set is empty if and only if a finite sub-intersection is already empty.
Co-authored with @ADedecker
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
400/0 |
Mathlib.lean,Mathlib/Topology/Compactness/Compact.lean,Mathlib/Topology/Sublevel.lean |
3 |
18 |
['AntoineChambert-Loir', 'github-actions', 'j-loreaux', 'mathlib4-merge-conflict-bot'] |
j-loreaux assignee:j-loreaux |
0-8676 2 hours ago |
1-13858 1 day ago |
7-16424 7 days |
| 31409 |
SnirBroshi author:SnirBroshi |
feat(Analysis/SpecialFunctions/Gamma/BohrMollerup): the Gamma function has a minimum in (1, 2) |
There's a number in `(1, 2)` which is a minimum of `Gamma` on `(0, ∞)`.
The actual number is ≈ 1.46163...
---
- [x] depends on: #31407
[](https://gitpod.io/from-referrer/)
|
t-analysis |
20/0 |
Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean |
2 |
4 |
['github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot'] |
grunweg assignee:grunweg |
0-8171 2 hours ago |
1-85340 1 day ago |
0-7270 2 hours |
| 31547 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(Analysis/Convex/SaddlePoint): define saddle points of a map |
* `IsSaddlePointOn`.
Let `f : E × F → β` be a map, where `β` is preordered.
A pair `(a,b)` in `E × F` is a *saddle point* of `f` on `X × Y`
if `f a y ≤ f x b` for all `x ∈ X` and all `y `in Y`.
* `isSaddlePointOn_iff`: if `β` is a complete linear order,
then `(a, b) ∈ X × Y` is a saddle point on `X × Y` iff
`⨆ y ∈ Y, f a y = ⨅ x ∈ X f x b = f a b`.
Co-authored-by: @ADedecker
---
[](https://gitpod.io/from-referrer/)
|
t-analysis |
228/0 |
Mathlib.lean,Mathlib/Analysis/Convex/Quasiconvex.lean,Mathlib/Analysis/Convex/SaddlePoint.lean,Mathlib/Data/Set/Basic.lean |
4 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
0-8035 2 hours ago |
1-54593 1 day ago |
6-74947 6 days |
| 31860 |
dagurtomas author:dagurtomas |
feat(CategoryTheory): effective epi implies strong epi |
Also:
* Import `EffectiveEpi.Basic` in the file defining `RegularEpi`, and prove the relationship there.
* Fix some names and golf some proofs in `EffectiveEpi.Basic`
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory |
71/85 |
Mathlib/CategoryTheory/EffectiveEpi/Basic.lean,Mathlib/CategoryTheory/EffectiveEpi/RegularEpi.lean,Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean |
3 |
2 |
['dagurtomas', 'github-actions'] |
nobody |
0-7383 2 hours ago |
0-20696 5 hours ago |
0-20740 5 hours |
| 31868 |
gasparattila author:gasparattila |
feat(Topology/UniformSpace/Closeds): uniform continuity of the singleton map |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
79/0 |
Mathlib/Topology/UniformSpace/Closeds.lean |
1 |
1 |
['github-actions'] |
nobody |
0-7380 2 hours ago |
0-7380 2 hours ago |
0-7421 2 hours |
| 31059 |
gasparattila author:gasparattila |
feat(Topology/Sets): define the Vietoris topology on `(Nonempty)Compacts` |
This PR defines the Vietoris topology on `Compacts` and `NonemptyCompacts`, and proves that it is induced by the Hausdorff uniformity.
---
- [x] depends on: #31031
- [x] depends on: #31058
[](https://gitpod.io/from-referrer/)
|
|
224/29 |
Mathlib.lean,Mathlib/Data/Rel.lean,Mathlib/Topology/MetricSpace/Closeds.lean,Mathlib/Topology/Sets/Compacts.lean,Mathlib/Topology/Sets/VietorisTopology.lean,Mathlib/Topology/UniformSpace/Closeds.lean |
6 |
4 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-7310 2 hours ago |
0-10584 2 hours ago |
0-14033 3 hours |
| 31142 |
thorimur author:thorimur |
feat(Linter): port unused `Decidable*` instance hypothesis linter |
This PR ports the `decidableClassical` linter from mathlib3 which detects `Decidable*` instances in the type of a theorem that are unused in the remainder of the type, and can therefore be replaced with `classical` in the proof.
Prior art: #10235. This is an open pull request from over a year ago that has slowed down, but fulfills a similar purpose. There is a major difference: #10235 contributes an `env_linter` that does not run interactively, while the current PR is a syntax linter that runs while editing.
In this PR, we lint only user-written theorems (including `theorem`s, `lemma`s, and `instance`s of `Prop` classes) by looking for elaborated declarations in the infotree. This opens us up to better logging and try-this suggestions. (While this PR is written with future expansion in mind, these tasks require developing the meta API a bit further and are left to subsequent PRs.)
The infrastructure here is generic to unused instances in the remainder of a type, and can easily be used to write the other `FinType`, `Encodable`, etc. linters.
We rename the linter from `decidableClassical` to `unusedDecidableInType` with the intention of naming all future related linters according to the same pattern.
This PR does *not* turn the linter on in mathlib; it is off by default.
---
[](https://gitpod.io/from-referrer/)
|
t-linter
t-meta
|
479/3 |
Mathlib.lean,Mathlib/Lean/Elab/InfoTree.lean,Mathlib/Lean/Environment.lean,Mathlib/Lean/Expr.lean,Mathlib/Lean/Expr/Basic.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean,Mathlib/Tactic/Linter/UnusedInstancesInType.lean,MathlibTest/UnusedInstancesInType.lean |
10 |
2 |
['github-actions', 'mathlib4-merge-conflict-bot'] |
nobody |
0-6032 1 hour ago |
1-59057 1 day ago |
15-6243 15 days |
| 31870 |
gasparattila author:gasparattila |
feat(Topology/UniformSpace/Closeds): uniform continuity of `Set.image` |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
57/2 |
Mathlib/Topology/UniformSpace/Closeds.lean |
1 |
1 |
['github-actions'] |
nobody |
0-5861 1 hour ago |
0-5865 1 hour ago |
0-5900 1 hour |
| 31869 |
gasparattila author:gasparattila |
feat(Topology/UniformSpace/Closeds): total boundedness of the powerset |
---
[](https://gitpod.io/from-referrer/)
|
t-topology |
29/42 |
Mathlib/Topology/MetricSpace/Closeds.lean,Mathlib/Topology/UniformSpace/Closeds.lean |
2 |
1 |
['github-actions'] |
nobody |
0-5718 1 hour ago |
0-6306 1 hour ago |
0-6346 1 hour |
| 26129 |
LessnessRandomness author:LessnessRandomness |
feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality for angles |
This PR continues the work from #24206.
Original PR: https://github.com/leanprover-community/mathlib4/pull/24206 |
new-contributor
t-euclidean-geometry
|
200/12 |
Mathlib.lean,Mathlib/Analysis/InnerProductSpace/Basic.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/TriangleInequality.lean |
5 |
101 |
['JovanGerb', 'LessnessRandomness', 'Timeroot', 'github-actions', 'jsm28', 'mathlib4-merge-conflict-bot', 'themathqueen'] |
jsm28 assignee:jsm28 |
0-4585 1 hour ago |
4-4934 4 days ago |
152-4087 152 days |
| 31611 |
thorimur author:thorimur |
feat(Meta): `withPlural` wrapper for more readable messages in source |
This small PR introduces a thin wrapper `withPlural` for Lean's textual datatypes so that we can write
```
"foo".withPlural "foos" count
```
instead of
```
if count = 1 then "foo" else "foos"
```
The dot notation here is chosen so that the singular version of the word appears at the start of the syntax, as opposed to buried in an `if/then`. This makes dynamically pluralizing a word in `MessageData` (which is a relatively common occurrence) a bit easier to read in source, especially when multiple pluralizations are needed close to one another.
---
Am I handling the copyright header correctly? My reasoning is that the file was devoid of content, and so this is ultimately a new file. But I'm not sure this is technically what should happen here.
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-meta
|
63/5 |
Mathlib/Lean/Message.lean |
1 |
16 |
['adomani', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot', 'thorimur'] |
alexjbest assignee:alexjbest |
0-3446 57 minutes ago |
0-84742 23 hours ago |
6-25287 6 days |
| 31864 |
erdOne author:erdOne |
feat(RingTheory): resultant is in the span of the two polynomials |
---
[](https://gitpod.io/from-referrer/)
|
t-ring-theory |
96/0 |
Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/RingTheory/Polynomial/Resultant/Basic.lean |
2 |
1 |
['github-actions'] |
nobody |
0-1684 28 minutes ago |
0-1684 27 minutes ago |
0-11649 3 hours |