Are you a maintainer with just a short amount of time? The following kinds of pull requests could be relevant for you.
| 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 |
| 24669 |
qawbecrdtey author:qawbecrdtey |
feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` |
---
[](https://gitpod.io/from-referrer/)
This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it.
```lean
def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E
```
|
maintainer-merge
t-analysis
awaiting-author
|
8/1 |
Mathlib/Analysis/Normed/Operator/LinearIsometry.lean |
1 |
12 |
['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] |
faenuccio assignee:faenuccio |
46-76945 1 month ago |
136-64777 4 months ago |
32-83569 32 days |
| 28893 |
joelriou author:joelriou |
refactor(AlgebraicTopology): redefine the topological simplex using the convexity API |
Before this PR, the n-dimensional topological simplex (in the `AlgebraicTopology` hierarchy) was defined as a subtype of `Fin (n + 1) → ℝ≥0`, which did not interact well with the convexity API which assumes the ambient type is a vector space. In this PR, we redefine the topological simplex functor (as a cosimplicial object in `TopCat`) using the already existing `stdSimplex` from `Analysis.Convex`.
---
- [x] depends on: #28891
- [x] depends on: #28869
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
t-convex-geometry
large-import
maintainer-merge
|
91/108 |
Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SingularSet.lean,Mathlib/AlgebraicTopology/TopologicalSimplex.lean,Mathlib/Analysis/Convex/StdSimplex.lean |
4 |
7 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
13-29814 13 days ago |
22-37853 22 days ago* |
0-2609 43 minutes* |
| 29143 |
RemyDegenne author:RemyDegenne |
feat(Probability/Decision): basic properties of the Bayes risk |
- Comparison of the Bayes risk and the minimax risk
- Maximal value of the Bayes risk and particular cases where it equals that value
- Data-processing inequality
---
- [x] depends on: #29137
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-measure-probability
|
262/1 |
Mathlib.lean,Mathlib/Probability/Decision/Risk/Basic.lean,Mathlib/Probability/Decision/Risk/Defs.lean |
3 |
16 |
['EtienneC30', 'RemyDegenne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
EtienneC30 assignee:EtienneC30 |
12-12434 12 days ago |
12-12434 12 days ago |
25-57290 25 days |
| 30137 |
vlad902 author:vlad902 |
feat(SimpleGraph): characterise when `SimpleGraph V` is a subsingleton/nontrivial |
Helper lemmas I found useful in mutliple PRs for dispatching trivial cases.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-combinatorics
|
14/0 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean |
1 |
5 |
['YaelDillies', 'github-actions', 'vlad902'] |
YaelDillies assignee:YaelDillies |
8-7844 8 days ago |
8-7844 8 days ago |
22-9634 22 days |
| 30136 |
vlad902 author:vlad902 |
feat(SimpleGraph): lemmas characterizing graphs that are not complete/empty |
Two helper lemmas that I've found useful in several other PRs that characterize graphs that are neither complete nor empty.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-combinatorics
|
8/0 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean |
1 |
11 |
['YaelDillies', 'github-actions', 'vlad902'] |
YaelDillies assignee:YaelDillies |
6-45887 6 days ago |
6-45887 6 days ago |
19-30994 19 days |
| 28818 |
SnirBroshi author:SnirBroshi |
feat(Data/Setoid/Basic): add theorems about lifting a function to its kernel |
Currently `ker_lift_injective` and `quotientKerEquivOfRightInverse` lift `f` to `ker f` in their definition.
This PR makes this function available as `Setoid.kerLift f` and adds a few more theorems about it.
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
new-contributor
|
34/16 |
Counterexamples/AharoniKorman.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean,Mathlib/Topology/Separation/Hausdorff.lean |
4 |
32 |
['SnirBroshi', 'eric-wieser', 'github-actions', 'kckennylau', 'mathlib4-merge-conflict-bot', 'pechersky'] |
pechersky assignee:pechersky |
4-24252 4 days ago |
4-24252 4 days ago |
56-53540 56 days |
| 30595 |
winstonyin author:winstonyin |
feat: $C^n$ implicit function theorem |
I formalise a proof that the implicit function obtained from a $C^n$ implicit equation ($n \geq 1$) is $C^n$. Roughly speaking, given an equation $f : E \times F \to F$ that is smooth at $(a,b) : E\times F$ and whose derivative $f'$ is in some sense non-singular, then there exists a function $\phi : E \to F$ such that $\phi(a) = b$, $f(x, \phi(x)) = f(a,b)$ for all $x$ in a neighbourhood of $a$, and $\phi$ is $C^n$ at $a$.
The current implicit function theorem in Mathlib is quite general and not directly applicable to many familiar scenarios. The statements added by this PR correspond to, e.g., the way the theorem is described on Wikipedia, and will be directly useful for an upcoming formalisation of the smoothness theorem for flows of ODEs.
- [x] depends on: #30607
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-analysis
|
145/0 |
Mathlib.lean,Mathlib/Analysis/Calculus/ImplicitContDiff.lean |
2 |
21 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'winstonyin'] |
grunweg assignee:grunweg |
4-8677 4 days ago |
4-8677 4 days ago |
6-83859 6 days |
| 30589 |
euprunin author:euprunin |
chore(Data/List/Perm): golf `Perm.bagInter_right` using `grind` |
---
Show trace profiling of Perm.bagInter_right: 43 ms before, 134 ms after
### Trace profiling of `Perm.bagInter_right` before PR 30589
```diff
diff --git a/Mathlib/Data/List/Perm/Lattice.lean b/Mathlib/Data/List/Perm/Lattice.lean
index 96c0389c29..b71bc44f7f 100644
--- a/Mathlib/Data/List/Perm/Lattice.lean
+++ b/Mathlib/Data/List/Perm/Lattice.lean
@@ -26,6 +26,7 @@ open Perm (swap)
variable [DecidableEq α]
+set_option trace.profiler true in
theorem Perm.bagInter_right {l₁ l₂ : List α} (t : List α) (h : l₁ ~ l₂) :
l₁.bagInter t ~ l₂.bagInter t := by
induction h generalizing t with
```
```
ℹ [454/454] Built Mathlib.Data.List.Perm.Lattice (769ms)
info: Mathlib/Data/List/Perm/Lattice.lean:30:0: [Elab.async] [0.044658] elaborating proof of List.Perm.bagInter_right
[Elab.definition.value] [0.043499] List.Perm.bagInter_right
[Elab.step] [0.042758] induction h generalizing t with
| nil => simp
| cons x => by_cases x ∈ t <;> simp [*]
| swap x y =>
by_cases h : x = y
· simp [h]
by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
· simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt]
| trans _ _ ih_1 ih_2 => exact (ih_1 _).trans (ih_2 _)
[Elab.step] [0.042746] induction h generalizing t with
| nil => simp
| cons x => by_cases x ∈ t <;> simp [*]
| swap x y =>
by_cases h : x = y
· simp [h]
by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
· simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt]
| trans _ _ ih_1 ih_2 => exact (ih_1 _).trans (ih_2 _)
[Elab.step] [0.042738] induction h generalizing t with
| nil => simp
| cons x => by_cases x ∈ t <;> simp [*]
| swap x y =>
by_cases h : x = y
· simp [h]
by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
· simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt]
| trans _ _ ih_1 ih_2 => exact (ih_1 _).trans (ih_2 _)
[Elab.step] [0.034137]
by_cases h : x = y
· simp [h]
by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
· simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt]
[Elab.step] [0.034116]
by_cases h : x = y
· simp [h]
by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
· simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt]
[Elab.step] [0.010183] · simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
[Elab.step] [0.010173] simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
[Elab.step] [0.010168] simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
[Elab.step] [0.010161] simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm,
swap]
Build completed successfully (454 jobs).
```
### Trace profiling of `Perm.bagInter_right` after PR 30589
```diff
diff --git a/Mathlib/Data/List/Perm/Lattice.lean b/Mathlib/Data/List/Perm/Lattice.lean
index 96c0389c29..e2a27287d8 100644
--- a/Mathlib/Data/List/Perm/Lattice.lean
+++ b/Mathlib/Data/List/Perm/Lattice.lean
@@ -26,20 +26,10 @@ open Perm (swap)
variable [DecidableEq α]
+set_option trace.profiler true in
theorem Perm.bagInter_right {l₁ l₂ : List α} (t : List α) (h : l₁ ~ l₂) :
l₁.bagInter t ~ l₂.bagInter t := by
- induction h generalizing t with
- | nil => simp
- | cons x => by_cases x ∈ t <;> simp [*]
- | swap x y =>
- by_cases h : x = y
- · simp [h]
- by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
- · simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
- · simp [xt, yt, mt mem_of_mem_erase]
- · simp [xt, yt, mt mem_of_mem_erase]
- · simp [xt, yt]
- | trans _ _ ih_1 ih_2 => exact (ih_1 _).trans (ih_2 _)
+ induction h generalizing t with grind
theorem Perm.bagInter_left (l : List α) {t₁ t₂ : List α} (p : t₁ ~ t₂) :
l.bagInter t₁ = l.bagInter t₂ := by
```
```
ℹ [454/454] Built Mathlib.Data.List.Perm.Lattice (848ms)
info: Mathlib/Data/List/Perm/Lattice.lean:30:0: [Elab.async] [0.134701] elaborating proof of List.Perm.bagInter_right
[Elab.definition.value] [0.133799] List.Perm.bagInter_right
[Elab.step] [0.133622] induction h generalizing t with grind
[Elab.step] [0.133610] induction h generalizing t with grind
[Elab.step] [0.133599] induction h generalizing t with grind
[Elab.step] [0.052692] grind
[Elab.step] [0.064967] grind
info: Mathlib/Data/List/Perm/Lattice.lean:32:34: [Elab.async] [0.017325] Lean.addDecl
[Kernel] [0.017314] ✅️ typechecking declarations [List.Perm.bagInter_right._proof_1_3]
Build completed successfully (454 jobs).
```
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
1/12 |
Mathlib/Data/List/Perm/Lattice.lean |
1 |
9 |
['JovanGerb', 'euprunin', 'github-actions', 'grunweg', 'pechersky'] |
grunweg assignee:grunweg |
3-36519 3 days ago |
8-50738 8 days ago |
8-78208 8 days |
| 27991 |
sinianluoye author:sinianluoye |
feat (Rat): add Rat.den_eq_of_add_den_eq_one and its dependent lemmas |
```lean4
example {q r : ℚ} (h : (q + r).den = 1) : q.den = r.den := by
```
It is so simple, but I couldn't find it in current mathlib repo.
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
new-contributor
|
22/0 |
Mathlib/Data/Rat/Lemmas.lean |
1 |
23 |
['github-actions', 'pechersky', 'sinianluoye', 'themathqueen'] |
pechersky assignee:pechersky |
3-18779 3 days ago |
3-18779 3 days ago |
77-75418 77 days |
| 25945 |
adomani author:adomani |
feat: the empty line in commands linter |
This linter flags empty lines within a command.
It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places.
It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread.
This PR continues the work from #25236. |
large-import
t-linter
maintainer-merge
|
380/22 |
Mathlib.lean,Mathlib/Algebra/Polynomial/RuleOfSigns.lean,Mathlib/Analysis/Meromorphic/FactorizedRational.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/CategoryTheory/Monoidal/Opposite/Mon_.lean,Mathlib/Data/UInt.lean,Mathlib/Init.lean,Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean,Mathlib/RingTheory/Flat/TorsionFree.lean,Mathlib/RingTheory/HahnSeries/HahnEmbedding.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean |
13 |
22 |
['adomani', 'bryangingechen', 'eric-wieser', 'github-actions', 'mathlib4-merge-conflict-bot'] |
bryangingechen assignee:bryangingechen |
2-85558 2 days ago |
2-85632 2 days ago |
45-25277 45 days |
| 29728 |
ADA-Projects author:ADA-Projects |
feat(Topology/KrullDimension): add subspace dimension inequality |
This PR proves that subspaces have Krull dimension at most that of the ambient space: dim(Y) ≤ dim(X) for Y ⊆ X (theorem topologicalKrullDim_subspace_le).
Supporting results about IrreducibleCloseds were refactored and moved from KrullDimension.lean to Closeds.lean for better modularity.
Note: Some code/documentation generated with AI assistance (Gemini).
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
new-contributor
t-topology
|
63/30 |
Mathlib/Topology/KrullDimension.lean,Mathlib/Topology/Sets/Closeds.lean |
2 |
46 |
['ADA-Projects', 'erdOne', 'fpvandoorn', 'github-actions', 'jcommelin', 'kim-em', 'mathlib4-merge-conflict-bot', 'riccardobrasca'] |
erdOne assignee:erdOne |
2-47336 2 days ago |
4-125 4 days ago |
25-34237 25 days |
| 24965 |
erdOne author:erdOne |
refactor: Make `IsLocalHom` take unbundled map |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebra
merge-conflict
awaiting-author
label:t-algebra$ |
16/7 |
Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean |
5 |
6 |
['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
143-72930 4 months ago |
143-72931 4 months ago |
10-26015 10 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. |
maintainer-merge
t-algebra
merge-conflict
label:t-algebra$ |
68/67 |
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/RootPositive.lean,Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean,Mathlib/RingTheory/Etale/Kaehler.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 |
53-34421 1 month ago |
53-34422 1 month ago |
51-74059 51 days |
| 28737 |
astrainfinita author:astrainfinita |
refactor: deprecate `MulEquivClass` |
This PR continues the work from #18806.
Original PR: https://github.com/leanprover-community/mathlib4/pull/18806 |
maintainer-merge
t-algebra
merge-conflict
awaiting-author
label:t-algebra$ |
67/77 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Irreducible/Lemmas.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/GroupWithZero/Equiv.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Ring/Divisibility/Basic.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Algebra/Star/MonoidHom.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/GroupTheory/Submonoid/Center.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean,Mathlib/Topology/Algebra/ContinuousMonoidHom.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean |
26 |
20 |
['Vierkantor', 'alreadydone', 'astrainfinita', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] |
Vierkantor assignee:Vierkantor |
44-38281 1 month ago |
44-38282 1 month ago |
4-17723 4 days |
| 28676 |
sun123zxy author:sun123zxy |
feat(NumberTheory/ArithmeticFunction): wrap `Nat.totient` as an `ArithmeticFunction` |
This wraps the Euler's totient function `Nat.totient` into a new `ArithmeticFunction` `ϕ`, with some basic identities such as `ϕ * ζ = id` and `μ * id = ϕ.`
---
We use the notation `ϕ` to distinguish from `Nat.totient`'s notation `φ`, however this might be controversial. Suggestions are welcome!
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
new-contributor
t-number-theory
merge-conflict
awaiting-author
|
45/5 |
Mathlib/NumberTheory/ArithmeticFunction.lean |
1 |
19 |
['MichaelStollBayreuth', 'SnirBroshi', 'b-mehta', 'eric-wieser', 'github-actions', 'mathlib4-merge-conflict-bot', 'riccardobrasca', 'sun123zxy'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
7-47227 7 days ago |
7-47228 7 days ago |
53-41880 53 days |
| 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 |
| 24669 |
qawbecrdtey author:qawbecrdtey |
feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` |
---
[](https://gitpod.io/from-referrer/)
This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it.
```lean
def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E
```
|
maintainer-merge
t-analysis
awaiting-author
|
8/1 |
Mathlib/Analysis/Normed/Operator/LinearIsometry.lean |
1 |
12 |
['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] |
faenuccio assignee:faenuccio |
46-76945 1 month ago |
136-64777 4 months ago |
32-83569 32 days |
| 28893 |
joelriou author:joelriou |
refactor(AlgebraicTopology): redefine the topological simplex using the convexity API |
Before this PR, the n-dimensional topological simplex (in the `AlgebraicTopology` hierarchy) was defined as a subtype of `Fin (n + 1) → ℝ≥0`, which did not interact well with the convexity API which assumes the ambient type is a vector space. In this PR, we redefine the topological simplex functor (as a cosimplicial object in `TopCat`) using the already existing `stdSimplex` from `Analysis.Convex`.
---
- [x] depends on: #28891
- [x] depends on: #28869
[](https://gitpod.io/from-referrer/)
|
t-algebraic-topology
t-convex-geometry
large-import
maintainer-merge
|
91/108 |
Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SingularSet.lean,Mathlib/AlgebraicTopology/TopologicalSimplex.lean,Mathlib/Analysis/Convex/StdSimplex.lean |
4 |
7 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] |
robin-carlier assignee:robin-carlier |
13-29814 13 days ago |
22-37853 22 days ago* |
0-2609 43 minutes* |
| 29143 |
RemyDegenne author:RemyDegenne |
feat(Probability/Decision): basic properties of the Bayes risk |
- Comparison of the Bayes risk and the minimax risk
- Maximal value of the Bayes risk and particular cases where it equals that value
- Data-processing inequality
---
- [x] depends on: #29137
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-measure-probability
|
262/1 |
Mathlib.lean,Mathlib/Probability/Decision/Risk/Basic.lean,Mathlib/Probability/Decision/Risk/Defs.lean |
3 |
16 |
['EtienneC30', 'RemyDegenne', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
EtienneC30 assignee:EtienneC30 |
12-12434 12 days ago |
12-12434 12 days ago |
25-57290 25 days |
| 30137 |
vlad902 author:vlad902 |
feat(SimpleGraph): characterise when `SimpleGraph V` is a subsingleton/nontrivial |
Helper lemmas I found useful in mutliple PRs for dispatching trivial cases.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-combinatorics
|
14/0 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean |
1 |
5 |
['YaelDillies', 'github-actions', 'vlad902'] |
YaelDillies assignee:YaelDillies |
8-7844 8 days ago |
8-7844 8 days ago |
22-9634 22 days |
| 30136 |
vlad902 author:vlad902 |
feat(SimpleGraph): lemmas characterizing graphs that are not complete/empty |
Two helper lemmas that I've found useful in several other PRs that characterize graphs that are neither complete nor empty.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-combinatorics
|
8/0 |
Mathlib/Combinatorics/SimpleGraph/Basic.lean |
1 |
11 |
['YaelDillies', 'github-actions', 'vlad902'] |
YaelDillies assignee:YaelDillies |
6-45887 6 days ago |
6-45887 6 days ago |
19-30994 19 days |
| 28818 |
SnirBroshi author:SnirBroshi |
feat(Data/Setoid/Basic): add theorems about lifting a function to its kernel |
Currently `ker_lift_injective` and `quotientKerEquivOfRightInverse` lift `f` to `ker f` in their definition.
This PR makes this function available as `Setoid.kerLift f` and adds a few more theorems about it.
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
new-contributor
|
34/16 |
Counterexamples/AharoniKorman.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean,Mathlib/Topology/Separation/Hausdorff.lean |
4 |
32 |
['SnirBroshi', 'eric-wieser', 'github-actions', 'kckennylau', 'mathlib4-merge-conflict-bot', 'pechersky'] |
pechersky assignee:pechersky |
4-24252 4 days ago |
4-24252 4 days ago |
56-53540 56 days |
| 30595 |
winstonyin author:winstonyin |
feat: $C^n$ implicit function theorem |
I formalise a proof that the implicit function obtained from a $C^n$ implicit equation ($n \geq 1$) is $C^n$. Roughly speaking, given an equation $f : E \times F \to F$ that is smooth at $(a,b) : E\times F$ and whose derivative $f'$ is in some sense non-singular, then there exists a function $\phi : E \to F$ such that $\phi(a) = b$, $f(x, \phi(x)) = f(a,b)$ for all $x$ in a neighbourhood of $a$, and $\phi$ is $C^n$ at $a$.
The current implicit function theorem in Mathlib is quite general and not directly applicable to many familiar scenarios. The statements added by this PR correspond to, e.g., the way the theorem is described on Wikipedia, and will be directly useful for an upcoming formalisation of the smoothness theorem for flows of ODEs.
- [x] depends on: #30607
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-analysis
|
145/0 |
Mathlib.lean,Mathlib/Analysis/Calculus/ImplicitContDiff.lean |
2 |
21 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'winstonyin'] |
grunweg assignee:grunweg |
4-8677 4 days ago |
4-8677 4 days ago |
6-83859 6 days |
| 30589 |
euprunin author:euprunin |
chore(Data/List/Perm): golf `Perm.bagInter_right` using `grind` |
---
Show trace profiling of Perm.bagInter_right: 43 ms before, 134 ms after
### Trace profiling of `Perm.bagInter_right` before PR 30589
```diff
diff --git a/Mathlib/Data/List/Perm/Lattice.lean b/Mathlib/Data/List/Perm/Lattice.lean
index 96c0389c29..b71bc44f7f 100644
--- a/Mathlib/Data/List/Perm/Lattice.lean
+++ b/Mathlib/Data/List/Perm/Lattice.lean
@@ -26,6 +26,7 @@ open Perm (swap)
variable [DecidableEq α]
+set_option trace.profiler true in
theorem Perm.bagInter_right {l₁ l₂ : List α} (t : List α) (h : l₁ ~ l₂) :
l₁.bagInter t ~ l₂.bagInter t := by
induction h generalizing t with
```
```
ℹ [454/454] Built Mathlib.Data.List.Perm.Lattice (769ms)
info: Mathlib/Data/List/Perm/Lattice.lean:30:0: [Elab.async] [0.044658] elaborating proof of List.Perm.bagInter_right
[Elab.definition.value] [0.043499] List.Perm.bagInter_right
[Elab.step] [0.042758] induction h generalizing t with
| nil => simp
| cons x => by_cases x ∈ t <;> simp [*]
| swap x y =>
by_cases h : x = y
· simp [h]
by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
· simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt]
| trans _ _ ih_1 ih_2 => exact (ih_1 _).trans (ih_2 _)
[Elab.step] [0.042746] induction h generalizing t with
| nil => simp
| cons x => by_cases x ∈ t <;> simp [*]
| swap x y =>
by_cases h : x = y
· simp [h]
by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
· simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt]
| trans _ _ ih_1 ih_2 => exact (ih_1 _).trans (ih_2 _)
[Elab.step] [0.042738] induction h generalizing t with
| nil => simp
| cons x => by_cases x ∈ t <;> simp [*]
| swap x y =>
by_cases h : x = y
· simp [h]
by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
· simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt]
| trans _ _ ih_1 ih_2 => exact (ih_1 _).trans (ih_2 _)
[Elab.step] [0.034137]
by_cases h : x = y
· simp [h]
by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
· simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt]
[Elab.step] [0.034116]
by_cases h : x = y
· simp [h]
by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
· simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt, mt mem_of_mem_erase]
· simp [xt, yt]
[Elab.step] [0.010183] · simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
[Elab.step] [0.010173] simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
[Elab.step] [0.010168] simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
[Elab.step] [0.010161] simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm,
swap]
Build completed successfully (454 jobs).
```
### Trace profiling of `Perm.bagInter_right` after PR 30589
```diff
diff --git a/Mathlib/Data/List/Perm/Lattice.lean b/Mathlib/Data/List/Perm/Lattice.lean
index 96c0389c29..e2a27287d8 100644
--- a/Mathlib/Data/List/Perm/Lattice.lean
+++ b/Mathlib/Data/List/Perm/Lattice.lean
@@ -26,20 +26,10 @@ open Perm (swap)
variable [DecidableEq α]
+set_option trace.profiler true in
theorem Perm.bagInter_right {l₁ l₂ : List α} (t : List α) (h : l₁ ~ l₂) :
l₁.bagInter t ~ l₂.bagInter t := by
- induction h generalizing t with
- | nil => simp
- | cons x => by_cases x ∈ t <;> simp [*]
- | swap x y =>
- by_cases h : x = y
- · simp [h]
- by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
- · simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
- · simp [xt, yt, mt mem_of_mem_erase]
- · simp [xt, yt, mt mem_of_mem_erase]
- · simp [xt, yt]
- | trans _ _ ih_1 ih_2 => exact (ih_1 _).trans (ih_2 _)
+ induction h generalizing t with grind
theorem Perm.bagInter_left (l : List α) {t₁ t₂ : List α} (p : t₁ ~ t₂) :
l.bagInter t₁ = l.bagInter t₂ := by
```
```
ℹ [454/454] Built Mathlib.Data.List.Perm.Lattice (848ms)
info: Mathlib/Data/List/Perm/Lattice.lean:30:0: [Elab.async] [0.134701] elaborating proof of List.Perm.bagInter_right
[Elab.definition.value] [0.133799] List.Perm.bagInter_right
[Elab.step] [0.133622] induction h generalizing t with grind
[Elab.step] [0.133610] induction h generalizing t with grind
[Elab.step] [0.133599] induction h generalizing t with grind
[Elab.step] [0.052692] grind
[Elab.step] [0.064967] grind
info: Mathlib/Data/List/Perm/Lattice.lean:32:34: [Elab.async] [0.017325] Lean.addDecl
[Kernel] [0.017314] ✅️ typechecking declarations [List.Perm.bagInter_right._proof_1_3]
Build completed successfully (454 jobs).
```
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
|
1/12 |
Mathlib/Data/List/Perm/Lattice.lean |
1 |
9 |
['JovanGerb', 'euprunin', 'github-actions', 'grunweg', 'pechersky'] |
grunweg assignee:grunweg |
3-36519 3 days ago |
8-50738 8 days ago |
8-78208 8 days |
| 27991 |
sinianluoye author:sinianluoye |
feat (Rat): add Rat.den_eq_of_add_den_eq_one and its dependent lemmas |
```lean4
example {q r : ℚ} (h : (q + r).den = 1) : q.den = r.den := by
```
It is so simple, but I couldn't find it in current mathlib repo.
---
[](https://gitpod.io/from-referrer/)
|
t-data
maintainer-merge
new-contributor
|
22/0 |
Mathlib/Data/Rat/Lemmas.lean |
1 |
23 |
['github-actions', 'pechersky', 'sinianluoye', 'themathqueen'] |
pechersky assignee:pechersky |
3-18779 3 days ago |
3-18779 3 days ago |
77-75418 77 days |
| 25945 |
adomani author:adomani |
feat: the empty line in commands linter |
This linter flags empty lines within a command.
It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places.
It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread.
This PR continues the work from #25236. |
large-import
t-linter
maintainer-merge
|
380/22 |
Mathlib.lean,Mathlib/Algebra/Polynomial/RuleOfSigns.lean,Mathlib/Analysis/Meromorphic/FactorizedRational.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/CategoryTheory/Monoidal/Opposite/Mon_.lean,Mathlib/Data/UInt.lean,Mathlib/Init.lean,Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean,Mathlib/RingTheory/Flat/TorsionFree.lean,Mathlib/RingTheory/HahnSeries/HahnEmbedding.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean |
13 |
22 |
['adomani', 'bryangingechen', 'eric-wieser', 'github-actions', 'mathlib4-merge-conflict-bot'] |
bryangingechen assignee:bryangingechen |
2-85558 2 days ago |
2-85632 2 days ago |
45-25277 45 days |
| 29728 |
ADA-Projects author:ADA-Projects |
feat(Topology/KrullDimension): add subspace dimension inequality |
This PR proves that subspaces have Krull dimension at most that of the ambient space: dim(Y) ≤ dim(X) for Y ⊆ X (theorem topologicalKrullDim_subspace_le).
Supporting results about IrreducibleCloseds were refactored and moved from KrullDimension.lean to Closeds.lean for better modularity.
Note: Some code/documentation generated with AI assistance (Gemini).
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
new-contributor
t-topology
|
63/30 |
Mathlib/Topology/KrullDimension.lean,Mathlib/Topology/Sets/Closeds.lean |
2 |
46 |
['ADA-Projects', 'erdOne', 'fpvandoorn', 'github-actions', 'jcommelin', 'kim-em', 'mathlib4-merge-conflict-bot', 'riccardobrasca'] |
erdOne assignee:erdOne |
2-47336 2 days ago |
4-125 4 days ago |
25-34237 25 days |
| 30518 |
euprunin author:euprunin |
chore(Cache): remove "No files to download" message. make `lake exe cache get` less verbose |
Fixes #27038.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
28/29 |
Cache/IO.lean,Cache/Requests.lean |
2 |
11 |
['YaelDillies', 'euprunin', 'github-actions'] |
ocfnash assignee:ocfnash |
0-78908 21 hours ago |
8-19914 8 days ago |
11-13984 11 days |
| 27578 |
bjornsolheim author:bjornsolheim |
feat: constructor for submodules and pointed cones from two-element closures |
in Algebra/Module/Submodule/Defs.lean
- Construct a submodule from closure under two-element linear combinations.
in Geometry/Convex/Cone/Pointed.lean
- Construct a pointed cone from closure under two-element conical combinations.
- lemma mem_span_set
---
- [x] depends on: #25292
[](https://gitpod.io/from-referrer/)
|
t-convex-geometry
maintainer-merge
new-contributor
|
30/0 |
Mathlib/Algebra/Module/Submodule/Defs.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean |
2 |
45 |
['YaelDillies', 'bjornsolheim', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] |
nobody |
0-63774 17 hours ago |
2-37994 2 days ago |
8-44030 8 days |
| 28296 |
strihanje01 author:strihanje01 |
feat(Combinatorics/Additive/VerySmallDoubling): Hamidoune's Freiman-Kneser theorem for nonabelian groups |
Prove the noncommutative Freiman-Kneser theorem for doubling less than 2 - ε
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
new-contributor
t-combinatorics
|
295/3 |
Mathlib/Combinatorics/Additive/VerySmallDoubling.lean |
1 |
22 |
['YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-merge-conflict-bot', 'strihanje01'] |
YaelDillies assignee:YaelDillies |
0-54043 15 hours ago |
8-27727 8 days ago |
59-30877 59 days |
| 30794 |
kebekus author:kebekus |
feat: API for dealing with divisors attached to meromorphic functions |
Provide supporting API useful in the discussion of (zero/pole) divisors attached to meromorphic functions.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-topology
|
45/4 |
Mathlib/Topology/LocallyFinsupp.lean |
1 |
9 |
['YaelDillies', 'github-actions', 'kebekus'] |
nobody |
0-53662 14 hours ago |
1-43911 1 day ago |
2-8827 2 days |
| 30806 |
yonggyuchoimath author:yonggyuchoimath |
chore(RingTheory/TensorProduct/Basic): split RingTheory.TensorProduct.Basic |
This PR splits the file
* Mathlib/RingTheory/TensorProduct/Basic.lean
into
* Mathlib/RingTheory/TensorProduct/Basic.lean
* Mathlib/RingTheory/TensorProduct/Maps.lean
Everything from the file `Basic.lean` related to maps between tensor products of `R`-algebras has been moved to a new file `Maps.lean`, unless it is required for constructions. |
maintainer-merge |
800/757 |
Mathlib.lean,Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean,Mathlib/Algebra/Azumaya/Basic.lean,Mathlib/Algebra/Category/AlgCat/Monoidal.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/TensorProduct/Opposite.lean,Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean,Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean,Mathlib/RingTheory/Bialgebra/Basic.lean,Mathlib/RingTheory/IsTensorProduct.lean,Mathlib/RingTheory/MatrixAlgebra.lean,Mathlib/RingTheory/Nilpotent/Exp.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/TensorProduct/Basic.lean,Mathlib/RingTheory/TensorProduct/Finite.lean,Mathlib/RingTheory/TensorProduct/Maps.lean,Mathlib/RingTheory/TensorProduct/Pi.lean |
17 |
3 |
['chrisflav', 'github-actions', 'yonggyuchoimath'] |
nobody |
0-50782 14 hours ago |
1-883 1 day ago |
1-74637 1 day |
| 30238 |
kebekus author:kebekus |
feat: behavior of divisors when taking powers of meromorphic functions |
Establish the behavior of divisors when taking powers of meromorphic functions. For consistency, provide `_fun`-versions of several simple lemmas.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-analysis
|
138/4 |
Mathlib/Algebra/Order/WithTop/Untop0.lean,Mathlib/Analysis/Meromorphic/Divisor.lean,Mathlib/Analysis/Meromorphic/FactorizedRational.lean,Mathlib/Analysis/Meromorphic/Order.lean |
4 |
57 |
['YaelDillies', 'bryangingechen', 'github-actions', 'kebekus', 'mathlib4-merge-conflict-bot'] |
YaelDillies assignee:YaelDillies |
0-46208 12 hours ago |
0-65145 18 hours ago |
17-2289 17 days |
| 30850 |
JovanGerb author:JovanGerb |
fix(Tactic/Lift): don't clear a variable if it's impossible |
Closes #19160.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-meta
|
19/14 |
Mathlib/Data/Set/Finite/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Basic.lean,Mathlib/Order/WithBot.lean,Mathlib/Tactic/Lift.lean,MathlibTest/lift.lean |
5 |
4 |
['github-actions', 'grunweg'] |
nobody |
0-36415 10 hours ago |
0-36484 10 hours ago |
0-38016 10 hours |
| 30793 |
LessnessRandomness author:LessnessRandomness |
feat(Analysis/InnerProductSpace/Basic): add a simp lemma |
Add a simp lemma (for benchmarking purposes - to see if it doesn't have a bad performance impact).
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-analysis
awaiting-author
|
7/4 |
Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean,Mathlib/Analysis/InnerProductSpace/Basic.lean,Mathlib/Analysis/InnerProductSpace/PiL2.lean,Mathlib/Geometry/Manifold/Instances/Sphere.lean |
4 |
20 |
['JovanGerb', 'LessnessRandomness', 'fpvandoorn', 'github-actions', 'leanprover-bot', 'mattrobball'] |
nobody |
0-32776 9 hours ago |
0-43876 12 hours ago |
1-61891 1 day |
| 30841 |
staroperator author:staroperator |
feat(SetTheory/ZFC): add `ZFSet.iUnion` |
which is just `sUnion (range f)`. We add a new definition for it instead of making `⋃ i, f i` a notation of `sUnion (range f)`, because the simp normal form of `(sUnion (range f)).toSet` is not `⋃ i, (f i).toSet`.
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
|
45/11 |
Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/SetTheory/ZFC/Ordinal.lean,Mathlib/SetTheory/ZFC/Rank.lean,Mathlib/SetTheory/ZFC/VonNeumann.lean |
4 |
7 |
['YaelDillies', 'github-actions', 'staroperator'] |
nobody |
0-31957 8 hours ago |
0-32403 8 hours ago |
0-47834 13 hours |
| 28833 |
yury-harmonic author:yury-harmonic |
feat(MvPolynomial/Expand): more lemmas |
---
- [x] depends on: #28832
- [x] depends on: #28830
[](https://gitpod.io/from-referrer/)
|
maintainer-merge |
92/20 |
Mathlib/Algebra/MvPolynomial/Eval.lean,Mathlib/Algebra/MvPolynomial/Expand.lean |
2 |
9 |
['dwrensha', 'github-actions', 'mathlib4-dependent-issues-bot', 'yury-harmonic'] |
dwrensha assignee:dwrensha |
0-615 10 minutes ago |
61-9241 2 months ago |
61-10987 61 days |
| 24965 |
erdOne author:erdOne |
refactor: Make `IsLocalHom` take unbundled map |
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-algebra
merge-conflict
awaiting-author
label:t-algebra$ |
16/7 |
Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean |
5 |
6 |
['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
143-72930 4 months ago |
143-72931 4 months ago |
10-26015 10 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. |
maintainer-merge
t-algebra
merge-conflict
label:t-algebra$ |
68/67 |
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/RootPositive.lean,Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean,Mathlib/RingTheory/Etale/Kaehler.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 |
53-34421 1 month ago |
53-34422 1 month ago |
51-74059 51 days |
| 28737 |
astrainfinita author:astrainfinita |
refactor: deprecate `MulEquivClass` |
This PR continues the work from #18806.
Original PR: https://github.com/leanprover-community/mathlib4/pull/18806 |
maintainer-merge
t-algebra
merge-conflict
awaiting-author
label:t-algebra$ |
67/77 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Irreducible/Lemmas.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/GroupWithZero/Equiv.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Ring/Divisibility/Basic.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Algebra/Star/MonoidHom.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/GroupTheory/Submonoid/Center.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean,Mathlib/Topology/Algebra/ContinuousMonoidHom.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean |
26 |
20 |
['Vierkantor', 'alreadydone', 'astrainfinita', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] |
Vierkantor assignee:Vierkantor |
44-38281 1 month ago |
44-38282 1 month ago |
4-17723 4 days |
| 28676 |
sun123zxy author:sun123zxy |
feat(NumberTheory/ArithmeticFunction): wrap `Nat.totient` as an `ArithmeticFunction` |
This wraps the Euler's totient function `Nat.totient` into a new `ArithmeticFunction` `ϕ`, with some basic identities such as `ϕ * ζ = id` and `μ * id = ϕ.`
---
We use the notation `ϕ` to distinguish from `Nat.totient`'s notation `φ`, however this might be controversial. Suggestions are welcome!
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
new-contributor
t-number-theory
merge-conflict
awaiting-author
|
45/5 |
Mathlib/NumberTheory/ArithmeticFunction.lean |
1 |
19 |
['MichaelStollBayreuth', 'SnirBroshi', 'b-mehta', 'eric-wieser', 'github-actions', 'mathlib4-merge-conflict-bot', 'riccardobrasca', 'sun123zxy'] |
MichaelStollBayreuth assignee:MichaelStollBayreuth |
7-47227 7 days ago |
7-47228 7 days ago |
53-41880 53 days |
| 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 |
| 15649 |
TpmKranz author:TpmKranz |
feat(Computability): introduce Generalised NFA as bridge to Regular Expression |
Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid.
Second chunk of #12648
---
- [x] depends on: #15647 [Data.FinEnum.Option unchanged since then]
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
awaiting-author
|
298/0 |
Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib |
5 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'trivial1711'] |
nobody |
172-1669 5 months ago |
172-1678 5 months ago |
23-54870 23 days |
| 20648 |
anthonyde author:anthonyde |
feat: formalize regular expression -> εNFA |
The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness.
---
- [x] depends on: #20644
- [x] depends on: #20645
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
|
490/0 |
Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib |
3 |
5 |
['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'qawbecrdtey'] |
nobody |
172-980 5 months ago |
172-1615 5 months ago |
75-77754 75 days |
| 20238 |
maemre author:maemre |
feat(Computability/DFA): Closure of regular languages under some set operations |
This shows that regular languages are closed under complement and intersection by constructing DFAs for them.
---
Closure under all other operations will be proved when someone adds the proof for DFA<->regular expression equivalence, so they are not part of this PR.
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
awaiting-author
|
159/0 |
Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean |
2 |
59 |
['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'meithecatte', 'urkud'] |
EtienneC30 assignee:EtienneC30 |
142-53840 4 months ago |
172-1579 5 months ago |
48-67492 48 days |
| 23929 |
meithecatte author:meithecatte |
feat(Computability/NFA): improve bound on pumping lemma |
---
- [x] depends on: #25321
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
|
101/10 |
Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean |
2 |
41 |
['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte'] |
nobody |
139-11231 4 months ago |
139-11232 4 months ago |
34-10595 34 days |
| 30150 |
imbrem author:imbrem |
feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory |
Add `AddMonoidalCategory`, the additive version of `MonoidalCategory`.
To get this to work, I needed to _remove_ the `to_additive` attributes in `Discrete.lean`, since existing code relies on the `AddMonoid M → MonoidalCategory M` instance. For now, we simply implement the additive variants by hand instead.
---
As discussed in #28718; I added an `AddMonoidalCategory` struct and tagged `MonoidalCategory` with `to_additive`, along with the lemmas in `Category.lean`.
I think this is the right approach, since under this framework the "correct" additive version of `Discrete.lean` would be mapping an `AddMonoid` to an `AddMonoidalCategory`.
Next steps would be to:
- Make `monoidal_coherence` and `coherence` support `AddMonoidalCategory`
- Add `CocartesianMonoidalCategory` extending `AddMonoidalCategory`
[](https://gitpod.io/from-referrer/)
|
large-import
awaiting-zulip
new-contributor
t-category-theory
t-meta
|
444/125 |
Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Tactic/ToAdditive/GuessName.lean |
3 |
19 |
['JovanGerb', 'YaelDillies', 'github-actions', 'imbrem'] |
nobody |
5-9645 5 days ago |
5-9645 5 days ago |
1-18384 1 day |
| 30526 |
SnirBroshi author:SnirBroshi |
chore(Logic/Relation): use `Subrelation` to state theorems |
chore(Logic/Relation): replace every `∀ x y, r x y → r' x y` with `Subrelation r r'`
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip |
79/73 |
Mathlib/CategoryTheory/IsConnected.lean,Mathlib/CategoryTheory/Limits/Types/Filtered.lean,Mathlib/CategoryTheory/Limits/Types/Shapes.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/Logic/Relation.lean,Mathlib/Order/Interval/Finset/Basic.lean |
7 |
4 |
['SnirBroshi', 'github-actions', 'thorimur', 'vihdzp'] |
thorimur assignee:thorimur |
1-79417 1 day ago |
1-79450 1 day ago |
8-76821 8 days |
| 30668 |
astrainfinita author:astrainfinita |
feat: `QuotLike` |
This typeclass is primarily for use by type synonyms of `Quot` and `Quotient`. Using `QuotLike` API for type synonyms of `Quot` and `Quotient` will avoid defeq abuse caused by directly using `Quot` and `Quotient` APIs.
This PR also adds some typeclasses to support different ways to find the quotient map that should be used. See the documentation comments of these typeclasses for examples of usage.
---
It's not a typical design to use these auxiliary typeclasses and term elaborators, but I haven't found a better way to support these notations.
Some of the naming may need to be discussed. For example:
- `⟦·⟧` is currently called `mkQ` in names. This distinguishes it from other `.mk`s and makes it possible to write the quotient map as `mkQ` `mkQ'` `mkQ_ h`. But this will also require changing the old lemma names.
- It would be helpful if the names of new type classes explained their functionality better.
- Maybe `QuotLike` isn't the appropriate name. It may suggest that this typeclass is similar to `FunLike` and `SetLike`, but it is not.
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/migrate.20to.20.60QuotLike.60.20API)
This PR continues the work from #16421.
Original PR: https://github.com/leanprover-community/mathlib4/pull/16421 |
t-data
awaiting-zulip
RFC
|
743/0 |
Mathlib.lean,Mathlib/Data/QuotLike.lean,MathlibTest/QuotLike.lean |
3 |
13 |
['YaelDillies', 'astrainfinita', 'github-actions', 'vihdzp'] |
nobody |
0-54407 15 hours ago |
5-63990 5 days ago |
0-81 1 minute |
| 11800 |
JADekker author:JADekker |
feat : Define KappaLindelöf spaces |
Define KappaLindelöf spaces by following the first one-third of the API for Lindelöf spaces. The remainder will be added in a future PR.
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-topology
merge-conflict
please-adopt
|
301/2 |
Mathlib.lean,Mathlib/Topology/Compactness/KappaLindelof.lean,Mathlib/Topology/Compactness/Lindelof.lean |
3 |
38 |
['ADedecker', 'JADekker', 'PatrickMassot', 'StevenClontz', 'adomani', 'github-actions', 'grunweg', 'kim-em', 'urkud'] |
nobody |
403-65102 1 year ago |
404-677 1 year ago |
119-10687 119 days |
| 17623 |
FR-vdash-bot author:FR-vdash-bot |
feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas |
Some lemmas in `Algebra.Order.GroupWithZero.Unbundled` have incorrect or unsatisfactory names, or assumptions that can be omitted using `ZeroLEOneClass`. The lemmas added in this PR are versions of existing lemmas that use the correct or better name or `ZeroLEOneClass` to omit an assumption. The original lemmas will be deprecated in #17593.
| New name | Old name |
|-------------------------|-------------------------|
| `mul_le_one_left₀` | `Left.mul_le_one_of_le_of_le` |
| `mul_lt_one_of_le_of_lt_left₀` (`0 ≤ ·` version) / `mul_lt_one_of_le_of_lt_of_pos_left` | `Left.mul_lt_of_le_of_lt_one_of_pos` |
| `mul_lt_one_of_lt_of_le_left₀` | `Left.mul_lt_of_lt_of_le_one_of_nonneg` |
| `mul_le_one_right₀` | `Right.mul_le_one_of_le_of_le` |
| `mul_lt_one_of_lt_of_le_right₀` (`0 ≤ ·` version) / `mul_lt_one_of_lt_of_le_of_pos_right` | `Right.mul_lt_one_of_lt_of_le_of_pos` |
| `mul_lt_one_of_le_of_lt_right₀` | `Right.mul_lt_one_of_le_of_lt_of_nonneg` |
The following lemmas use `ZeroLEOneClass`.
| New name | Old name |
|-------------------------|-------------------------|
| `(Left.)one_le_mul₀` | `Left.one_le_mul_of_le_of_le` |
| `Left.one_lt_mul_of_le_of_lt₀` | `Left.one_lt_mul_of_le_of_lt_of_pos` |
| `Left.one_lt_mul_of_lt_of_le₀` | `Left.lt_mul_of_lt_of_one_le_of_nonneg` / `one_lt_mul_of_lt_of_le` (still there) |
| `(Left.)one_lt_mul₀` | |
| `Right.one_le_mul₀` | `Right.one_le_mul_of_le_of_le` |
| `Right.one_lt_mul_of_lt_of_le₀` | `Right.one_lt_mul_of_lt_of_le_of_pos` |
| `Right.one_lt_mul_of_le_of_lt₀` | `Right.one_lt_mul_of_le_of_lt_of_nonneg` / `one_lt_mul_of_le_of_lt` (still there) / `one_lt_mul` (still there) |
| `Right.one_lt_mul₀` | `Right.one_lt_mul_of_lt_of_lt` |
---
Split from #17593.
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-order
t-algebra
merge-conflict
label:t-algebra$ |
146/44 |
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean |
2 |
11 |
['FR-vdash-bot', 'YaelDillies', 'github-actions', 'j-loreaux'] |
nobody |
338-38352 11 months ago |
338-38352 11 months ago |
33-64877 33 days |
| 8370 |
eric-wieser author:eric-wieser |
refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` |
This argument is still needed for almost all the lemmas, which means it can longer be found by unification.
We keep around `expSeries 𝕂 A`, as it's needed for talking about the radius of convergence over different base fields.
This is a prerequisite for #8372, as we can't merge the functions until they have the same interface.\
Zulip thread: [#mathlib4 > Real.exp @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Real.2Eexp/near/401602245)
---
[](https://gitpod.io/from-referrer/)
This is started from the mathport output on https://github.com/leanprover-community/mathlib/pull/19244 |
awaiting-zulip
t-analysis
merge-conflict
|
432/387 |
Mathlib/Analysis/CStarAlgebra/Exponential.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean,Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean,Mathlib/Analysis/NormedSpace/DualNumber.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean |
11 |
29 |
['YaelDillies', 'eric-wieser', 'girving', 'github-actions', 'j-loreaux', 'kbuzzard', 'leanprover-community-bot-assistant', 'urkud'] |
nobody |
182-80129 5 months ago |
194-22359 6 months ago |
29-60989 29 days |
| 15651 |
TpmKranz author:TpmKranz |
feat(Computability/NFA): operations for Thompson's construction |
Lays the groundwork for a proof of equivalence of RE and NFA, w.r.t. described language. Actual connection to REs comes later, after the groundwork for the opposite direction has been laid.
Third chunk of #12648
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
merge-conflict
awaiting-author
|
307/5 |
Mathlib/Computability/NFA.lean |
1 |
15 |
['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte'] |
nobody |
158-24235 5 months ago |
158-24236 5 months ago |
45-84611 45 days |
| 22361 |
rudynicolop author:rudynicolop |
feat(Computability/NFA): nfa closure properties |
Add the closure properties union, intersection and reversal for NFA.
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
merge-conflict
awaiting-author
|
218/2 |
Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean |
2 |
90 |
['EtienneC30', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] |
EtienneC30 assignee:EtienneC30 |
158-23309 5 months ago |
158-23311 5 months ago |
39-67601 39 days |
| 17458 |
urkud author:urkud |
refactor(Algebra/Group): make `IsUnit` a typeclass |
Also change some lemmas to assume `[IsUnit _]` instead of `[Invertible _]`.
Motivated by potential non-defeq diamonds in #14986, see also [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Invertible.20and.20data)
I no longer plan to merge this PR, but I'm going to cherry-pick some changes to a new PR before closing this one.
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-algebra
merge-conflict
label:t-algebra$ |
82/72 |
Mathlib/Algebra/CharP/Invertible.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Units.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Affine/Isometry.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/GroupTheory/Submonoid/Inverses.lean,Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean,Mathlib/LinearAlgebra/AffineSpace/Combination.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean,Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean,Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean |
26 |
12 |
['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'urkud'] |
nobody |
111-68378 3 months ago |
111-68378 3 months ago |
0-66650 18 hours |
| 25218 |
kckennylau author:kckennylau |
feat(AlgebraicGeometry): Tate normal form of elliptic curves |
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
new-contributor
t-algebraic-geometry
merge-conflict
|
291/26 |
Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean |
5 |
31 |
['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau', 'leanprover-community-bot-assistant'] |
nobody |
111-67216 3 months ago |
111-67217 3 months ago |
6-51040 6 days |
| 28298 |
thorimur author:thorimur |
chore: dedent `to_additive` docstrings |
This PR uses automation to dedent `to_additive` docstrings throughout Mathlib. It does not lint against indentation or in any way enforce indentation standards for future docstrings. The convention was chosen in accordance with the discussion and polls at [this Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Poll.3A.20Indentation.20style.20for.20.60to_additive.60.20docstrings/with/534285603).
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
merge-conflict
documentation
|
949/949 |
Mathlib/Algebra/BigOperators/Fin.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/BigOperators/Finsupp/Basic.lean,Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean,Mathlib/Algebra/BigOperators/Group/List/Basic.lean,Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean,Mathlib/Algebra/BigOperators/Pi.lean,Mathlib/Algebra/Category/Grp/Basic.lean,Mathlib/Algebra/Category/Grp/FilteredColimits.lean,Mathlib/Algebra/Category/Grp/Limits.lean,Mathlib/Algebra/Category/Grp/Ulift.lean,Mathlib/Algebra/Category/MonCat/Basic.lean,Mathlib/Algebra/Category/MonCat/FilteredColimits.lean,Mathlib/Algebra/Category/MonCat/Limits.lean,Mathlib/Algebra/Category/Semigrp/Basic.lean,Mathlib/Algebra/Free.lean,Mathlib/Algebra/FreeMonoid/Basic.lean,Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/Pi.lean,Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Algebra/Group/Basic.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Embedding.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Equiv/Opposite.lean,Mathlib/Algebra/Group/Even.lean,Mathlib/Algebra/Group/Hom/Basic.lean,Mathlib/Algebra/Group/Hom/Defs.lean,Mathlib/Algebra/Group/Hom/Instances.lean,Mathlib/Algebra/Group/Indicator.lean,Mathlib/Algebra/Group/Pi/Lemmas.lean,Mathlib/Algebra/Group/Pi/Units.lean,Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/Group/Pointwise/Set/Basic.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Group/Subgroup/Basic.lean,Mathlib/Algebra/Group/Subgroup/Defs.lean,Mathlib/Algebra/Group/Subgroup/Ker.lean,Mathlib/Algebra/Group/Subgroup/Lattice.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Subgroup/Pointwise.lean,Mathlib/Algebra/Group/Submonoid/Basic.lean,Mathlib/Algebra/Group/Submonoid/BigOperators.lean,Mathlib/Algebra/Group/Submonoid/Defs.lean,Mathlib/Algebra/Group/Submonoid/Membership.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Subsemigroup/Basic.lean,Mathlib/Algebra/Group/Subsemigroup/Operations.lean,Mathlib/Algebra/Group/UniqueProds/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/Algebra/Group/Units/Opposite.lean,Mathlib/Algebra/Notation/Pi/Basic.lean,Mathlib/Algebra/Opposites.lean,Mathlib/Algebra/Order/BigOperators/Group/List.lean,Mathlib/Algebra/Order/Group/Abs.lean,Mathlib/Algebra/Order/Group/Basic.lean,Mathlib/Algebra/Order/Group/Cone.lean,Mathlib/Algebra/Order/Group/OrderIso.lean,Mathlib/Algebra/Order/Group/Units.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Order/Monoid/Basic.lean,Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean,Mathlib/Algebra/Order/Monoid/Submonoid.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/Algebra/Order/Monoid/Units.lean,Mathlib/Algebra/Order/Pi.lean,Mathlib/Algebra/Regular/Defs.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Fintype/BigOperators.lean,Mathlib/Data/Set/MulAntidiagonal.lean,Mathlib/Data/Set/SMulAntidiagonal.lean,Mathlib/Data/Vector/Basic.lean,Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean,Mathlib/Dynamics/FixedPoints/Prufer.lean,Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean,Mathlib/GroupTheory/Complement.lean,Mathlib/GroupTheory/Congruence/Basic.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/GroupTheory/Coprod/Basic.lean,Mathlib/GroupTheory/Coset/Basic.lean,Mathlib/GroupTheory/Divisible.lean,Mathlib/GroupTheory/EckmannHilton.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/GroupTheory/FreeGroup/Reduce.lean,Mathlib/GroupTheory/GroupAction/Basic.lean,Mathlib/GroupTheory/GroupAction/Blocks.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/FixedPoints.lean,Mathlib/GroupTheory/GroupAction/Hom.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/Primitive.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean |
141 |
10 |
['eric-wieser', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot', 'thorimur'] |
nobody |
71-9310 2 months ago |
71-83082 2 months ago |
0-61617 17 hours |
| 28803 |
astrainfinita author:astrainfinita |
refactor: unbundle algebra from `ENormed*` |
Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`.
This PR continues the work from #23961.
- Change `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` so they no longer carry algebraic data.
- Deprecate `ESeminormed(Add)CommMonoid` and `ENormed(Add)CommMonoid` in favor of `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` with a commutative algebraic typeclass.
|Old|New|
|---|---|
| `[ESeminormed(Add)(Comm)Monoid E]` | `[(Add)(Comm)Monoid E] [ESeminormed(Add)Monoid E]` |
| `[ENormed(Add)(Comm)Monoid]` | `[(Add)(Comm)Monoid E] [ENormed(Add)Monoid]` |
See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2328803.20refactor.3A.20unbundle.20algebra.20from.20.60ENormed*.60/with/536024350)
------------
- [x] depends on: #28813 |
awaiting-zulip
slow-typeclass-synthesis
t-algebra
t-analysis
merge-conflict
label:t-algebra$ |
80/63 |
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/Normed/Group/InfiniteSum.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean,Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean,Mathlib/MeasureTheory/Function/L1Space/Integrable.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean |
14 |
28 |
['astrainfinita', 'bryangingechen', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] |
grunweg assignee:grunweg |
51-82861 1 month ago |
51-82862 1 month ago |
0-20585 5 hours |
| 28925 |
grunweg author:grunweg |
chore: remove `linear_combination'` tactic |
When `linear_combination` was refactored in #15899, the old code was kept as the `linear_combination'` tactic, for easier migration. The consensus of the zulip discussion ([#mathlib4 > Narrowing the scope of `linear_combination` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Narrowing.20the.20scope.20of.20.60linear_combination.60/near/470237816)) was to wait, and "revisit this once people have experienced the various tactics in practice".
One year later, the old tactic has almost no uses: it is unused in mathlib; [searching on github](https://github.com/search?q=linear_combination%27%20path%3A*.lean&type=code) yields 37 hits --- all of which are in various forks of mathlib. Thus, removing this tactic seems appropriate.
---
Do not merge before the zulip discussion has concluded!
[](https://gitpod.io/from-referrer/)
|
file-removed
awaiting-zulip
merge-conflict
|
0/564 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/LinearCombination'.lean,Mathlib/Tactic/Linter/UnusedTactic.lean,MathlibTest/linear_combination'.lean |
5 |
4 |
['euprunin', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot'] |
nobody |
8-60071 8 days ago |
8-60072 8 days ago |
0-1 1 second |
| 17518 |
grunweg author:grunweg |
feat: lint on declarations mentioning `Invertible` or `Unique` |
Using the same infrastructure as for #10235. Depends on that PR to land first, and also (for the first lint) a zulip discussion if that change is desired/about the best way to enact it.
---
- [ ] depends on: #10235 |
awaiting-zulip
t-linter
merge-conflict
blocked-by-other-PR
|
149/7 |
Mathlib.lean,Mathlib/Algebra/MvPolynomial/PDeriv.lean,Mathlib/Computability/Halting.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/GroupTheory/Perm/DomMulAct.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/NumberTheory/JacobiSum/Basic.lean,Mathlib/Order/Heyting/Regular.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/UnusedAssumptionInType.lean |
13 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mergify'] |
nobody |
356-18821 11 months ago |
382-7343 1 year ago* |
0-0 0 seconds* |
| 15654 |
TpmKranz author:TpmKranz |
feat(Computability): language-preserving maps between NFA and RE |
Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs
Last chunk of #12648
---
- [ ] depends on: #15651
- [ ] depends on: #15649
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
new-contributor
merge-conflict
blocked-by-other-PR
|
985/2 |
Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib |
7 |
3 |
['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte'] |
nobody |
172-1629 5 months ago |
172-1634 5 months ago |
0-179 2 minutes |