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 |
| 21624 |
sinhp author:sinhp |
feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories |
Given a family of closed monoidal categories, we show that the product of these categories
is a closed monoidal category with the pointwise monoidal structure.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-category-theory
awaiting-author
|
144/0 |
Mathlib.lean,Mathlib/CategoryTheory/Pi/Basic.lean,Mathlib/CategoryTheory/Pi/Monoidal.lean,Mathlib/CategoryTheory/Pi/MonoidalClosed.lean |
4 |
19 |
['TwoFX', 'YaelDillies', 'b-mehta', 'github-actions', 'jcommelin', 'sinhp'] |
nobody |
35-48316 1 month ago |
35-67149 1 month ago |
54-54882 54 days |
| 24450 |
justus-springer author:justus-springer |
feat(Algebra/Order/Nonneg): A finite module is finite over the nonnegative scalars |
From Toric
---
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
new-contributor
t-algebra
label:t-algebra$ |
21/3 |
Mathlib/Algebra/Order/Nonneg/Module.lean |
1 |
3 |
['YaelDillies', 'github-actions'] |
nobody |
2-53677 2 days ago |
2-53677 2 days ago |
14-30240 14 days |
| 24205 |
meithecatte author:meithecatte |
chore(RegularExpressions): clarify that TODO has pending PRs |
The TODO on equivalence between regular expressions and DFAs seems to be particularly appealing to new contributors, having spawned multiple competing PRs working towards that goal.
It is also one where a new contributor is quite likely to produce a design that is not inline with mathlib's API design philosophy and will require a lot of guidance, which causes the PRs to languish in review.
Reword the TODO to make it less likely that the situation gets worse.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-computability
new-contributor
easy
|
2/1 |
Mathlib/Computability/RegularExpressions.lean |
1 |
7 |
['YaelDillies', 'github-actions', 'meithecatte', 'urkud'] |
nobody |
2-45556 2 days ago |
2-45556 2 days ago |
24-12960 24 days |
| 24673 |
adomani author:adomani |
fix(docstring linter): inspect also internal docstrings |
This omission was pointed out in #24532.
---
[](https://gitpod.io/from-referrer/)
|
t-linter
maintainer-merge
|
81/32 |
Mathlib/Algebra/Homology/ShortComplex/Homology.lean,Mathlib/CategoryTheory/EpiMono.lean,Mathlib/Tactic/FunProp/Types.lean,Mathlib/Tactic/Linter/DocString.lean,Mathlib/Tactic/MkIffOfInductiveProp.lean,Mathlib/Topology/CWComplex/Classical/Finite.lean,MathlibTest/DocString.lean |
7 |
12 |
['adomani', 'github-actions', 'grunweg'] |
grunweg assignee:grunweg |
2-15463 2 days ago |
2-15464 2 days ago |
5-25243 5 days |
| 23961 |
FR-vdash-bot author:FR-vdash-bot |
refactor: unbundle algebra from `ENormed*` |
Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`.
---
[](https://gitpod.io/from-referrer/)
|
slow-typeclass-synthesis
maintainer-merge
t-algebra
t-analysis
merge-conflict
label:t-algebra$ |
32/25 |
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean |
5 |
11 |
['FR-vdash-bot', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-bot-assistant'] |
nobody |
7-16743 7 days ago |
14-22309 14 days ago |
17-72244 17 days |
| 21751 |
vihdzp author:vihdzp |
refactor(SetTheory/Ordinal/Arithmetic): rework `Ordinal.pred` API |
This PR does the following:
- give a simpler definition of `Ordinal.pred`
- replace `¬ ∃ a, o = succ a` and `∀ a, o ≠ succ a` by `IsSuccPrelimit o` throughout
- improve theorem names
---
There's a legitimate question of whether we even want `Ordinal.pred` (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ordinal.2Epred)) but this should be a good change in the meanwhile regardless.
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
merge-conflict
|
102/67 |
Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean |
2 |
13 |
['YaelDillies', 'github-actions', 'grunweg', 'vihdzp'] |
nobody |
7-1397 7 days ago |
53-66424 1 month ago |
36-50134 36 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 |
| 21624 |
sinhp author:sinhp |
feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories |
Given a family of closed monoidal categories, we show that the product of these categories
is a closed monoidal category with the pointwise monoidal structure.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-category-theory
awaiting-author
|
144/0 |
Mathlib.lean,Mathlib/CategoryTheory/Pi/Basic.lean,Mathlib/CategoryTheory/Pi/Monoidal.lean,Mathlib/CategoryTheory/Pi/MonoidalClosed.lean |
4 |
19 |
['TwoFX', 'YaelDillies', 'b-mehta', 'github-actions', 'jcommelin', 'sinhp'] |
nobody |
35-48316 1 month ago |
35-67149 1 month ago |
54-54882 54 days |
| 24450 |
justus-springer author:justus-springer |
feat(Algebra/Order/Nonneg): A finite module is finite over the nonnegative scalars |
From Toric
---
[](https://gitpod.io/from-referrer/)
|
large-import
maintainer-merge
new-contributor
t-algebra
label:t-algebra$ |
21/3 |
Mathlib/Algebra/Order/Nonneg/Module.lean |
1 |
3 |
['YaelDillies', 'github-actions'] |
nobody |
2-53677 2 days ago |
2-53677 2 days ago |
14-30240 14 days |
| 24205 |
meithecatte author:meithecatte |
chore(RegularExpressions): clarify that TODO has pending PRs |
The TODO on equivalence between regular expressions and DFAs seems to be particularly appealing to new contributors, having spawned multiple competing PRs working towards that goal.
It is also one where a new contributor is quite likely to produce a design that is not inline with mathlib's API design philosophy and will require a lot of guidance, which causes the PRs to languish in review.
Reword the TODO to make it less likely that the situation gets worse.
---
[](https://gitpod.io/from-referrer/)
|
maintainer-merge
t-computability
new-contributor
easy
|
2/1 |
Mathlib/Computability/RegularExpressions.lean |
1 |
7 |
['YaelDillies', 'github-actions', 'meithecatte', 'urkud'] |
nobody |
2-45556 2 days ago |
2-45556 2 days ago |
24-12960 24 days |
| 24673 |
adomani author:adomani |
fix(docstring linter): inspect also internal docstrings |
This omission was pointed out in #24532.
---
[](https://gitpod.io/from-referrer/)
|
t-linter
maintainer-merge
|
81/32 |
Mathlib/Algebra/Homology/ShortComplex/Homology.lean,Mathlib/CategoryTheory/EpiMono.lean,Mathlib/Tactic/FunProp/Types.lean,Mathlib/Tactic/Linter/DocString.lean,Mathlib/Tactic/MkIffOfInductiveProp.lean,Mathlib/Topology/CWComplex/Classical/Finite.lean,MathlibTest/DocString.lean |
7 |
12 |
['adomani', 'github-actions', 'grunweg'] |
grunweg assignee:grunweg |
2-15463 2 days ago |
2-15464 2 days ago |
5-25243 5 days |
| 24312 |
YaelDillies author:YaelDillies |
feat: more lemmas about torsion-free monoids |
The new imports just come from making `#min_imports` and `mk_iff` available earlier.
From Toric
---
[](https://gitpod.io/from-referrer/)
|
toric
large-import
maintainer-merge
t-algebra
label:t-algebra$ |
117/17 |
Mathlib/Algebra/Group/Pi/Lemmas.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Group/Subgroup/Basic.lean,Mathlib/Algebra/Group/Torsion.lean,Mathlib/Algebra/Lie/Weights/Chain.lean,Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean,Mathlib/GroupTheory/OrderOfElement.lean,Mathlib/GroupTheory/Torsion.lean,Mathlib/Topology/Instances/ZMultiples.lean |
9 |
7 |
['YaelDillies', 'b-mehta', 'github-actions', 'grunweg'] |
b-mehta assignee:b-mehta |
0-16790 4 hours ago |
0-18890 5 hours ago |
20-37964 20 days |
| 24855 |
euprunin author:euprunin |
feat: register more tactics for `hint` |
The following example shows test cases that `hint` now supports, which were unsupported prior to this PR:
```
import Mathlib
-- The tactics registered in this PR
register_hint compute_degree
register_hint field_simp
register_hint finiteness
-- "hint" now correctly suggests "compute_degree" which closes the goal (no closing tactic suggested prior to this PR)
open Polynomial in
example : natDegree ((X + 1) : Nat[X]) ≤ 1 := by hint
-- "hint" now correctly suggests "field_simp" which closes the goal (no closing tactic suggested prior to this PR)
example (R : Type) (a b : R) [CommRing R] (u₁ : Rˣ) : a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁ := by hint
-- "hint" now correctly suggests "finiteness" which closes the goal (no closing tactic suggested prior to this PR)
example (a : ℝ) : (ENNReal.ofReal (1 + a ^ 2))⁻¹ < ⊤ := by hint
``` |
maintainer-merge
t-meta
|
15/0 |
Mathlib/Tactic/ComputeDegree.lean,Mathlib/Tactic/FieldSimp.lean,Mathlib/Tactic/Finiteness.lean |
3 |
4 |
['euprunin', 'github-actions', 'grunweg'] |
nobody |
0-3974 1 hour ago |
0-6341 1 hour ago |
0-15731 4 hours |
| 23961 |
FR-vdash-bot author:FR-vdash-bot |
refactor: unbundle algebra from `ENormed*` |
Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`.
---
[](https://gitpod.io/from-referrer/)
|
slow-typeclass-synthesis
maintainer-merge
t-algebra
t-analysis
merge-conflict
label:t-algebra$ |
32/25 |
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean |
5 |
11 |
['FR-vdash-bot', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-bot-assistant'] |
nobody |
7-16743 7 days ago |
14-22309 14 days ago |
17-72244 17 days |
| 21751 |
vihdzp author:vihdzp |
refactor(SetTheory/Ordinal/Arithmetic): rework `Ordinal.pred` API |
This PR does the following:
- give a simpler definition of `Ordinal.pred`
- replace `¬ ∃ a, o = succ a` and `∀ a, o ≠ succ a` by `IsSuccPrelimit o` throughout
- improve theorem names
---
There's a legitimate question of whether we even want `Ordinal.pred` (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ordinal.2Epred)) but this should be a good change in the meanwhile regardless.
[](https://gitpod.io/from-referrer/)
|
t-set-theory
maintainer-merge
merge-conflict
|
102/67 |
Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean |
2 |
13 |
['YaelDillies', 'github-actions', 'grunweg', 'vihdzp'] |
nobody |
7-1397 7 days ago |
53-66424 1 month ago |
36-50134 36 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 |
| 23866 |
kim-em author:kim-em |
chore: remove `[AtLeastTwo n]` hypothesis from the `NatCast` to `OfNat` instance |
This PR observes that we can change
```
instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] : OfNat R n
```
to
```
instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] : OfNat R n
```
with minimal fall-out.
A follow-up PR #23867 then observes that we can remove nearly all the `[Nat.AtLeastTwo n]` hypotheses in Mathlib.
This is slightly dangerous -- it does make it more likely that we'll generate non-defeq instances, but it appears to happen very rarely.
However, it will make life slightly easier for something Leo and I are trying to do with `grind` and Grobner bases (we'd like to be able to assume types we consume have `[∀ n, OfNat α n]`, which is possible with this change, but not without...).
Zulip thread: [#PR reviews > #23866 and #23867, removing most `[Nat.AtLeastTwo n]` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2323866.20and.20.2323867.2C.20removing.20most.20.60.5BNat.2EAtLeastTwo.20n.5D.60/near/511157297) |
awaiting-zulip |
21/26 |
Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/Data/Nat/Cast/Defs.lean,Mathlib/Data/Nat/Cast/Order/Basic.lean |
3 |
3 |
['eric-wieser', 'github-actions', 'urkud'] |
nobody |
34-12027 1 month ago |
34-12116 1 month ago |
0-23929 6 hours |
| 24151 |
robertmaxton42 author:robertmaxton42 |
chore (Limits/Pullback): fix misnamed `pullback_fst_iso_of_right_iso` |
`pullback_snd_iso_of_right_iso` in fact proves that `IsIso pullback.fst`; change the lemma name to match the content.
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-category-theory
easy
|
1/1 |
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Iso.lean |
1 |
6 |
['github-actions', 'grunweg', 'robertmaxton42'] |
nobody |
20-12027 20 days ago |
20-12027 20 days ago |
0-36289 10 hours |
| 24409 |
urkud author:urkud |
chore(*): fix `nmem` vs `not_mem` names |
---
There are some missing/buggy deprecations, I'm going to fix them later today or tomorrow.
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
tech debt
delegated
|
317/176 |
Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean,Mathlib/Algebra/Group/Indicator.lean,Mathlib/Algebra/Group/Support.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Order/Group/Indicator.lean,Mathlib/Algebra/Polynomial/AlgebraMap.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Analysis/Calculus/BumpFunction/Basic.lean,Mathlib/Analysis/Calculus/DSlope.lean,Mathlib/Analysis/Calculus/Deriv/Basic.lean,Mathlib/Analysis/Calculus/Deriv/Support.lean,Mathlib/Analysis/Calculus/FDeriv/Basic.lean,Mathlib/Analysis/Calculus/Rademacher.lean,Mathlib/Analysis/Complex/RemovableSingularity.lean,Mathlib/Analysis/Convex/Cone/InnerDual.lean,Mathlib/Analysis/Convex/Cone/Proper.lean,Mathlib/Analysis/Convolution.lean,Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean,Mathlib/Data/LocallyFinsupp.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Data/Set/Insert.lean,Mathlib/Dynamics/Ergodic/Conservative.lean,Mathlib/Dynamics/Ergodic/Ergodic.lean,Mathlib/Dynamics/Ergodic/Function.lean,Mathlib/Dynamics/PeriodicPts/Defs.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/PartitionOfUnity.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/FreeModule/PID.lean,Mathlib/LinearAlgebra/PID.lean,Mathlib/LinearAlgebra/RootSystem/Base.lean,Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean,Mathlib/MeasureTheory/Function/ContinuousMapDense.lean,Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean,Mathlib/MeasureTheory/Function/L2Space.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean,Mathlib/MeasureTheory/Integral/Average.lean,Mathlib/MeasureTheory/Integral/Bochner/Set.lean,Mathlib/MeasureTheory/Integral/Layercake.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean,Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean,Mathlib/MeasureTheory/Measure/AddContent.lean,Mathlib/MeasureTheory/Measure/DiracProba.lean,Mathlib/MeasureTheory/Measure/Haar/Unique.lean,Mathlib/MeasureTheory/Measure/Restrict.lean,Mathlib/MeasureTheory/Measure/WithDensity.lean,Mathlib/MeasureTheory/OuterMeasure/AE.lean,Mathlib/MeasureTheory/SetSemiring.lean,Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean,Mathlib/Order/Filter/Cocardinal.lean,Mathlib/Order/Filter/Cofinite.lean,Mathlib/Order/Filter/Tendsto.lean,Mathlib/Order/Filter/Ultrafilter/Basic.lean,Mathlib/Probability/Distributions/Uniform.lean,Mathlib/Probability/Kernel/Basic.lean,Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean,Mathlib/RingTheory/AdicCompletion/LocalRing.lean,Mathlib/RingTheory/Ideal/Maximal.lean,Mathlib/RingTheory/LaurentSeries.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/Spectrum/Maximal/Localization.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/Topology/Algebra/InfiniteSum/Group.lean,Mathlib/Topology/Algebra/Module/Cardinality.lean,Mathlib/Topology/Algebra/Support.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean,Mathlib/Topology/Order/Basic.lean,Mathlib/Topology/UrysohnsLemma.lean |
77 |
3 |
['b-mehta', 'github-actions', 'jcommelin', 'mathlib-bors'] |
nobody |
14-42247 14 days ago |
14-42247 14 days ago |
0-55045 15 hours |
| 23658 |
grunweg author:grunweg |
feat: require that real or complex models with corners have convex interior |
Follow-up to #18403.
---
- [ ] depends on: #23657
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-differential-geometry
blocked-by-other-PR
WIP
|
130/18 |
Mathlib/Geometry/Manifold/Instances/Real.lean,Mathlib/Geometry/Manifold/IsManifold/Basic.lean |
2 |
3 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] |
nobody |
14-35000 14 days ago |
14-35000 14 days ago |
0-9 9 seconds |
| 24083 |
Parcly-Taxel author:Parcly-Taxel |
feat: the `longFileHard` linter |
@kim-em [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/long.20files/near/510548946):
> Yes, we don't have a sustainable mechanism that will prevent long files creeping back, unless when we reach "no long file", we turn it into an non-overridable error...!
>
> It would be great to have such a mechanism, of course, because I agree, of course, that this would be annoying to contributors (and doubly annoying to reviewers if they had to remind contributors not to "compress" things). |
awaiting-zulip
t-linter
|
72/1 |
Mathlib/Tactic/Linter/Style.lean,MathlibTest/LongFile.lean,lakefile.lean |
3 |
2 |
['github-actions', 'grunweg'] |
nobody |
10-46474 10 days ago |
28-22778 28 days ago |
0-5347 1 hour |
| 24396 |
JovanGerb author:JovanGerb |
feat(Order/Defs): refactor in preparation of `to_dual` attribute |
When the `to_dual` attribute lands in Mathlib, we will tag many lemmas about order with this tag, which will automatically give us the dual statements. This PR prepares for this by
- moving dual declarations closer together
- replacing occurrences of `>` and `≥` with `<` and `≤`
- consistently applying a new naming convention that helps us to name dual lemmas: we use the keywords `ge` and `gt` in place of `le` and `lt` to indicate that the same pair `a, b` in `a < b` is in the opposite order to the order in which it appeared the first time.
- when we have to disambiguate the order of the argument to `<` or `≤`, we sometimes use `gt` or `ge` instead of `lt` or `le`. We also use this to get rid of many primed lemma names.
This is a copy of #24376, but it doesn't remove the old lemma names, so doesn't require making changes in >500 files. deprecating these lemmas will be left to a future PR.
[#mathlib4 > naming convention for ≤ and <](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/naming.20convention.20for.20.E2.89.A4.20and.20.3C)
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-order
|
248/230 |
Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean,Mathlib/Algebra/Polynomial/Degree/Domain.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Bool/Basic.lean,Mathlib/Data/Char.lean,Mathlib/Data/Complex/Order.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Int/Order/Basic.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Nat/Factorization/Defs.lean,Mathlib/Data/Nat/Find.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/Num/Lemmas.lean,Mathlib/Data/Num/ZNum.lean,Mathlib/Data/PSigma/Order.lean,Mathlib/Data/Prod/Lex.lean,Mathlib/Data/Real/Basic.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/Data/Sigma/Order.lean,Mathlib/Data/String/Basic.lean,Mathlib/Data/Sum/Order.lean,Mathlib/GroupTheory/MonoidLocalization/Order.lean,Mathlib/NumberTheory/Zsqrtd/Basic.lean,Mathlib/Order/Antisymmetrization.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Booleanisation.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/Order/Defs/PartialOrder.lean,Mathlib/Order/RelClasses.lean,Mathlib/Order/WithBot.lean,Mathlib/Probability/Martingale/Upcrossing.lean,Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean,Mathlib/SetTheory/Game/Basic.lean,Mathlib/SetTheory/Ordinal/Basic.lean,Mathlib/SetTheory/Ordinal/Notation.lean,Mathlib/SetTheory/Surreal/Basic.lean,Mathlib/Tactic/Linarith/Frontend.lean,MathlibTest/linarith.lean |
43 |
4 |
['JovanGerb', 'bryangingechen', 'github-actions', 'leanprover-community-bot-assistant'] |
bryangingechen assignee:bryangingechen |
10-35082 10 days ago |
11-9025 11 days ago |
5-75236 5 days |
| 19872 |
YaelDillies author:YaelDillies |
chore(GroupTheory/Index): rename `relindex` to `relIndex` |
---
- [x] depends on: #24044
[](https://gitpod.io/from-referrer/)
|
FLT
awaiting-zulip
t-algebra
label:t-algebra$ |
214/137 |
Mathlib/FieldTheory/Relrank.lean,Mathlib/GroupTheory/Commensurable.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/GroupTheory/GroupAction/Blocks.lean,Mathlib/GroupTheory/Index.lean,Mathlib/GroupTheory/IndexNormal.lean,Mathlib/GroupTheory/PGroup.lean,Mathlib/GroupTheory/Schreier.lean,Mathlib/GroupTheory/SchurZassenhaus.lean,Mathlib/GroupTheory/Sylow.lean,Mathlib/GroupTheory/Transfer.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/RingTheory/Ideal/Quotient/Index.lean |
13 |
19 |
['Ruben-VandeVelde', 'TwoFX', 'YaelDillies', 'alreadydone', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant', 'loefflerd', 'madvorak', 'mathlib4-dependent-issues-bot', 'tb65536'] |
nobody |
10-27730 10 days ago |
27-50985 27 days ago |
114-79171 114 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
awaiting-author
|
218/2 |
Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean |
2 |
89 |
['EtienneC30', 'b-mehta', 'github-actions', 'meithecatte', 'rudynicolop'] |
EtienneC30 assignee:EtienneC30 |
7-86035 7 days ago |
7-86117 7 days ago |
39-67601 39 days |
| 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 |
7-85904 7 days ago |
7-85913 7 days ago |
23-54870 23 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
awaiting-author
|
307/5 |
Mathlib/Computability/NFA.lean |
1 |
14 |
['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'meithecatte'] |
nobody |
7-85882 7 days ago |
7-85887 7 days ago |
45-84611 45 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
|
114/0 |
Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean |
2 |
57 |
['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'meithecatte', 'urkud'] |
EtienneC30 assignee:EtienneC30 |
7-85809 7 days ago |
7-85814 7 days ago |
48-67492 48 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 |
7-85215 7 days ago |
7-85850 7 days ago |
75-77754 75 days |
| 23048 |
scholzhannah author:scholzhannah |
feat: PartialEquiv on closed sets restricts to closed map |
This PR shows that a PartialEquiv that is continuous on both source and target restricts to a homeomorphism. It then uses that to show that a PartialEquiv with closed source and target and which is continuous on both the source and target restricts to a closed map.
---
See [this Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Generalizing.20.60PartialHomeomorph.60.3F) that will probably mean that I close this PR.
I need the latter statement to prove that one can transport a CW complex along a PartialEquiv. I had trouble finding a good spot for these statements; I hope this solution works.
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-topology
|
53/0 |
Mathlib.lean,Mathlib/Topology/PartialEquiv.lean |
2 |
3 |
['ADedecker', 'github-actions', 'scholzhannah'] |
ADedecker assignee:ADedecker |
0-23399 6 hours ago |
4-30175 4 days ago |
51-86236 51 days |
| 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 |
239-62937 7 months ago |
239-84912 7 months ago |
119-10687 119 days |
| 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 |
192-16656 6 months ago |
218-5178 7 months ago* |
0-0 0 seconds* |
| 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)
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-algebra
merge-conflict
label:t-algebra$ |
107/114 |
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/Definitions.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/Fintype.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean |
27 |
11 |
['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'urkud'] |
nobody |
179-40971 5 months ago |
179-40971 5 months ago |
0-66650 18 hours |
| 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 |
174-36187 5 months ago |
174-36187 5 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 |
18-77964 18 days ago |
30-20194 1 month ago |
29-60989 29 days |
| 21573 |
lambda-fairy author:lambda-fairy |
feat(Computability): regular languages are closed under reversal |
This PR proves that regular languages are closed under reversal.
It works by reversing the transitions in the NFA, and proving that the resulting automaton matches the reversed language. The argument proceeds by induction on the input word, ensuring that, at each character, the state sets for the forward and reverse automaton correspond to each other.
I also clean up the existing NFA module, which includes making the `M` argument implicit by default. I can revert that if it's controversial.
Thank you @Rob23oba for their help with the induction proof.
---
[](https://gitpod.io/from-referrer/)
|
awaiting-zulip
t-computability
merge-conflict
|
75/7 |
Mathlib/Computability/NFA.lean |
1 |
9 |
['github-actions', 'lambda-fairy', 'madvorak', 'meithecatte', 'tristan-f-r'] |
nobody |
7-85939 7 days ago |
7-85954 7 days ago |
24-86139 24 days |
| 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 |
7-85864 7 days ago |
7-85869 7 days ago |
0-179 2 minutes |
| 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 |
| 24215 |
BoltonBailey author:BoltonBailey |
chore: remove erw from WSeq.bind_assoc |
---
[](https://gitpod.io/from-referrer/)
|
tech debt |
9/2 |
Mathlib/Data/WSeq/Relation.lean |
1 |
5 |
['BoltonBailey', 'github-actions', 'kim-em', 'mathlib-bors'] |
nobody |
19-75059 19 days ago |
19-75059 19 days ago |
20-10139 20 days |
| 16408 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprecate `Order.Nat` |
* Move the two `Nat` instances and `bot_eq_zero` to `Order.BoundedOrder.Basic`. We also remove the TODO relating to #13092, as it was tried and it was agreed not to be a good idea.
* Move the other two lemmas in `Order.Nat` to `Data.Nat.Find`. |
will-close-soon
tech debt
|
35/54 |
Mathlib/Algebra/IsPrimePow.lean,Mathlib/Data/Finset/Grade.lean,Mathlib/Data/Finset/Lattice/Fold.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Nat/Cast/SetInterval.lean,Mathlib/Data/Nat/Find.lean,Mathlib/Data/Nat/SuccPred.lean,Mathlib/Data/Rat/Cast/Defs.lean,Mathlib/Order/BoundedOrder/Basic.lean,Mathlib/Order/Filter/AtTopBot/Basic.lean,Mathlib/Order/Nat.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/SetTheory/Cardinal/Order.lean |
13 |
8 |
['Parcly-Taxel', 'YaelDillies', 'github-actions', 'grunweg'] |
nobody |
14-3265 14 days ago |
14-3265 14 days ago |
30-22710 30 days |
| 23676 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprime `induction'` for localizations and quotients |
All these removed instances of `induction'` generate only one subgoal. In some cases `obtain` can be used.
The relevant instances were identified by adding the following to `Mathlib.Tactic.Cases`
```diff
diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean
index 4a60db6c551..08c06520879 100644
--- a/Mathlib/Tactic/Cases.lean
+++ b/Mathlib/Tactic/Cases.lean
@@ -122,6 +122,16 @@ elab (name := induction') "induction' " tgts:(Parser.Tactic.elimTarget,+)
g.assign result.elimApp
let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
(generalized := fvarIds) (toClear := targetFVarIds) (toTag := toTag)
+ let body ← inferType targets[0]!
+ let names : Array Format := if withArg.1.getArgs.size > 1 then
+ (withArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+ let gens : Array Format := if genArg.1.getArgs.size > 1 then
+ (genArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty
+ let inductor : Format := if usingArg.1.getArgs.size > 1 then
+ Syntax.prettyPrint usingArg.1.getArgs[1]! else "~"
+ if subgoals.toList.length ≤ 1 then
+ logInfoAt tgts m!"{body.getAppFn.setPPExplicit true} {inductor} {gens} {names} \
+ {subgoals.toList.length}"
setGoals <| (subgoals ++ result.others).toList ++ gs
/-- The `cases'` tactic is similar to the `cases` tactic in Lean 4 core, but the syntax for giving
```
and then examining [the output](https://github.com/leanprover-community/mathlib4/actions/runs/14270845291/job/40003467676). |
tech debt |
94/113 |
Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Pointwise/Stabilizer.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Limits/Types/Colimits.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Finsupp/BigOperators.lean,Mathlib/Data/Fintype/Quotient.lean,Mathlib/Data/List/Cycle.lean,Mathlib/Data/Nat/ChineseRemainder.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/FieldTheory/RatFunc/Basic.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/GroupTheory/OreLocalization/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Concrete.lean,Mathlib/GroupTheory/Perm/Sign.lean,Mathlib/GroupTheory/Torsion.lean,Mathlib/RingTheory/OreLocalization/Basic.lean,Mathlib/RingTheory/OreLocalization/Ring.lean,Mathlib/SetTheory/Surreal/Basic.lean |
25 |
10 |
['Parcly-Taxel', 'apnelson1', 'eric-wieser', 'github-actions', 'grunweg', 'urkud'] |
nobody |
10-51649 10 days ago |
10-52692 10 days ago |
38-27012 38 days |
| 23394 |
BoltonBailey author:BoltonBailey |
chore(Data/Int/WithZero): fix erw |
---
Removing an `erw`. This is my first time doing this, so please tell me if I am doing something wrong here (e.g. should the new lemma be `simp`?).
[](https://gitpod.io/from-referrer/)
|
tech debt |
5/3 |
Mathlib/Algebra/Group/WithOne/Defs.lean,Mathlib/Algebra/GroupWithZero/WithZero.lean,Mathlib/Data/Int/WithZero.lean |
3 |
13 |
['BoltonBailey', 'Ruben-VandeVelde', 'eric-wieser', 'github-actions'] |
nobody |
10-24248 10 days ago |
10-53205 10 days ago |
26-40847 26 days |
| 24492 |
Parcly-Taxel author:Parcly-Taxel |
chore: remove some adaptation notes |
|
tech debt |
15/32 |
Mathlib/Algebra/Homology/Single.lean,Mathlib/Combinatorics/Enumerative/DyckWord.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Int/Cast/Basic.lean,Mathlib/NumberTheory/DiophantineApproximation/Basic.lean |
5 |
12 |
['JovanGerb', 'Parcly-Taxel', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] |
nobody |
6-54580 6 days ago |
6-54596 6 days ago |
11-48854 11 days |
| 24493 |
urkud author:urkud |
chore(*): review `simp` lemmas for `piCongr*` equivs |
- remove `@[simp]` from lemmas with `Eq.rec` in the RHS;
- add missing `@[simp]` lemmas;
---
[](https://gitpod.io/from-referrer/)
|
tech debt |
55/12 |
Mathlib/Logic/Equiv/Basic.lean,Mathlib/Topology/Homeomorph/Lemmas.lean,Mathlib/Topology/UniformSpace/Equiv.lean |
3 |
3 |
['eric-wieser', 'github-actions', 'urkud'] |
nobody |
2-30251 2 days ago |
6-29840 6 days ago |
12-64259 12 days |