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-48598 2 months ago |
96-55053 3 months ago |
96-55080 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-83912 1 month ago |
52-58000 1 month ago |
52-59572 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-30764 1 month ago |
50-1706 1 month ago |
50-60717 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-83868 1 month ago |
40-56413 1 month ago |
40-56441 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-2262 1 month ago |
65-39241 2 months ago |
65-55442 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-52442 29 days ago |
30-41935 30 days ago |
30-41973 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-83916 27 days ago |
73-81861 2 months ago |
73-81832 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-83896 25 days ago |
33-22545 1 month ago |
40-42264 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-31754 20 days ago |
20-34607 20 days ago |
113-69819 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-45060 16 days ago |
16-48690 16 days ago |
122-70327 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-83896 15 days ago |
48-10501 1 month ago |
48-16545 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-83885 15 days ago |
23-38703 23 days ago |
23-47567 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-83881 15 days ago |
23-53979 23 days ago |
23-54019 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-55776 14 days ago |
31-54838 1 month ago |
31-79573 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-35596 14 days ago |
41-16296 1 month ago |
41-18519 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-83899 13 days ago |
21-22569 21 days ago |
21-55890 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-3413 13 days ago |
32-45991 1 month ago |
32-50634 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-81210 11 days ago |
37-12359 1 month ago |
37-12393 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-73975 11 days ago |
11-82679 11 days ago |
91-34762 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-59024 11 days ago |
11-59026 11 days ago |
11-59057 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-57035 11 days ago |
11-57059 11 days ago |
45-36971 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-49000 11 days ago |
11-49274 11 days ago |
11-49296 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-83889 10 days ago |
18-5817 18 days ago |
18-5790 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-39986 10 days ago |
10-39998 10 days ago |
10-40033 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-30986 10 days ago |
11-41640 11 days ago |
11-41635 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-5386 9 days ago |
9-11328 9 days ago |
60-85354 60 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-83898 8 days ago |
13-23487 13 days ago |
13-25995 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-83890 8 days ago |
16-75422 16 days ago |
16-75410 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-83879 8 days ago |
15-4244 15 days ago |
15-4279 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-83878 8 days ago |
14-72616 14 days ago |
14-72595 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-83867 8 days ago |
12-6488 12 days ago |
12-6518 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-11644 8 days ago |
65-83920 2 months ago |
87-52012 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-83902 7 days ago |
15-30992 15 days ago |
15-30943 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-83876 7 days ago |
11-23360 11 days ago |
11-23395 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-44309 7 days ago |
7-44310 7 days ago |
11-30287 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-42475 7 days ago |
7-57175 7 days ago |
7-57207 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-57789 6 days ago |
6-57991 6 days ago |
21-24892 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-8638 6 days ago |
6-21108 6 days ago |
19-62838 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-83893 5 days ago |
9-29552 9 days ago |
9-29593 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-29951 5 days ago |
18-21908 18 days ago |
23-22210 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-83882 4 days ago |
8-82930 8 days ago |
8-82967 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-83876 4 days ago |
8-40578 8 days ago |
8-40619 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-83873 4 days ago |
8-10355 8 days ago |
8-10479 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-15231 4 days ago |
4-20439 4 days ago |
4-21155 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-83893 3 days ago |
15-33811 15 days ago |
15-33846 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-83879 3 days ago |
7-37207 7 days ago |
7-37242 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-82749 3 days ago |
17-79778 17 days ago |
17-79752 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-81154 3 days ago |
16-48058 16 days ago |
16-48031 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-68377 3 days ago |
4-52253 4 days ago |
4-52291 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-45920 3 days ago |
22-45039 22 days ago |
22-45012 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-31654 3 days ago |
15-25523 15 days ago |
15-25510 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-30486 3 days ago |
3-30486 3 days ago |
3-56652 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-25331 3 days ago |
7-6247 7 days ago |
7-8706 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-22232 3 days ago |
4-52591 4 days ago |
4-52576 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-8536 3 days ago |
21-6905 21 days ago |
21-6939 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-1313 3 days ago |
3-1313 3 days ago |
45-47950 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-84398 2 days ago |
2-84398 2 days ago |
63-5228 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-83901 2 days ago |
7-675 7 days ago |
8-57000 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-69862 2 days ago |
2-69869 2 days ago |
2-69902 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-58402 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-25873 2 days ago |
7-8727 7 days ago |
7-8705 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-22149 2 days ago |
2-22462 2 days ago |
2-22495 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-18679 2 days ago |
2-18697 2 days ago |
2-18731 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-83903 1 day ago |
50-56791 1 month ago |
50-56764 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-83901 1 day ago |
27-73249 27 days ago |
27-73284 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-83900 1 day ago |
27-41716 27 days ago |
27-41688 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-83894 1 day ago |
7-40439 7 days ago |
7-40477 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-83888 1 day ago |
5-25106 5 days ago |
5-25141 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-76981 1 day ago |
1-77004 1 day ago |
28-16026 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-69118 1 day ago |
1-69431 1 day ago |
2-55711 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-68393 1 day ago |
1-68402 1 day ago |
1-68438 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-57294 1 day ago |
5-7557 5 days ago |
17-33557 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-56842 1 day ago |
5-22818 5 days ago |
5-28064 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-56800 1 day ago |
3-76305 3 days ago |
64-17992 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-56348 1 day ago |
14-9903 14 days ago |
23-59263 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-55449 1 day ago |
1-55762 1 day ago |
1-59749 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-54359 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-52701 1 day ago |
5-18816 5 days ago |
5-29449 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-51584 1 day ago |
1-51600 1 day ago |
2-26324 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-49641 1 day ago |
1-55034 1 day ago |
1-55053 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-49434 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-49426 1 day ago |
23-21228 23 days ago |
23-51764 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-49366 1 day ago |
1-49379 1 day ago |
18-60382 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-49364 1 day ago |
31-59472 1 month ago |
49-7616 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-49016 1 day ago |
1-49030 1 day ago |
80-66747 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-48438 1 day ago |
1-48455 1 day ago |
6-5283 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-48258 1 day ago |
22-17079 22 days ago |
52-43869 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-48054 1 day ago |
1-48071 1 day ago |
42-20294 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-48026 1 day ago |
1-48041 1 day ago |
6-35270 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-46765 1 day ago |
1-55779 1 day ago |
9-48542 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-44076 1 day ago |
1-48824 1 day ago |
51-19686 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-43920 1 day ago |
1-43936 1 day ago |
14-45861 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-43653 1 day ago |
1-43661 1 day ago |
17-86312 17 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-43479 1 day ago |
190-39342 6 months ago |
275-12358 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-33482 1 day ago |
2-4815 2 days ago |
5-14623 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-32572 1 day ago |
1-32580 1 day ago |
24-72639 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-31936 1 day ago |
1-31936 1 day ago |
7-44822 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-31435 1 day ago |
12-64360 12 days ago |
69-58451 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-31077 1 day ago |
46-25840 1 month ago |
46-25867 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 |
11 |
['Ruben-VandeVelde', 'github-actions', 'josephmckinsey', 'mathlib4-merge-conflict-bot'] |
joneugster assignee:joneugster |
1-30981 1 day ago |
14-29170 14 days ago |
40-22433 40 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-30017 1 day ago |
1-30017 1 day ago |
4-59055 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-29177 1 day ago |
1-33247 1 day ago |
1-34751 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-29040 1 day ago |
1-29058 1 day ago |
9-4046 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-27244 1 day ago |
70-24874 2 months ago |
154-24909 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-27154 1 day ago |
1-27162 1 day ago |
37-31845 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-26496 1 day ago |
1-51052 1 day ago |
5-22292 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-25893 1 day ago |
1-25893 1 day ago |
99-50816 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-25073 1 day ago |
1-36320 1 day ago |
11-15080 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-24067 1 day ago |
1-32656 1 day ago |
28-76116 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-22866 1 day ago |
1-22885 1 day ago |
3-15390 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-22700 1 day ago |
9-24480 9 days ago |
17-15487 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-22609 1 day ago |
9-44098 9 days ago |
20-46266 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-21978 1 day ago |
1-21994 1 day ago |
50-72241 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-21563 1 day ago |
1-52879 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-21006 1 day ago |
5-12762 5 days ago |
10-57081 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-20967 1 day ago |
11-46858 11 days ago |
11-46832 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-20643 1 day ago |
1-20739 1 day ago |
1-20712 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-18633 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-18311 1 day ago |
1-39348 1 day ago |
26-27340 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-17010 1 day ago |
50-34233 1 month ago |
130-35449 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-10607 1 day ago |
8-9776 8 days ago |
8-9807 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-1700 1 day ago |
1-47455 1 day ago |
240-62256 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-433 1 day ago |
107-2149 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 |
0-85643 23 hours ago |
0-85643 23 hours ago |
1-18737 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-83902 23 hours ago |
1-28761 1 day ago |
9-56327 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-80536 22 hours ago |
15-34390 15 days ago |
15-34424 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-79549 22 hours ago |
89-46225 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-79138 21 hours ago |
1-57594 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-78803 21 hours ago |
4-3607 4 days ago |
4-3596 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-76244 21 hours ago |
0-76261 21 hours ago |
9-61917 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-73294 20 hours ago |
0-74867 20 hours ago |
0-75719 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-71056 19 hours ago |
0-74308 20 hours ago |
4-1293 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-63461 17 hours ago |
0-66301 18 hours ago |
7-65892 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-62834 17 hours ago |
0-62835 17 hours ago |
0-62924 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-61504 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-57432 15 hours ago |
0-57497 15 hours ago |
0-57472 15 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-56807 15 hours ago |
10-29446 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-56165 15 hours ago |
9-44445 9 days ago |
19-36540 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-54989 15 hours ago |
2-7589 2 days ago |
2-30219 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-54217 15 hours ago |
1-56623 1 day ago |
15-20589 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-50346 13 hours ago |
0-51123 14 hours ago |
11-33215 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-50063 13 hours ago |
0-83263 23 hours ago |
10-34220 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-49864 13 hours ago |
0-83551 23 hours ago |
4-36699 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-48951 13 hours ago |
3-15028 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-48858 13 hours ago |
31-59936 1 month ago |
54-82796 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-48760 13 hours ago |
0-48779 13 hours ago |
7-1769 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-45745 12 hours ago |
0-46281 12 hours ago |
14-47047 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-44984 12 hours ago |
0-44984 12 hours ago |
0-45021 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-44744 12 hours ago |
0-45860 12 hours ago |
0-45900 12 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-44513 12 hours ago |
16-38453 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-44437 12 hours ago |
1-55704 1 day ago |
75-12096 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-43535 12 hours ago |
0-43543 12 hours ago |
31-20447 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-43465 12 hours ago |
0-43486 12 hours ago |
2-80757 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-41685 11 hours ago |
0-41687 11 hours ago |
1-16585 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-41130 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-41089 11 hours ago |
12-11967 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-40063 11 hours ago |
0-46024 12 hours ago |
0-46065 12 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-39781 11 hours ago |
0-39800 11 hours ago |
3-28251 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-39306 10 hours ago |
12-12319 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-38277 10 hours ago |
0-38340 10 hours ago |
0-38314 10 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-37861 10 hours ago |
1-52827 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-36677 10 hours ago |
1-30364 1 day ago |
1-30458 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-36263 10 hours ago |
0-55926 15 hours ago |
0-55901 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-36207 10 hours ago |
1-39800 1 day ago |
34-26153 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-35265 9 hours ago |
0-37744 10 hours ago |
0-37782 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-34355 9 hours ago |
59-29594 1 month ago |
59-30869 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-33454 9 hours ago |
16-33436 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-33372 9 hours ago |
0-40026 11 hours ago |
8-78742 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-32956 9 hours ago |
0-32974 9 hours ago |
13-62426 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-31404 8 hours ago |
0-44674 12 hours ago |
16-60147 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-31391 8 hours ago |
0-58743 16 hours ago |
1-32663 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-31323 8 hours ago |
4-63428 4 days ago |
4-63462 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-31278 8 hours ago |
1-57229 1 day ago |
25-27479 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-31257 8 hours ago |
1-57124 1 day ago |
25-80542 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-31243 8 hours ago |
1-57013 1 day ago |
26-45836 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-31187 8 hours ago |
1-57600 1 day ago |
53-49756 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-31165 8 hours ago |
1-58318 1 day ago |
21-58958 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-31107 8 hours ago |
0-67846 18 hours ago |
3-57490 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-30075 8 hours ago |
0-30075 8 hours ago |
1-11778 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-29418 8 hours ago |
0-32961 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-29381 8 hours ago |
4-20483 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-25599 7 hours ago |
1-22824 1 day ago |
5-39141 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-23947 6 hours ago |
1-49161 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-22699 6 hours ago |
1-32819 1 day ago |
3-1888 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-22653 6 hours ago |
0-33468 9 hours ago |
0-33489 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-19830 5 hours ago |
0-69422 19 hours ago |
0-81372 22 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-17321 4 hours ago |
0-17321 4 hours ago |
6-18591 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-16147 4 hours ago |
1-53124 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-14012 3 hours ago |
1-57095 1 day ago |
129-28447 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-13985 3 hours ago |
0-13993 3 hours ago |
71-73859 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-12984 3 hours ago |
0-13008 3 hours ago |
28-59620 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-12736 3 hours ago |
0-69988 19 hours ago |
0-70021 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-12324 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-12015 3 hours ago |
0-25473 7 hours ago |
0-30802 8 hours |
| 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-9501 2 hours ago |
1-52874 1 day ago |
6-37616 6 days |
| 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-7208 2 hours ago |
1-12390 1 day ago |
7-14954 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-6703 1 hour ago |
1-83872 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-6567 1 hour ago |
1-53125 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-5915 1 hour ago |
0-19228 5 hours ago |
0-19270 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-5912 1 hour ago |
0-5912 1 hour ago |
0-5951 1 hour |
| 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-5842 1 hour ago |
0-9116 2 hours ago |
0-12563 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-4564 1 hour ago |
1-57589 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-4393 1 hour ago |
0-4397 1 hour ago |
0-4430 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-4250 1 hour ago |
0-4838 1 hour ago |
0-4876 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-3117 51 minutes ago |
4-3466 4 days ago |
152-2616 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-1978 32 minutes ago |
0-83274 23 hours ago |
6-23817 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-216 3 minutes ago |
0-216 3 minutes ago |
0-10179 2 hours |