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-45136 2 months ago |
96-51591 3 months ago |
96-51623 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-80450 1 month ago |
52-54538 1 month ago |
52-56115 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-27302 1 month ago |
49-84644 1 month ago |
50-57260 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-80406 1 month ago |
40-52951 1 month ago |
40-52984 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 |
31-85200 1 month ago |
65-35779 2 months ago |
65-51985 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-48980 29 days ago |
30-38473 30 days ago |
30-38515 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-80454 27 days ago |
73-78399 2 months ago |
73-78375 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-80434 25 days ago |
33-19083 1 month ago |
40-38807 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-28292 20 days ago |
20-31145 20 days ago |
113-66362 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-41598 16 days ago |
16-45228 16 days ago |
122-66870 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-80434 15 days ago |
48-7039 1 month ago |
48-13088 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-80423 15 days ago |
23-35241 23 days ago |
23-44109 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-80419 15 days ago |
23-50517 23 days ago |
23-50561 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-52314 14 days ago |
31-51376 1 month ago |
31-76115 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-32134 14 days ago |
41-12834 1 month ago |
41-15062 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-80437 13 days ago |
21-19107 21 days ago |
21-52432 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 |
12-86351 12 days ago |
32-42529 1 month ago |
32-47176 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-77748 11 days ago |
37-8897 1 month ago |
37-8936 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-70513 11 days ago |
11-79217 11 days ago |
91-31305 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-55562 11 days ago |
11-55564 11 days ago |
11-55600 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-53573 11 days ago |
11-53597 11 days ago |
45-33514 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-45538 11 days ago |
11-45812 11 days ago |
11-45839 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-80427 10 days ago |
18-2355 18 days ago |
18-2333 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-36524 10 days ago |
10-36536 10 days ago |
10-36576 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-27524 10 days ago |
11-38178 11 days ago |
11-38178 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-1924 9 days ago |
9-7866 9 days ago |
60-81897 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-80436 8 days ago |
13-20025 13 days ago |
13-22538 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-80428 8 days ago |
16-71960 16 days ago |
16-71953 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-80417 8 days ago |
15-782 15 days ago |
15-822 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-80416 8 days ago |
14-69154 14 days ago |
14-69138 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-80405 8 days ago |
12-3026 12 days ago |
12-3061 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-8182 8 days ago |
65-80458 2 months ago |
87-48554 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-80440 7 days ago |
15-27530 15 days ago |
15-27489 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-80414 7 days ago |
11-19898 11 days ago |
11-19938 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-40847 7 days ago |
7-40848 7 days ago |
11-26830 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-39013 7 days ago |
7-53713 7 days ago |
7-53750 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-54327 6 days ago |
6-54529 6 days ago |
21-21434 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-5176 6 days ago |
6-17646 6 days ago |
19-59380 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-80431 5 days ago |
9-26090 9 days ago |
9-26136 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-26489 5 days ago |
18-18446 18 days ago |
23-18752 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-80420 4 days ago |
8-79468 8 days ago |
8-79510 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-80414 4 days ago |
8-37116 8 days ago |
8-37162 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-80411 4 days ago |
8-6893 8 days ago |
8-7022 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-11769 4 days ago |
4-16977 4 days ago |
4-17698 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-80431 3 days ago |
15-30349 15 days ago |
15-30389 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-80417 3 days ago |
7-33745 7 days ago |
7-33785 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-79287 3 days ago |
17-76316 17 days ago |
17-76295 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-77692 3 days ago |
16-44596 16 days ago |
16-44574 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-64915 3 days ago |
4-48791 4 days ago |
4-48833 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-42458 3 days ago |
22-41577 22 days ago |
22-41554 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-28192 3 days ago |
15-22061 15 days ago |
15-22053 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-27024 3 days ago |
3-27024 3 days ago |
3-53195 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-21869 3 days ago |
7-2785 7 days ago |
7-5249 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-18770 3 days ago |
4-49129 4 days ago |
4-49118 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-5074 3 days ago |
21-3443 21 days ago |
21-3481 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 |
2-84251 2 days ago |
2-84251 2 days ago |
45-44493 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-80936 2 days ago |
2-80936 2 days ago |
63-1771 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-80439 2 days ago |
6-83613 6 days ago |
8-53543 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-66400 2 days ago |
2-66407 2 days ago |
2-66444 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-54940 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-22411 2 days ago |
7-5265 7 days ago |
7-5248 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-18687 2 days ago |
2-19000 2 days ago |
2-19037 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-15217 2 days ago |
2-15235 2 days ago |
2-15273 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-80441 1 day ago |
50-53329 1 month ago |
50-53306 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-80439 1 day ago |
27-69787 27 days ago |
27-69826 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-80438 1 day ago |
27-38254 27 days ago |
27-38230 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-80432 1 day ago |
7-36977 7 days ago |
7-37020 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-80426 1 day ago |
5-21644 5 days ago |
5-21684 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-73519 1 day ago |
1-73542 1 day ago |
28-12568 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-65656 1 day ago |
1-65969 1 day ago |
2-52253 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-64931 1 day ago |
1-64940 1 day ago |
1-64980 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-53832 1 day ago |
5-4095 5 days ago |
17-30100 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-53380 1 day ago |
5-19356 5 days ago |
5-24607 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-53338 1 day ago |
3-72843 3 days ago |
64-14535 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-52886 1 day ago |
14-6441 14 days ago |
23-55805 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-51987 1 day ago |
1-52300 1 day ago |
1-56292 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-50897 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-49239 1 day ago |
5-15354 5 days ago |
5-25992 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-48122 1 day ago |
1-48138 1 day ago |
2-22866 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-46179 1 day ago |
1-51572 1 day ago |
1-51595 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-45972 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-45964 1 day ago |
23-17766 23 days ago |
23-48306 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-45904 1 day ago |
1-45917 1 day ago |
18-56924 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-45902 1 day ago |
31-56010 1 month ago |
49-4158 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-45554 1 day ago |
1-45568 1 day ago |
80-63290 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-44976 1 day ago |
1-44993 1 day ago |
6-1825 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-44796 1 day ago |
22-13617 22 days ago |
52-40411 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-44592 1 day ago |
1-44609 1 day ago |
42-16837 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-44564 1 day ago |
1-44579 1 day ago |
6-31813 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-43303 1 day ago |
1-52317 1 day ago |
9-45084 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-40614 1 day ago |
1-45362 1 day ago |
51-16229 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-40458 1 day ago |
1-40474 1 day ago |
14-42404 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-40191 1 day ago |
1-40199 1 day ago |
17-82855 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-40017 1 day ago |
190-35880 6 months ago |
275-8902 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-30020 1 day ago |
2-1353 2 days ago |
5-11166 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-29110 1 day ago |
1-29118 1 day ago |
24-69181 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-28474 1 day ago |
1-28474 1 day ago |
7-41365 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-27973 1 day ago |
12-60898 12 days ago |
69-54994 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-27615 1 day ago |
46-22378 1 month ago |
46-22410 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-27519 1 day ago |
14-25708 14 days ago |
40-18975 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-26555 1 day ago |
1-26555 1 day ago |
4-55598 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-25715 1 day ago |
1-29785 1 day ago |
1-31294 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-25578 1 day ago |
1-25596 1 day ago |
9-589 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-23782 1 day ago |
70-21412 2 months ago |
154-21452 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-23692 1 day ago |
1-23700 1 day ago |
37-28387 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-23034 1 day ago |
1-47590 1 day ago |
5-18835 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-22431 1 day ago |
1-22431 1 day ago |
99-47359 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-21611 1 day ago |
1-32858 1 day ago |
11-11622 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-20605 1 day ago |
1-29194 1 day ago |
28-72658 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-19404 1 day ago |
1-19423 1 day ago |
3-11933 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-19238 1 day ago |
9-21018 9 days ago |
17-12030 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-19147 1 day ago |
9-40636 9 days ago |
20-42808 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-18516 1 day ago |
1-18532 1 day ago |
50-68783 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-18101 1 day ago |
1-49417 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-17544 1 day ago |
5-9300 5 days ago |
10-53624 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-17505 1 day ago |
11-43396 11 days ago |
11-43375 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-17181 1 day ago |
1-17277 1 day ago |
1-17254 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-15171 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-14849 1 day ago |
1-35886 1 day ago |
26-23882 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-13548 1 day ago |
50-30771 1 month ago |
130-31993 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-7145 1 day ago |
8-6314 8 days ago |
8-6350 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 |
0-84638 23 hours ago |
1-43993 1 day ago |
240-58800 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 |
0-83371 23 hours ago |
106-85087 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-82181 22 hours ago |
0-82181 22 hours ago |
1-15279 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-80440 22 hours ago |
1-25299 1 day ago |
9-52870 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-77074 21 hours ago |
15-30928 15 days ago |
15-30967 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-76087 21 hours ago |
89-42763 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-75676 21 hours ago |
1-54132 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-75341 20 hours ago |
4-145 4 days ago |
4-138 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-72782 20 hours ago |
0-72799 20 hours ago |
9-58460 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-69832 19 hours ago |
0-71405 19 hours ago |
0-72261 20 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-67594 18 hours ago |
0-70846 19 hours ago |
3-84235 3 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-59999 16 hours ago |
0-62839 17 hours ago |
7-62434 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-59372 16 hours ago |
0-59373 16 hours ago |
0-59467 16 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-58042 16 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-53970 14 hours ago |
0-54035 15 hours ago |
0-54014 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-53345 14 hours ago |
10-25984 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-52703 14 hours ago |
9-40983 9 days ago |
19-33082 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-51527 14 hours ago |
2-4127 2 days ago |
2-26762 2 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-50839 14 hours ago |
0-79812 22 hours ago |
6-20360 6 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-50755 14 hours ago |
1-53161 1 day ago |
15-17132 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-46884 13 hours ago |
0-47661 13 hours ago |
11-29758 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-46601 12 hours ago |
0-79801 22 hours ago |
10-30763 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-46402 12 hours ago |
0-80089 22 hours ago |
4-33242 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-45489 12 hours ago |
3-11566 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-45396 12 hours ago |
31-56474 1 month ago |
54-79338 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-45298 12 hours ago |
0-45317 12 hours ago |
6-84712 6 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/)
|
|
162/0 |
Mathlib.lean,Mathlib/Algebra/FiveLemma.lean,Mathlib/RingTheory/Flat/IsBaseChange.lean |
3 |
4 |
['github-actions', 'mathlib4-merge-conflict-bot', 'urkud'] |
kex-y assignee:kex-y |
0-42283 11 hours ago |
8-39390 8 days ago |
15-54879 15 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-41522 11 hours ago |
0-41522 11 hours ago |
0-41563 11 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-41282 11 hours ago |
0-42398 11 hours ago |
0-42442 11 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-41051 11 hours ago |
16-34991 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-40975 11 hours ago |
1-52242 1 day ago |
75-8639 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-40073 11 hours ago |
0-40081 11 hours ago |
31-16990 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$ |
179/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-40003 11 hours ago |
1-49380 1 day ago |
2-37298 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-38223 10 hours ago |
0-38225 10 hours ago |
1-13127 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-37668 10 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-37627 10 hours ago |
12-8505 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-36601 10 hours ago |
0-42562 11 hours ago |
0-42607 11 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-36319 10 hours ago |
0-36338 10 hours ago |
3-24793 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-35844 9 hours ago |
12-8857 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-34815 9 hours ago |
0-34878 9 hours ago |
0-34856 9 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-34399 9 hours ago |
1-49365 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-33215 9 hours ago |
1-26902 1 day ago |
1-27000 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-32801 9 hours ago |
0-52464 14 hours ago |
0-52443 14 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-32745 9 hours ago |
1-36338 1 day ago |
34-22696 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-31803 8 hours ago |
0-34282 9 hours ago |
0-34324 9 hours |
| 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-31205 8 hours ago |
4-4 3 days ago |
151-85559 151 days |
| 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-30893 8 hours ago |
59-26132 1 month ago |
59-27412 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-29992 8 hours ago |
16-29974 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-29910 8 hours ago |
0-36564 10 hours ago |
8-75285 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-29494 8 hours ago |
0-29512 8 hours ago |
13-58969 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-27942 7 hours ago |
0-41212 11 hours ago |
16-56689 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.
- [ ] 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 |
270/58 |
Mathlib.lean,Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean,Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean,Mathlib/CategoryTheory/RegularCategory/Basic.lean,docs/references.bib |
5 |
4 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-27929 7 hours ago |
1-54122 1 day ago |
0-60348 16 hours |
| 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-27861 7 hours ago |
4-59966 4 days ago |
4-60004 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-27816 7 hours ago |
1-53767 1 day ago |
25-24021 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-27795 7 hours ago |
1-53662 1 day ago |
25-77084 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-27781 7 hours ago |
1-53551 1 day ago |
26-42378 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-27725 7 hours ago |
1-54138 1 day ago |
53-46299 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 |
161/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-27703 7 hours ago |
1-54856 1 day ago |
21-55501 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-27645 7 hours ago |
0-64384 17 hours ago |
3-54033 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-26613 7 hours ago |
0-26613 7 hours ago |
1-8320 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-25956 7 hours ago |
0-29499 8 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-25919 7 hours ago |
4-17021 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-22137 6 hours ago |
1-19362 1 day ago |
5-35684 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-20485 5 hours ago |
1-45699 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-19237 5 hours ago |
1-29357 1 day ago |
2-84831 2 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-19191 5 hours ago |
0-30006 8 hours ago |
0-30031 8 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-16368 4 hours ago |
0-65960 18 hours ago |
0-77914 21 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-13859 3 hours ago |
0-13859 3 hours ago |
6-15134 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-12685 3 hours ago |
1-49662 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-10550 2 hours ago |
1-53633 1 day ago |
129-24990 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-10523 2 hours ago |
1-55284 1 day ago |
71-59886 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-9522 2 hours ago |
0-9546 2 hours ago |
28-56162 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-9274 2 hours ago |
0-66526 18 hours ago |
0-66563 18 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-8862 2 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-8553 2 hours ago |
0-22011 6 hours ago |
0-27344 7 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-6039 1 hour ago |
1-49412 1 day ago |
6-37616 6 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-3241 54 minutes ago |
1-80410 1 day ago |
0-7270 2 hours |
| 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-2453 40 minutes ago |
0-15766 4 hours ago |
0-15812 4 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-1102 18 minutes ago |
1-54127 1 day ago |
15-6243 15 days |