Would you like to help out at a PR, differently from reviewing? Here are some ideas:
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 |
12936 |
mattrobball author:mattrobball |
chore(Quiver.Opposite): make `Quiver.Hom.op/unop` `abbrev`'s |
These are wrappers around the constructor and projection for `Opposite Quiver.Hom _ _`. The projection itself is reducible and with structure eta built in to defeq it seems like we might be making Lean work harder than is necessary.
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict |
39/34 |
Mathlib/Algebra/Homology/ShortComplex/Homology.lean,Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean,Mathlib/CategoryTheory/Idempotents/Basic.lean,Mathlib/CategoryTheory/Limits/HasLimits.lean,Mathlib/CategoryTheory/Limits/Opposites.lean,Mathlib/CategoryTheory/Opposites.lean,Mathlib/CategoryTheory/Sites/CoverLifting.lean,Mathlib/CategoryTheory/Subobject/Comma.lean,Mathlib/CategoryTheory/Triangulated/Opposite.lean,Mathlib/Combinatorics/Quiver/Basic.lean |
10 |
9 |
['YaelDillies', 'kim-em', 'leanprover-bot', 'mattrobball'] |
nobody |
286-42798 9 months ago |
354-8790 11 months ago |
0-0 0 seconds |
10721 |
urkud author:urkud |
feat(Order/FunLike): define `PointwiseLE` |
- introduce a mixin class `DFunLike.PointwiseLE`, use it to define `DFunLike.instPartialOrder`;
- add a generic `DFunLike.orderEmbeddingCoe`
- add `DFunLike.PointwiseLE` instances here and there.
With this refactor and #13022, I'm going to generalize lemmas like `MeasureTheory.ae_mono` to `OuterMeasureClass`.
---
- [x] depends on: #12983
[](https://gitpod.io/from-referrer/) |
t-logic
t-order
merge-conflict
|
123/50 |
Mathlib.lean,Mathlib/Algebra/Order/Hom/Ring.lean,Mathlib/Data/DFinsupp/Order.lean,Mathlib/Data/Finsupp/Order.lean,Mathlib/Data/FunLike/Basic.lean,Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean,Mathlib/GroupTheory/Congruence.lean,Mathlib/Order/FunLike.lean,Mathlib/Order/Heyting/Hom.lean,Mathlib/Order/Hom/Basic.lean,Mathlib/Order/Hom/Bounded.lean,Mathlib/Order/Hom/CompleteLattice.lean,Mathlib/Topology/Order/Hom/Basic.lean |
13 |
48 |
['YaelDillies', 'dupuisf', 'leanprover-community-mathlib4-bot', 'urkud'] |
nobody |
286-42796 9 months ago |
308-23498 10 months ago |
64-12826 64 days |
8788 |
FMLJohn author:FMLJohn |
feat(Algebra/Module/GradeZeroModule): if `A` is a graded semiring and `M` is a graded `A`-module, then each grade of `M` is a module over the 0-th grade of `A`. |
---
- [ ] depends on: #8187
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
237/4 |
Mathlib.lean,Mathlib/Algebra/DirectSum/Internal.lean,Mathlib/Algebra/GradedMonoid.lean,Mathlib/Algebra/Module/GradeZeroModule.lean,Mathlib/RingTheory/GradedAlgebra/Basic.lean,Mathlib/RingTheory/GradedAlgebra/Noetherian.lean |
6 |
4 |
['FMLJohn', 'github-actions', 'leanprover-community-mathlib4-bot'] |
nobody |
286-42795 9 months ago |
320-30697 10 months ago |
0-0 0 seconds |
9339 |
FMLJohn author:FMLJohn |
feat (RingTheory/GradedAlgebra/HomogeneousIdeal): given a finitely generated homogeneous ideal of a graded semiring, construct a finite spanning set for the ideal which only contains homogeneous elements |
---
- [ ] depends on: #8187
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
402/4 |
Mathlib.lean,Mathlib/Algebra/DirectSum/Internal.lean,Mathlib/Algebra/GradedMonoid.lean,Mathlib/Algebra/Module/GradeZeroModule.lean,Mathlib/RingTheory/Finiteness.lean,Mathlib/RingTheory/GradedAlgebra/Basic.lean,Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean,Mathlib/RingTheory/GradedAlgebra/Noetherian.lean |
8 |
11 |
['FMLJohn', 'github-actions', 'jjaassoonn', 'leanprover-community-mathlib4-bot'] |
nobody |
286-42795 9 months ago |
320-30712 10 months ago |
0-0 0 seconds |
7875 |
FR-vdash-bot author:FR-vdash-bot |
chore: make `SMulCommClass A A B` and `SMulCommClass A B B` higher priority |
---
[](https://gitpod.io/from-referrer/)
|
slow-typeclass-synthesis
t-algebra
merge-conflict
label:t-algebra$ |
54/48 |
Mathlib/Algebra/Algebra/Basic.lean,Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/DirectSum/Algebra.lean,Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Subgroup/Actions.lean,Mathlib/Algebra/Lie/NonUnitalNonAssocAlgebra.lean,Mathlib/Algebra/Module/LinearMap/End.lean,Mathlib/Algebra/MonoidAlgebra/Basic.lean,Mathlib/Algebra/MvPolynomial/Basic.lean,Mathlib/Algebra/Ring/CentroidHom.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Algebra/Star/NonUnitalSubalgebra.lean,Mathlib/Analysis/Complex/UnitDisc/Basic.lean,Mathlib/Analysis/NormedSpace/lpSpace.lean,Mathlib/Data/Matrix/Basic.lean,Mathlib/GroupTheory/GroupAction/Prod.lean,Mathlib/GroupTheory/GroupAction/Ring.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean,Mathlib/GroupTheory/MonoidLocalization.lean,Mathlib/GroupTheory/Submonoid/Center.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean,Mathlib/RingTheory/Ideal/Quotient.lean,Mathlib/RingTheory/TensorProduct/Basic.lean,Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean,Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean,Mathlib/Topology/ContinuousFunction/ZeroAtInfty.lean |
27 |
15 |
['FR-vdash-bot', 'Parcly-Taxel', 'jcommelin', 'leanprover-bot'] |
nobody |
286-42794 9 months ago |
308-23498 10 months ago |
1-47913 1 day |
6777 |
adomani author:adomani |
chore(Co*variantClass): replace eta-expanded (· * ·), (· + ·), (· ≤ ·), (· < ·) |
Replace `CovariantClass X X (· * ·) (· ≤ ·)` with -> `CovariantClass X X HMul.hMul LE.le` and similarly for `HAdd`, `LT`, `Contravariant`.
This PR is inspired by [Issue #6646](https://github.com/leanprover-community/mathlib4/issues/6646) and, more specifically, [this comment](https://github.com/leanprover-community/mathlib4/issues/6646#issuecomment-1692792066).
Note that https://github.com/leanprover/lean4/pull/2267 would make this unnecessary
---
```bash
# First sed command:
# the first captured pattern is `Co*variantClass `
# the second captured pattern is ``
# the third captured pattern is `+` or `*`
# the fourth captured pattern is `<` or `≤`
# a match for `Co*variantClass (· ·) (· ·)` becomes
# `Co*variantClass replaceop replaceop`
# Second sed command: similar to the first, but looks for `(Function.swap (· ·))`
sed -i '
s=\(Co[ntra]*variantClass \(..*\) \2 \)(· *\([+*]\) *·) (· *\([<≤]\) *·)=\1replaceop\3 replaceop\4=g
s=\(Co[ntra]*variantClass \(..*\) \2 \)(\([Functio\.swap ]*\)(· *\([+*]\) *·)) (· *\([<≤]\) *·)=\1(\3replaceop\4) replaceop\5=g
s=replaceop+=HAdd.hAdd=g
s=replaceop\*=HMul.hMul=g
s=replaceop<=LT.lt=g
s=replaceop≤=LE.le=g
s=\(Co[ntra]*variantClass N N\) (· \* ·) r=\1 HMul.hMul r=g
s=\(Co[ntra]*variantClass N N (swap μ)\) (· ≤ ·)=\1 LE.le=g
s=\(Co[ntra]*variantClass N N\) (swap (· \* ·)) r=\1 (swap HMul.hMul) r=g
s=\(CovariantClass (Filter α) (Filter α)\) (· / ·) (· ≤ ·)=\1 HDiv.hDiv LE.le=g
s=\(CovariantClass (Filter α) (Filter α)\) (swap (· / ·)) (· ≤ ·)=\1 (swap HDiv.hDiv) LE.le=g
s=\(Co[ntra]*variantClass .* (fun x y .> . \* .)\) (· ≤ ·)=\1 LE.le=g
s=\(Co[ntra]*variantClass .* (fun x y .> . \* .)\) (· < ·)=\1 LT.lt=g
s=\(Co[ntra]*variantClass [^}]*\) (· ≤ ·)=\1 LE.le=g
s=\(CovariantClass .* (Filter β)\) (· • ·) LE.le=\1 HSMul.hSMul LE.le=g
' $(git ls-files '*.lean')
```
[](https://gitpod.io/from-referrer/)
|
merge-conflict |
703/678 |
Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean,Mathlib/Algebra/BigOperators/Basic.lean,Mathlib/Algebra/Bounds.lean,Mathlib/Algebra/CovariantAndContravariant.lean,Mathlib/Algebra/DirectSum/Internal.lean,Mathlib/Algebra/Group/UniqueProds.lean,Mathlib/Algebra/GroupPower/Order.lean,Mathlib/Algebra/MonoidAlgebra/Degree.lean,Mathlib/Algebra/Order/Archimedean.lean,Mathlib/Algebra/Order/Group/Abs.lean,Mathlib/Algebra/Order/Group/Defs.lean,Mathlib/Algebra/Order/Group/DenselyOrdered.lean,Mathlib/Algebra/Order/Group/MinMax.lean,Mathlib/Algebra/Order/Group/OrderIso.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Order/Interval.lean,Mathlib/Algebra/Order/Kleene.lean,Mathlib/Algebra/Order/LatticeGroup.lean,Mathlib/Algebra/Order/Module.lean,Mathlib/Algebra/Order/Monoid/Basic.lean,Mathlib/Algebra/Order/Monoid/Cancel/Defs.lean,Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean,Mathlib/Algebra/Order/Monoid/Defs.lean,Mathlib/Algebra/Order/Monoid/Lemmas.lean,Mathlib/Algebra/Order/Monoid/MinMax.lean,Mathlib/Algebra/Order/Monoid/NatCast.lean,Mathlib/Algebra/Order/Monoid/OrderDual.lean,Mathlib/Algebra/Order/Monoid/Prod.lean,Mathlib/Algebra/Order/Monoid/WithTop.lean,Mathlib/Algebra/Order/Monoid/WithZero/Basic.lean,Mathlib/Algebra/Order/Monoid/WithZero/Defs.lean,Mathlib/Algebra/Order/Nonneg/Ring.lean,Mathlib/Algebra/Order/Pointwise.lean,Mathlib/Algebra/Order/Positive/Ring.lean,Mathlib/Algebra/Order/Ring/Canonical.lean,Mathlib/Algebra/Order/Ring/Defs.lean,Mathlib/Algebra/Order/Ring/Lemmas.lean,Mathlib/Algebra/Order/Sub/Basic.lean,Mathlib/Algebra/Order/Sub/Canonical.lean,Mathlib/Algebra/Order/Sub/Defs.lean,Mathlib/Algebra/Order/WithZero.lean,Mathlib/Algebra/Parity.lean,Mathlib/Algebra/Star/Order.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Analysis/Normed/Order/Lattice.lean,Mathlib/Data/DFinsupp/Lex.lean,Mathlib/Data/DFinsupp/Order.lean,Mathlib/Data/Finset/Fold.lean,Mathlib/Data/Finsupp/Lex.lean,Mathlib/Data/Finsupp/Order.lean,Mathlib/Data/List/BigOperators/Basic.lean,Mathlib/Data/List/BigOperators/Lemmas.lean,Mathlib/Data/Multiset/Basic.lean,Mathlib/Data/Nat/Cast/Order.lean,Mathlib/Data/PNat/Basic.lean,Mathlib/Data/Real/ENNReal.lean,Mathlib/Data/Real/NNReal.lean,Mathlib/Data/Set/Semiring.lean,Mathlib/Data/Sign.lean,Mathlib/MeasureTheory/Function/LpOrder.lean,Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean,Mathlib/MeasureTheory/Measure/MeasureSpace.lean,Mathlib/MeasureTheory/Measure/VectorMeasure.lean,Mathlib/Order/ConditionallyCompleteLattice/Group.lean,Mathlib/Order/Filter/Basic.lean,Mathlib/Order/Filter/Pointwise.lean,Mathlib/Probability/Martingale/Basic.lean,Mathlib/Probability/Process/Stopping.lean,Mathlib/RingTheory/GradedAlgebra/Basic.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Game/Basic.lean,Mathlib/SetTheory/Game/PGame.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Basic.lean,Mathlib/SetTheory/Ordinal/NaturalOps.lean,Mathlib/Tactic/GCongr/Core.lean,Mathlib/Tactic/Positivity/Basic.lean,Mathlib/Topology/ContinuousFunction/Algebra.lean,lean-toolchain,test/Recall.lean,test/propose.lean |
81 |
36 |
['adomani', 'alreadydone', 'digama0', 'eric-wieser', 'ericrbg', 'jcommelin', 'leanprover-bot', 'sgouezel'] |
nobody |
286-42794 9 months ago |
308-23498 10 months ago |
35-56459 35 days |
6491 |
eric-wieser author:eric-wieser |
chore(Mathlib/Algebra/Hom/GroupAction): add `SMulHomClass.comp_smul` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
24/10 |
Mathlib/Algebra/Hom/GroupAction.lean |
1 |
0 |
[] |
nobody |
286-42793 9 months ago |
308-23498 10 months ago |
83-76369 83 days |
6993 |
jjaassoonn author:jjaassoonn |
feat : lemmas about `AddMonoidAlgebra.{divOf, modOf}` |
---
- [x] depends on: #7582
- [x] depends on: #8975
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
147/3 |
Mathlib/Algebra/MonoidAlgebra/Division.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/MvPolynomial/Basic.lean,Mathlib/Data/MvPolynomial/CommRing.lean,Mathlib/Data/MvPolynomial/Division.lean |
5 |
42 |
['YaelDillies', 'alreadydone', 'digama0', 'eric-wieser', 'github-actions', 'jjaassoonn', 'leanprover-community-mathlib4-bot'] |
nobody |
286-42793 9 months ago |
308-23498 10 months ago |
102-21189 102 days |
10629 |
madvorak author:madvorak |
feat: List.cons_sublist_append_iff_right |
---
[](https://gitpod.io/from-referrer/)
|
t-data
merge-conflict
|
11/0 |
Mathlib/Data/List/Basic.lean |
1 |
1 |
['eric-wieser'] |
nobody |
272-36338 8 months ago |
272-36338 8 months ago |
53-73442 53 days |
11632 |
mattrobball author:mattrobball |
chore(Group/RingTheory.Congruence): make `Quotient`'s reducible |
These are essentially wrappers and should not expose any data when made reducible. Their use in constructing typeclass instances makes reducible transparency desirable.
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict |
16/35 |
Mathlib/GroupTheory/Congruence/Basic.lean,Mathlib/RingTheory/Congruence/Basic.lean |
2 |
14 |
['eric-wieser', 'fpvandoorn', 'github-actions', 'grunweg', 'kmill', 'leanprover-bot', 'mattrobball'] |
nobody |
267-85762 8 months ago |
298-21122 9 months ago |
2-10495 2 days |
13791 |
digama0 author:digama0 |
refactor: Primrec and Partrec |
General cleanup of the `Primrec` and `Partrec` files, to better adjust to lean 4 things. The main user-visible change is that `Primrec₂` is no longer a `def` but an `abbrev`, because it was causing inference issues in lean 4. I also removed all the nonterminal `simp`s in `PartrecCode.lean`.
---
[](https://gitpod.io/from-referrer/)
|
tech debt
t-computability
merge-conflict
|
585/778 |
Mathlib/Computability/Ackermann.lean,Mathlib/Computability/Halting.lean,Mathlib/Computability/Partrec.lean,Mathlib/Computability/PartrecCode.lean,Mathlib/Computability/Primrec.lean |
5 |
2 |
['github-actions', 'grunweg'] |
nobody |
267-85583 8 months ago |
308-23498 10 months ago |
1-84718 1 day |
11964 |
adamtopaz author:adamtopaz |
feat: The functor of points of a scheme |
We construct the functor of points functor, and prove that it's full and faithful.
---
- [ ] depends on: #11947
[](https://gitpod.io/from-referrer/)
|
t-algebraic-geometry
t-category-theory
merge-conflict
|
210/0 |
Mathlib.lean,Mathlib/AlgebraicGeometry/FunctorOfPoints.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean |
3 |
4 |
['github-actions', 'grunweg', 'leanprover-community-mathlib4-bot'] |
nobody |
267-85442 8 months ago |
308-23498 10 months ago |
0-1223 20 minutes |
12418 |
rosborn author:rosborn |
style: replace preimage_val with ↓∩ notation |
---
This is a rough draft of what the new `↓∩` notation would look like within mathlib. I believe this is an improvement in clarity and would like to have `↓∩` as a standard notation (along with `''`, `⁻¹'`, `↑`, etc...). As `↓∩` is specialized for `Set`s, I have only changed `preimage_val` when the left-hand side of `↓∩` is a `Set`.
The introduction of the `↓∩` notation to Data.Set.Image is temporary as it isn't possible to import Data.Set.Subset directly. If we want `↓∩` unscoped, where would be the best place to define it? An option is Data.Set.Defs, but the notation cannot be defined without additional imports as the file does not import `notation3`.
[](https://gitpod.io/from-referrer/)
|
merge-conflict |
56/61 |
Mathlib/Analysis/InnerProductSpace/Projection.lean,Mathlib/Data/Set/Function.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/Set/Subset.lean,Mathlib/MeasureTheory/Constructions/Polish.lean,Mathlib/MeasureTheory/MeasurableSpace/Basic.lean,Mathlib/MeasureTheory/Measure/Restrict.lean,Mathlib/Order/UpperLower/Basic.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/Clopen.lean,Mathlib/Topology/Connected/Basic.lean,Mathlib/Topology/Connected/PathConnected.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/ContinuousOn.lean,Mathlib/Topology/LocalAtTarget.lean,Mathlib/Topology/LocallyConstant/Basic.lean,Mathlib/Topology/Separation.lean,Mathlib/Topology/Sober.lean |
18 |
3 |
['grunweg', 'rosborn'] |
nobody |
267-85341 8 months ago |
308-23498 10 months ago |
29-14218 29 days |
12751 |
Command-Master author:Command-Master |
feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size |
Remove `@[simp]` from `Nat.bit_false` and `Nat.bit_true`, as `bit0` and `bit1` are deprecated, and add some lemmas to `Bits`, `Bitwise` and `Size`.
---
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
merge-conflict
|
66/7 |
Mathlib/Data/Nat/Bits.lean,Mathlib/Data/Nat/Bitwise.lean,Mathlib/Data/Nat/Multiplicity.lean,Mathlib/Data/Nat/Size.lean |
4 |
26 |
['Command-Master', 'Rida-Hamadani', 'Ruben-VandeVelde', 'YaelDillies', 'github-actions', 'jcommelin'] |
nobody |
267-20095 8 months ago |
272-36337 8 months ago |
54-52408 54 days |
16464 |
Parcly-Taxel author:Parcly-Taxel |
chore: deprecate `Nat.(case_)strong_induction_on` |
…in favour of the now-renamed `Nat.(case)strongInductionOn` in core. |
tech debt
merge-conflict
|
54/56 |
Archive/Imo/Imo1981Q3.lean,Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean,Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean,Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean,Mathlib/Algebra/Polynomial/Derivative.lean,Mathlib/Algebra/Polynomial/Lifts.lean,Mathlib/Analysis/Analytic/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Hofer.lean,Mathlib/Analysis/SpecificLimits/Normed.lean,Mathlib/Combinatorics/Derangements/Finite.lean,Mathlib/Combinatorics/Enumerative/Catalan.lean,Mathlib/Combinatorics/Hall/Finite.lean,Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean,Mathlib/Computability/Primrec.lean,Mathlib/Data/Fintype/Basic.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/Data/Nat/Choose/Central.lean,Mathlib/Data/Nat/Defs.lean,Mathlib/Data/Nat/Digits.lean,Mathlib/Data/Nat/Log.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean,Mathlib/LinearAlgebra/Multilinear/Basic.lean,Mathlib/NumberTheory/BernoulliPolynomials.lean,Mathlib/NumberTheory/DiophantineApproximation.lean,Mathlib/NumberTheory/Pell.lean,Mathlib/NumberTheory/Primorial.lean,Mathlib/Order/Fin/Basic.lean,Mathlib/RingTheory/Adjoin/PowerBasis.lean,Mathlib/RingTheory/LittleWedderburn.lean,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean,Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean,Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean,Mathlib/RingTheory/Polynomial/Nilpotent.lean,Mathlib/RingTheory/PowerSeries/Basic.lean,Mathlib/RingTheory/QuotientNilpotent.lean,Mathlib/RingTheory/WittVector/Defs.lean,Mathlib/RingTheory/WittVector/Frobenius.lean,Mathlib/RingTheory/WittVector/StructurePolynomial.lean,Mathlib/SetTheory/Surreal/Dyadic.lean,Mathlib/Topology/Metrizable/Uniformity.lean |
43 |
13 |
['Parcly-Taxel', 'b-mehta', 'github-actions', 'jcommelin'] |
nobody |
235-8651 7 months ago |
235-8651 7 months ago |
8-1989 8 days |
17127 |
FR-vdash-bot author:FR-vdash-bot |
chore: remove global `Quotient.mk` `⟦·⟧` notation |
---
Merge this PR when we are ready to migrate to `QuotLike` API (#16421).
[](https://gitpod.io/from-referrer/)
|
t-data
merge-conflict
|
137/2 |
Counterexamples/Pseudoelement.lean,Mathlib/Algebra/Associated/Basic.lean,Mathlib/Algebra/BigOperators/Group/Finset.lean,Mathlib/Algebra/Group/Conj.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Order/CauSeq/Completion.lean,Mathlib/Algebra/Quandle.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean,Mathlib/CategoryTheory/Abelian/Pseudoelements.lean,Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean,Mathlib/CategoryTheory/Monoidal/Free/Basic.lean,Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean,Mathlib/CategoryTheory/Skeletal.lean,Mathlib/Data/Finset/Card.lean,Mathlib/Data/Fintype/List.lean,Mathlib/Data/Fintype/Quotient.lean,Mathlib/Data/Multiset/Basic.lean,Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean,Mathlib/Data/QPF/Univariate/Basic.lean,Mathlib/Data/Quot.lean,Mathlib/Data/Real/Basic.lean,Mathlib/Data/Set/Finite.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/GroupTheory/GroupAction/Basic.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/LinearAlgebra/Dual.lean,Mathlib/LinearAlgebra/Ray.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/ModelTheory/DirectLimit.lean,Mathlib/ModelTheory/Fraisse.lean,Mathlib/ModelTheory/Quotients.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean,Mathlib/NumberTheory/NumberField/Embeddings.lean,Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean,Mathlib/NumberTheory/Padics/PadicIntegers.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/Order/RelIso/Basic.lean,Mathlib/RepresentationTheory/Action/Concrete.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Cardinal/Ordinal.lean,Mathlib/SetTheory/Game/Basic.lean,Mathlib/SetTheory/Game/Birthday.lean,Mathlib/SetTheory/Game/Impartial.lean,Mathlib/SetTheory/Game/Ordinal.lean,Mathlib/SetTheory/Game/State.lean,Mathlib/SetTheory/Lists.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Basic.lean,Mathlib/SetTheory/Surreal/Basic.lean,Mathlib/SetTheory/Surreal/Dyadic.lean,Mathlib/SetTheory/Surreal/Multiplication.lean,Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/SetTheory/ZFC/Rank.lean,Mathlib/Topology/Connected/PathConnected.lean,Mathlib/Topology/Homotopy/HomotopyGroup.lean,Mathlib/Topology/Homotopy/Path.lean,Mathlib/Topology/Homotopy/Product.lean,Mathlib/Topology/MetricSpace/GromovHausdorff.lean,Mathlib/Topology/UniformSpace/Separation.lean,test/interactiveUnfold.lean |
68 |
1 |
['github-actions'] |
nobody |
225-57434 7 months ago |
225-57434 7 months ago |
4-72805 4 days |
8029 |
alreadydone author:alreadydone |
refactor: Homotopy between Functions not ContinuousMaps |
This allows talking about homotopies without needing to supply proofs of continuity for the two ends. This for example simplifies the definition of H-spaces.
Of course, if a homotopy exists between two functions, those two functions are automatically continuous because they are restrictions of the homotopy (which is continuous) to subspaces.
`Homotopy.refl` still needs a continuous map as input, and `Homotopic` is only an equivalence relation when restricted to ContinuousMap.
---
TODO: fix docstrings
[](https://gitpod.io/from-referrer/)
|
t-topology
RFC
merge-conflict
|
246/250 |
Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean,Mathlib/Topology/Homotopy/Basic.lean,Mathlib/Topology/Homotopy/Contractible.lean,Mathlib/Topology/Homotopy/Equiv.lean,Mathlib/Topology/Homotopy/HSpaces.lean,Mathlib/Topology/Homotopy/HomotopyGroup.lean,Mathlib/Topology/Homotopy/Path.lean,Mathlib/Topology/Homotopy/Product.lean |
8 |
3 |
['alreadydone', 'urkud'] |
nobody |
215-86239 7 months ago |
308-23498 10 months ago |
9-20043 9 days |
14598 |
Command-Master author:Command-Master |
chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. |
Add the four typeclasses `IsTopAbsorbing`, `IsBotAbsorbing`, `NoTopSum`, `NoBotSum`, as additive equivalents for `MulZeroClass` and `NoZeroDivisors`. Add instances of these for `ENNReal`, `WithTop α`, `WithBot α`, `PUnit`, `EReal`, `PartENat`, `Measure`, `Interval` and `Filter`.
Also split `Algebra/Order/AddGroupWithTop` to `Algebra/Order/Group/WithTop` and `Algebra/Order/Monoid/WithTop`
---
Previous usages of lemmas with quantified names like `WithTop.add_top` have to be changed to just `add_top`.
`add_lt_top` is `@[simp]`, in accordance with `ENNReal.add_lt_top` being `@[simp]`. This affects `WithTop.add_lt_top` which previously hadn't been `@[simp]`.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-order
t-algebra
merge-conflict
label:t-algebra$ |
264/195 |
Archive/Wiedijk100Theorems/BallotProblem.lean,Mathlib.lean,Mathlib/Algebra/Order/Group/WithTop.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Interval/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean,Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/Algebra/Order/Monoid/WithTop.lean,Mathlib/Algebra/PUnitInstances/Order.lean,Mathlib/Algebra/Polynomial/Degree/Definitions.lean,Mathlib/Algebra/Polynomial/Monic.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Analysis/Analytic/Meromorphic.lean,Mathlib/Analysis/Normed/Lp/ProdLp.lean,Mathlib/Analysis/NormedSpace/ENorm.lean,Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean,Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean,Mathlib/Data/ENNReal/Operations.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/Nat/WithBot.lean,Mathlib/Data/Real/EReal.lean,Mathlib/LinearAlgebra/Lagrange.lean,Mathlib/MeasureTheory/Covering/Differentiation.lean,Mathlib/MeasureTheory/Decomposition/Lebesgue.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean,Mathlib/MeasureTheory/Function/Jacobian.lean,Mathlib/MeasureTheory/Function/L1Space.lean,Mathlib/MeasureTheory/Function/L2Space.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Function/LpSpace.lean,Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean,Mathlib/MeasureTheory/Function/UniformIntegrable.lean,Mathlib/MeasureTheory/Integral/Bochner.lean,Mathlib/MeasureTheory/Integral/MeanInequalities.lean,Mathlib/MeasureTheory/Integral/SetIntegral.lean,Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean,Mathlib/MeasureTheory/Measure/Hausdorff.lean,Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/MeasureTheory/Measure/MeasureSpace.lean,Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean,Mathlib/MeasureTheory/Measure/Regular.lean,Mathlib/MeasureTheory/Measure/Typeclasses.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/Order/Filter/Pointwise.lean,Mathlib/Probability/Kernel/Defs.lean,Mathlib/Probability/Martingale/Convergence.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/UniqueFactorizationDomain.lean,Mathlib/Topology/EMetricSpace/Defs.lean,Mathlib/Topology/MetricSpace/Bounded.lean,Mathlib/Topology/MetricSpace/HausdorffDistance.lean,Mathlib/Topology/MetricSpace/Lipschitz.lean |
57 |
30 |
['Command-Master', 'YaelDillies', 'github-actions'] |
nobody |
188-52900 6 months ago |
188-52900 6 months ago |
7-45599 7 days |
12778 |
MichaelStollBayreuth author:MichaelStollBayreuth |
perf: decouple algebraic and order hierarchies in type class search |
Based on the experience gained with [#12680](https://github.com/leanprover-community/mathlib4/pull/12680), this attempts to decouple the algebraic and order hierarchies in type class search.
* We lower the priorities of instances like `OrderedSemiring.toSemiring` (which are generated by the `extends` clause with default priority 1000) to 50.
* Additionally, we make the default priority available via `open scoped AlgebraOrderInstances` and use that where appropriate.
**Motivation:** Looking at instance synthesization traces, it appears that when (e.g.) presented with the goal to find a `Semiring` instance, the algorithm frequently goes down a rabbit hole trying and failing to find order instances. This seems to be caused by the presence of instances like `OrderedSemiring.toSemiring` with default priority, which are tried early in the search, but lead nowhere (after a fairly long time). These instances are created by declarations of the form
```lean
class OrderedSemiring (α : Type u) extends Semiring α, OrderedAddCommMonoid α where ...
```
which automatically sets up (among other things) an instance `OrderedSemiring.toSemiring` with default piority. It appears that these instances cannot be removed completely (only locally in a module), so the next best solution is to make them low priority (which is possible also for downstream modules). To provide for situations where these instances are desired, we put a default priority version in the scope `AlgebraOrderInstances`.
---
[](https://gitpod.io/from-referrer/)
|
slow-typeclass-synthesis
t-order
t-algebra
merge-conflict
label:t-algebra$ |
306/27 |
Mathlib/Algebra/Algebra/Subalgebra/Order.lean,Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean,Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean,Mathlib/Algebra/Module/Rat.lean,Mathlib/Algebra/Module/Submodule/Order.lean,Mathlib/Algebra/Order/AbsoluteValue.lean,Mathlib/Algebra/Order/Algebra.lean,Mathlib/Algebra/Order/Antidiag/Prod.lean,Mathlib/Algebra/Order/Archimedean/Basic.lean,Mathlib/Algebra/Order/BigOperators/Group/Finset.lean,Mathlib/Algebra/Order/BigOperators/Group/List.lean,Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean,Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean,Mathlib/Algebra/Order/BigOperators/Ring/List.lean,Mathlib/Algebra/Order/BigOperators/Ring/Multiset.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Chebyshev.lean,Mathlib/Algebra/Order/CompleteField.lean,Mathlib/Algebra/Order/Field/Basic.lean,Mathlib/Algebra/Order/Field/Defs.lean,Mathlib/Algebra/Order/Field/Pi.lean,Mathlib/Algebra/Order/Floor.lean,Mathlib/Algebra/Order/Floor/Div.lean,Mathlib/Algebra/Order/Group/Defs.lean,Mathlib/Algebra/Order/Group/Units.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Hom/Basic.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Order/Interval/Basic.lean,Mathlib/Algebra/Order/Interval/Set/Instances.lean,Mathlib/Algebra/Order/Invertible.lean,Mathlib/Algebra/Order/Kleene.lean,Mathlib/Algebra/Order/Module/Algebra.lean,Mathlib/Algebra/Order/Module/Defs.lean,Mathlib/Algebra/Order/Module/Pointwise.lean,Mathlib/Algebra/Order/Monoid/Basic.lean,Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean,Mathlib/Algebra/Order/Monoid/Defs.lean,Mathlib/Algebra/Order/Monoid/OrderDual.lean,Mathlib/Algebra/Order/Monoid/Prod.lean,Mathlib/Algebra/Order/Nonneg/Field.lean,Mathlib/Algebra/Order/Nonneg/Ring.lean,Mathlib/Algebra/Order/Pi.lean,Mathlib/Algebra/Order/Positive/Field.lean,Mathlib/Algebra/Order/Positive/Ring.lean,Mathlib/Algebra/Order/Rearrangement.lean,Mathlib/Algebra/Order/Ring/Basic.lean,Mathlib/Algebra/Order/Ring/Defs.lean,Mathlib/Algebra/Order/Ring/InjSurj.lean,Mathlib/Algebra/Order/Ring/Pow.lean,Mathlib/Algebra/Order/Sub/WithTop.lean,Mathlib/Algebra/Order/ToIntervalMod.lean,Mathlib/Algebra/Ring/BooleanRing.lean,Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean,Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/Analysis/BoundedVariation.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean,Mathlib/Analysis/Convex/Basic.lean,Mathlib/Analysis/Convex/Cone/Basic.lean,Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Analysis/Convex/Cone/Pointed.lean,Mathlib/Analysis/Convex/Cone/Proper.lean,Mathlib/Analysis/Convex/Exposed.lean,Mathlib/Analysis/Convex/Extrema.lean,Mathlib/Analysis/Convex/Function.lean,Mathlib/Analysis/Convex/Gauge.lean,Mathlib/Analysis/Convex/GaugeRescale.lean,Mathlib/Analysis/Convex/Hull.lean,Mathlib/Analysis/Convex/Join.lean,Mathlib/Analysis/Convex/Mul.lean,Mathlib/Analysis/Convex/Quasiconvex.lean,Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean,Mathlib/Analysis/Convex/Star.lean,Mathlib/Analysis/Convex/Strict.lean,Mathlib/Analysis/InnerProductSpace/Orientation.lean,Mathlib/Analysis/MeanInequalities.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Polynomials.lean,Mathlib/Analysis/SpecificLimits/FloorPow.lean,Mathlib/Analysis/SpecificLimits/Normed.lean,Mathlib/Combinatorics/Optimization/ValuedCSP.lean,Mathlib/Combinatorics/Pigeonhole.lean,Mathlib/Combinatorics/SetFamily/FourFunctions.lean,Mathlib/Data/DFinsupp/Lex.lean,Mathlib/Data/DFinsupp/Multiset.lean,Mathlib/Data/DFinsupp/Order.lean,Mathlib/Data/Finset/MulAntidiagonal.lean,Mathlib/Data/Finsupp/Lex.lean,Mathlib/Data/Finsupp/Multiset.lean,Mathlib/Data/Finsupp/Order.lean,Mathlib/Data/Int/Log.lean,Mathlib/Data/Multiset/Antidiagonal.lean,Mathlib/Data/Multiset/Basic.lean,Mathlib/Data/Multiset/Bind.lean,Mathlib/Data/Nat/Cast/Field.lean,Mathlib/Data/Nat/Cast/Order/Basic.lean,Mathlib/Data/Nat/Choose/Bounds.lean,Mathlib/Data/PNat/Factors.lean,Mathlib/Data/Rat/Denumerable.lean,Mathlib/Data/Set/Pointwise/Interval.lean |
135 |
34 |
['MichaelStollBayreuth', 'YaelDillies', 'github-actions', 'leanprover-bot'] |
nobody |
188-51803 6 months ago |
188-51803 6 months ago |
18-19513 18 days |
18806 |
FR-vdash-bot author:FR-vdash-bot |
refactor: deprecate `MulEquivClass` |
---
- [x] depends on: #18809
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
84/72 |
Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/GroupWithZero/Hom.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Ring/Divisibility/Basic.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Ideal/Norm.lean,Mathlib/RingTheory/Localization/FractionRing.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean |
15 |
6 |
['FR-vdash-bot', 'github-actions', 'leanprover-bot', 'mathlib4-dependent-issues-bot', 'vihdzp'] |
nobody |
176-9081 5 months ago |
176-9081 5 months ago |
4-31794 4 days |
19212 |
Julian author:Julian |
feat(LinearAlgebra): add a variable_alias for VectorSpace |
Taken directly from the variable_alias docs.
Zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/why.20.5Bvariable_alias.5D.20attribute.20is.20not.20used.20in.20Mathlib.3F
---
This is the first actual variable alias added to mathlib. I haven't reviewed variable_alias fully, but it seems like there's at least 3 ways they could be distributed in Mathlib:
* alongside whatever subfolder they "belong to" (which is what I've tentatively done here)
* In a file called `Aliases` somewhere near the thing they alias (which seems less discoverable to me)
* In a single file, a la `Mathlib.TrainingWheels` (with some less playful name) which is meant to define a bunch of more "friendly" aliases all in one place.
I kind of like the idea of the third thing as a future module but perhaps it can be synthesized if/when there are more aliases? For now as I say I've done the first one, but please let me know if someone prefers something else.
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
25/0 |
Mathlib.lean,Mathlib/LinearAlgebra/VectorSpace.lean,scripts/noshake.json |
3 |
10 |
['Julian', 'PieterCuijpers', 'github-actions', 'urkud'] |
nobody |
168-29655 5 months ago |
168-29655 5 months ago |
7-68492 7 days |
19337 |
zeramorphic author:zeramorphic |
feat(Data/Finsupp): generalise `Finsupp` to any "zero" value |
Remove the explicit dependence of `Finsupp` on `[Zero M]`, instead defining `Finsupp'` (better name pending) to be functions that are equal to a fixed value `z : M` cofinitely often.
This PR is intended to do the initial work of replacing the definition of `Finsupp` with an instantiation of the more general definition, without adding any appropriate API. If accepted, the API development will follow in later PRs.
Issues to consider:
- Naming of `Finsupp'.`
- Where should `Finsupp'` lemmas go? Do they need their own file/folder under `Data/`?
Relevant Zulip threads:
- https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Finsupp.20generalisations
- https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Finsupp-like.20partial.20function
Comments are welcome.
---
[](https://gitpod.io/from-referrer/)
|
t-data
merge-conflict
|
203/83 |
Archive/Wiedijk100Theorems/Partition.lean,Mathlib/Algebra/MvPolynomial/Basic.lean,Mathlib/Algebra/MvPolynomial/Rename.lean,Mathlib/Algebra/MvPolynomial/Variables.lean,Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Algebra/Polynomial/Laurent.lean,Mathlib/Data/Finsupp/BigOperators.lean,Mathlib/Data/Finsupp/Defs.lean,Mathlib/Data/Finsupp/Order.lean,Mathlib/Data/Nat/Choose/Multinomial.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean,Mathlib/RingTheory/PowerBasis.lean,scripts/nolints_prime_decls.txt |
13 |
5 |
['github-actions', 'vihdzp', 'zeramorphic'] |
nobody |
166-5732 5 months ago |
166-5732 5 months ago |
4-60621 4 days |
18756 |
FR-vdash-bot author:FR-vdash-bot |
refactor: deprecate `DistribMulActionSemiHomClass` `MulSemiringActionSemiHomClass` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
50/28 |
Mathlib/Algebra/Algebra/NonUnitalHom.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/GroupTheory/GroupAction/Hom.lean |
3 |
4 |
['FR-vdash-bot', 'github-actions', 'leanprover-bot'] |
nobody |
154-57801 5 months ago |
154-57801 5 months ago |
31-75259 31 days |
18912 |
b-mehta author:b-mehta |
feat(SpecialFunctions/Log): more continuity and limits for logb |
Continuation from #18621.
From the ExponentialRamsey project.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
merge-conflict
|
144/17 |
Mathlib/Analysis/SpecialFunctions/Log/Base.lean,Mathlib/Data/Set/Pointwise/Interval.lean,Mathlib/Topology/Algebra/Order/Field.lean |
3 |
9 |
['b-mehta', 'dupuisf', 'github-actions', 'j-loreaux'] |
nobody |
154-15915 5 months ago |
154-15915 5 months ago |
1-18352 1 day |
19046 |
j-loreaux author:j-loreaux |
feat: define class `SemigroupAction` |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
34/25 |
Mathlib/Algebra/Category/ModuleCat/Presheaf.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean,Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/End.lean,Mathlib/Algebra/Group/Action/Prod.lean,Mathlib/Algebra/Group/Action/TypeTags.lean,Mathlib/Algebra/Polynomial/Laurent.lean,Mathlib/Analysis/Distribution/SchwartzSpace.lean,Mathlib/GroupTheory/CoprodI.lean,Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean,Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean |
11 |
7 |
['alreadydone', 'github-actions', 'j-loreaux', 'leanprover-bot', 'urkud'] |
nobody |
151-19285 5 months ago |
151-19286 5 months ago |
6-21105 6 days |
18748 |
FR-vdash-bot author:FR-vdash-bot |
refactor: deprecate `ContinuousLinearMapClass` |
---
- [ ] depends on: #18689
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-topology
merge-conflict
label:t-algebra$ |
115/49 |
Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Operator/LinearIsometry.lean,Mathlib/Topology/Algebra/Module/Basic.lean,Mathlib/Topology/Algebra/Module/CharacterSpace.lean,Mathlib/Topology/Algebra/Module/FiniteDimension.lean,Mathlib/Topology/Algebra/Module/StrongTopology.lean,Mathlib/Topology/Algebra/Module/WeakDual.lean,Mathlib/Topology/Homeomorph.lean |
10 |
5 |
['FR-vdash-bot', 'github-actions', 'leanprover-bot', 'mathlib4-dependent-issues-bot'] |
nobody |
148-21814 4 months ago |
148-21817 4 months ago |
0-989 16 minutes |
20527 |
trivial1711 author:trivial1711 |
refactor(Topology/UniformSpace/Completion): more descriptive names for `α → Completion α` |
- We rename the various maps `α → Completion α` in order to make their names more consistent.
- Let `α` be a uniform space. We rename the uniformly continuous function `α → Completion α` from `UniformSpace.Completion.coe'` to `UniformSpace.Completion.coe`.
- Let `α` be a uniform additive group. We rename the additive group homomorphism `α →+ Completion α` from `UniformSpace.Completion.toCompl` to `UniformSpace.Completion.coeAddHom`.
- Let `α` be a uniform ring. The ring homomorphism `α →+* Completion α` is called `UniformSpace.Completion.coeRingHom`; its name is unchanged.
- Let `α` be a normed space over a field `𝕜`. We rename the linear isometry `α →ₗᵢ[𝕜] Completion α` from `UniformSpace.Completion.toComplₗᵢ` to `UniformSpace.Completion.coeₗᵢ`.
- Let `α` be a normed space over a field `𝕜`. We rename the continuous linear map `α →L[𝕜] Completion α` from `UniformSpace.Completion.toComplL` to `UniformSpace.Completion.coeL`.
- Let `α` be a normed additive group. We rename the norm preserving homomorphism `NormedAddGroupHom α (Completion α)` from `NormedAddCommGroup.toCompl` to `UniformSpace.Completion.coeNormedAddGroupHom`.
- We analogously rename some other theorems.
- We add some trivial theorems (all of which are proved by `rfl`) that state that the functions considered above are equal. We give all of them the `simp` and `norm_cast` attributes.
- We add a new theorem `UniformSpace.Completion.coeAddHom_eq_coe` that states that `UniformSpace.Completion.coeAddHom` and `UniformSpace.Completion.coe` are equal as functions.
- We similarly add a new theorem `UniformSpace.Completion.coeRingHom_eq_coe`.
- We rename the theorem `UniformSpace.Completion.coe_toComplₗᵢ` to `UniformSpace.Completion.coeₗᵢ_eq_coe`.
- We rename the theorem `UniformSpace.Completion.coe_toComplL` to `UniformSpace.Completion.coeL_eq_coe`.
- We similarly add a new theorem `UniformSpace.Completion.coeNormedAddGroupHom_eq_coe`.
- We change all occurrences of the string `((↑) : α → Completion α)` to `(coe : α → Completion α)` or just `coe`.
- We put the statements of some theorems into simp normal form by using the plain function `coe` rather than the homomorphisms that carry more structure.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
merge-conflict
|
130/92 |
Mathlib/Analysis/Analytic/Uniqueness.lean,Mathlib/Analysis/Calculus/FDeriv/Analytic.lean,Mathlib/Analysis/Complex/AbsMax.lean,Mathlib/Analysis/Complex/Liouville.lean,Mathlib/Analysis/InnerProductSpace/Completion.lean,Mathlib/Analysis/Normed/Group/HomCompletion.lean,Mathlib/Analysis/Normed/Module/Completion.lean,Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean,Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean,Mathlib/Topology/Algebra/GroupCompletion.lean,Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean,Mathlib/Topology/Algebra/InfiniteSum/Nonarchimedean.lean,Mathlib/Topology/Algebra/Nonarchimedean/Completion.lean,Mathlib/Topology/Algebra/UniformRing.lean,Mathlib/Topology/Category/UniformSpace.lean,Mathlib/Topology/MetricSpace/Completion.lean,Mathlib/Topology/UniformSpace/Completion.lean |
17 |
4 |
['eric-wieser', 'github-actions', 'trivial1711'] |
nobody |
120-18607 4 months ago |
120-18607 4 months ago |
6-66637 6 days |
18474 |
FR-vdash-bot author:FR-vdash-bot |
perf: lower the priority of `*WithOne.to*` instances |
---
From #7873.
[](https://gitpod.io/from-referrer/)
|
t-data
slow-typeclass-synthesis
t-algebra
merge-conflict
label:t-algebra$ |
9/2 |
Mathlib/Algebra/Polynomial/BigOperators.lean,Mathlib/Data/Int/Cast/Defs.lean,Mathlib/Data/Nat/Cast/Defs.lean |
3 |
7 |
['FR-vdash-bot', 'eric-wieser', 'github-actions', 'leanprover-bot'] |
nobody |
118-5637 3 months ago |
118-5637 3 months ago |
76-67978 76 days |
19091 |
Vierkantor author:Vierkantor |
chore(Algebra/MonoidAlgebra): split Defs.lean further |
This PR further splits the big file `MonoidAlgebra/Defs.lean` to focus on the ring structure on (`Add`)`MonoidAlgebra`. The following files have been split off:
* `MonoidAlgebra/Lift.lean`: definition of `liftNC`
* `MonoidAlgebra/MapDomain.lean`: definition of `mapDomain`
* `MonoidAlgebra/Module.lean`: module structure (and some submodule results)
* `MonoidAlgebra/Opposite.lean`: results on the `MulOpposite` ring structure
I also changed one proof about scalar multiplication by natural numbers, so that it wouldn't need a full on module structure on `Finsupp`. This required adding a pair of lemmas on the definition of multiplying `Finsupp`s by natural numbers.
---
- [ ] depends on: #19087
- [ ] depends on: #19205
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
883/560 |
Mathlib.lean,Mathlib/Algebra/MonoidAlgebra/Basic.lean,Mathlib/Algebra/MonoidAlgebra/Defs.lean,Mathlib/Algebra/MonoidAlgebra/Division.lean,Mathlib/Algebra/MonoidAlgebra/Lift.lean,Mathlib/Algebra/MonoidAlgebra/MapDomain.lean,Mathlib/Algebra/MonoidAlgebra/Module.lean,Mathlib/Algebra/MonoidAlgebra/Opposite.lean,Mathlib/Algebra/MonoidAlgebra/Support.lean,Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Data/Finsupp/Defs.lean,Mathlib/RingTheory/Polynomial/Opposites.lean |
12 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
117-27154 3 months ago |
117-27154 3 months ago |
2-72196 2 days |
20372 |
jvlmdr author:jvlmdr |
feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L) |
Introduce ContinuousLinearMap.bilinearCompLp and bilinearCompLpL.
Generalize eLpNorm_le_eLpNorm_mul_eLpNorm theorems to include constant C in bound condition.
---
Expect this may be useful for defining tempered distributions from functions in `L^p`.
The definitions more or less follow `ContinuousLinearMap.compLp...`. Names are loosely analogous to `ContinuousLinearMap.bilinearComp` and `SchwartzMap.bilinLeftCLM`.
Note: I preferred the spelling `hpqr : p⁻¹ + q⁻¹ = r⁻¹` with `f` in `L^p` and `g` in `L^q` to `hpqr : 1 / p = 1 / q + 1 / r`. It's easier to obtain from `ENNReal.IsConjExponent` too.
A few questions:
- [ ] I defined `bilinear{Left,Right}LpL` in addition to `bilinearCompLpL` because `LinearMap.mkContinuous₂` is marked as `noncomputable` and `LinearMap.mkContinuous` is not. Is this worth the extra definitions? (Note: This is not visible in the source due to `noncomputable section`.)
- [ ] Should I use `C : ℝ` instead of `C : NNReal` for `eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm'`?
- [ ] Is it going to be painful to have `[Fact (1 ≤ p)] [Fact (1 ≤ q)] [Fact (1 ≤ r)]`? I don't think there's a way to avoid it though. Maybe providing specialized versions for `p.IsConjExponent q` with `L^1`?
Naming:
- [ ] Is it satisfactory to add a `'` to the `eLpNorm_le_eLpNorm_mul_eLpNorm ` definitions in `CompareExp.lean` where `≤ ‖f x‖ * ‖g x‖` has been replaced with `≤ C * ‖f x‖ * ‖g x‖`? These could replace the existing theorems, although I don't want to break backwards compatibility. There are 5 instances: `eLpNorm_le_eLpNorm_top_mul_eLpNorm'`, `eLpNorm_le_eLpNorm_mul_eLpNorm_top'`, `eLpNorm'_le_eLpNorm'_mul_eLpNorm''`, `eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm'`, `eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm'` (I'm not sure why the existing theorem `eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm` has an internal `'`)
- [ ] Is `bilinearLeftLpL` a suitable name? Other options: `bilinearCompLpLeftL`, `bilinearCompLeftLpL`, `bilinLeftLpL` (analogous to `SchwartzMap.bilinLeftCLM`)
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-measure-probability
merge-conflict
|
203/40 |
Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSpace.lean |
2 |
1 |
['github-actions'] |
nobody |
105-29894 3 months ago |
105-29894 3 months ago |
27-43617 27 days |
21948 |
ChrisHughes24 author:ChrisHughes24 |
feat(ModelTheory): Formula.iSup and iInf |
---
This was a slightly controversial addition discussed in #20175
[](https://gitpod.io/from-referrer/)
|
t-logic
merge-conflict
|
24/7 |
Mathlib/ModelTheory/Semantics.lean,Mathlib/ModelTheory/Syntax.lean |
2 |
5 |
['YaelDillies', 'github-actions'] |
nobody |
85-19354 2 months ago |
85-19354 2 months ago |
1-18127 1 day |
18463 |
vihdzp author:vihdzp |
feat(SetTheory/Ordinal/Notation/FundamentalSequence): define type of fundamental sequences |
We define `Sequence α` as the type of sequences with length 0, 1, or `ω`, and give a basic API. A subsequent PR will introduce the notion of a (countable and computable) fundamental sequence and establish basic results.
The goal of this is to generalize [`ONote.fundamentalSequence`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Ordinal/Notation.html#ONote.fundamentalSequence) to allow the construction of fundamental sequences for other ordinal notations.
---
See [my ordinal notation repository](https://github.com/vihdzp/ordinal-notation/blob/a6fdd7fe7cb521e686ea271902e7e5496f1804d3/OrdinalNotation/Cantor.lean#L1218) for a demonstration of how this API looks in practice.
[](https://gitpod.io/from-referrer/)
|
t-set-theory
t-order
merge-conflict
|
174/1 |
Mathlib.lean,Mathlib/SetTheory/Ordinal/Notation/Cantor.lean,Mathlib/SetTheory/Ordinal/Notation/FundamentalSequence.lean |
3 |
19 |
['YnirPaz', 'b-mehta', 'github-actions', 'vihdzp'] |
nobody |
83-54036 2 months ago |
83-54036 2 months ago |
52-25108 52 days |
21099 |
chrisflav author:chrisflav |
chore(RingTheory/Generators): use unification hints for variables and relations |
When working with generators and presentations, we rely on the `MvPolynomial` API, but since the type of variables is bundled in `Generators R S`, many lemmas don't apply with `rw` or `simp`, because they can't see through the definition of `vars` in constructions such as `Generators.comp` and `Generators.localizationAway`.
A possible approach is to make all of these constructions `abbrev`s, but this causes `simp` to also unfold `val` which is not always desirable. More generally, it is then harder to predict how instance search and `simp` behave. This approach is tried in #21050, but causes many regressions.
This approach is less invasive, as it uses `unif_hint` to unify the `vars` (and `rels`) fields of constructions with the correct type.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
231/91 |
Mathlib/Algebra/Module/Presentation/Differentials.lean,Mathlib/RingTheory/Generators.lean,Mathlib/RingTheory/Kaehler/JacobiZariski.lean,Mathlib/RingTheory/Presentation.lean,Mathlib/RingTheory/Smooth/StandardSmooth.lean |
5 |
16 |
['chrisflav', 'erdOne', 'github-actions', 'leanprover-bot', 'mattrobball'] |
nobody |
79-12872 2 months ago |
79-12872 2 months ago |
27-75210 27 days |
13964 |
pechersky author:pechersky |
feat(Data/DigitExpansion): begin defining variant of reals without rationals |
Based on a de Bruijn 1976 paper.
This file is just the basic definition of a digit expansion. Will be followed up with furhter constructions.
---
[](https://gitpod.io/from-referrer/)
|
t-data
merge-conflict
|
518/0 |
Mathlib.lean,Mathlib/Data/DigitExpansion/Defs.lean,docs/references.bib |
3 |
11 |
['eric-wieser', 'github-actions', 'kim-em', 'pechersky'] |
dupuisf assignee:dupuisf |
71-15977 2 months ago |
198-32485 6 months ago |
129-57991 129 days |
21339 |
vihdzp author:vihdzp |
fix(Data/List/Lex): remove duplicate `List.LE` instance |
Mathlib currently duplicates the Lean core instance for `≤` in lists in an incompatible way. We delete this duplicate instance.
See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Two.20.60List.2ELE.60.20instances.3F/near/497241115).
---
This is a very quick and dirty fix. Core Lean provides all of the theorems we need to prove `≤` forms a linear order, but it provides them in terms of `Std` relation typeclasses which currently see no use in Mathlib. I've added the instances that were required to get the list theorems working. In the future, we really ought to unify the core and Mathlib relation typeclasses.
[](https://gitpod.io/from-referrer/)
|
t-data
merge-conflict
|
24/22 |
Mathlib/Data/List/Lex.lean,Mathlib/Data/String/Basic.lean,Mathlib/Topology/Category/Profinite/Nobeling.lean |
3 |
1 |
['github-actions'] |
nobody |
71-11764 2 months ago |
71-11764 2 months ago |
16-65973 16 days |
21959 |
BGuillemet author:BGuillemet |
feat(Topology/ContinuousMap): Stone-Weierstrass theorem for MvPolynomial |
Add the subalgebra of multivariate polynomials and prove it separates points, on the same model as `ContinuousMap/Polynomial.lean`.
Prove the Stone-Weierstrass theorem and some variations for multivariate polynomials.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
merge-conflict
|
285/1 |
Mathlib.lean,Mathlib/Topology/ContinuousMap/MvPolynomial.lean,Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean |
3 |
1 |
['github-actions'] |
nobody |
69-15915 2 months ago |
69-15915 2 months ago |
16-76141 16 days |
22603 |
pechersky author:pechersky |
chore(Topology): rename pi family from π to X |
Only in files that mentioned such a family, via a script:
```
git grep -e "π : . → Type" --name-only | rg Topology | xargs -I{} sed -i -e 's/π/X/g' {}
```
---
[](https://gitpod.io/from-referrer/)
|
tech debt
t-topology
merge-conflict
|
232/232 |
Mathlib/Topology/AlexandrovDiscrete.lean,Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean,Mathlib/Topology/Algebra/Module/Equiv.lean,Mathlib/Topology/Algebra/Order/LiminfLimsup.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/Bornology/Constructions.lean,Mathlib/Topology/Connected/Basic.lean,Mathlib/Topology/Connected/Clopen.lean,Mathlib/Topology/Connected/LocallyConnected.lean,Mathlib/Topology/Connected/TotallyDisconnected.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/ContinuousOn.lean,Mathlib/Topology/EMetricSpace/Diam.lean,Mathlib/Topology/EMetricSpace/Pi.lean,Mathlib/Topology/ExtremallyDisconnected.lean,Mathlib/Topology/Inseparable.lean,Mathlib/Topology/MetricSpace/Basic.lean,Mathlib/Topology/MetricSpace/Infsep.lean,Mathlib/Topology/MetricSpace/ProperSpace.lean,Mathlib/Topology/MetricSpace/Pseudo/Pi.lean,Mathlib/Topology/Metrizable/Basic.lean,Mathlib/Topology/Order/Basic.lean,Mathlib/Topology/Separation/Hausdorff.lean,Mathlib/Topology/UniformSpace/Ascoli.lean |
24 |
1 |
['github-actions'] |
nobody |
63-17646 2 months ago |
63-17646 2 months ago |
5-80034 5 days |
22660 |
Ruben-VandeVelde author:Ruben-VandeVelde |
chore: follow naming convention around Group.IsNilpotent |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
133/67 |
Mathlib/GroupTheory/Frattini.lean,Mathlib/GroupTheory/Nilpotent.lean,Mathlib/GroupTheory/SpecificGroups/ZGroup.lean |
3 |
1 |
['github-actions'] |
nobody |
57-38170 1 month ago |
57-38170 1 month ago |
10-48025 10 days |
21856 |
vihdzp author:vihdzp |
chore(SetTheory/Cardinal/Basic): generalize universes of `sum_le_iSup_lift` |
We prove a more general version of the lemma which talks about families `ι → Cardinal.{v}` with `Small.{v} ι`, rather than just families `f : ι → Cardinal.{max u v}` with `ι : Type v`.
We keep the old version, as it's seemingly more useful under common circumstances.
---
[](https://gitpod.io/from-referrer/)
|
t-set-theory
merge-conflict
|
16/10 |
Mathlib/SetTheory/Cardinal/Basic.lean |
1 |
6 |
['b-mehta', 'github-actions', 'vihdzp'] |
nobody |
56-29404 1 month ago |
56-29404 1 month ago |
32-26420 32 days |
22027 |
vihdzp author:vihdzp |
chore(SetTheory/Ordinal/FixedPoint); review `Ordinal.nfp` API |
This PR does the following:
- add `iff` variants of various theorems, renaming some in the process
- weaken some assumptions slightly
- golf throughout
---
- [x] depends on: #22017
[](https://gitpod.io/from-referrer/)
|
t-set-theory
merge-conflict
|
64/61 |
Mathlib/Logic/Equiv/List.lean,Mathlib/SetTheory/Ordinal/FixedPoint.lean |
2 |
3 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] |
nobody |
37-82322 1 month ago |
40-49282 1 month ago |
43-68322 43 days |
13861 |
BoltonBailey author:BoltonBailey |
feat(Data/Finsupp/Basic): `Finsupp.optionElim'` |
Similar to how `Finsupp.cons` constructs a map `Fin (n + 1) →₀ M` from a map `Fin n →₀ M`,
we define `Finsupp.optionElim'` to construct a map `Option α →₀ M` from a map `α →₀ M`, given an additional value for `none`. As a function, it behaves as `Option.elim'`, hence the name.
We prove a variety of API lemmas, based on those for `Finsupp.cons`, to bring the definitions more in line with the contents of `Data/Finsupp/Fin`.
We also do some light refactoring for succinctness, and put this any related preexisting lemmas in a new file to not trigger the linter.
Needed by #12664
---
[](https://gitpod.io/from-referrer/)
|
t-data
merge-conflict
|
204/62 |
Mathlib.lean,Mathlib/Algebra/Category/MonCat/Adjunctions.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Finsupp/Option.lean,Mathlib/Data/Finsupp/Single.lean,Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean |
6 |
1 |
['github-actions'] |
nobody |
36-80907 1 month ago |
36-80907 1 month ago |
12-6613 12 days |
21858 |
vihdzp author:vihdzp |
refactor(SetTheory/Ordinal/FixedPoint): redefine `Ordinal.deriv` |
We previously defined the [ordinal derivative](https://en.wikipedia.org/wiki/Normal_function#Properties) of a function as the unique normal function satisfying `deriv f 0 = nfp f 0` and `deriv f (o + 1) = nfp f (deriv f o)` (where `nfp f a` is the next fixed point of `f` that's `≥ a`). The motivation here was to give a "nice" junk value on non-normal functions (the function is normal no matter what). However, in practice, this definition makes it unwieldy to prove things, by either requiring a tedious zero/successor/limit argument, or requiring one to rewrite `deriv f = enumOrd (fixedPoints f)`.
We can instead define `deriv f = enumOrd (fixedPoints f)`. At the cost of giving "worse" junk values (which we have no legitimate uses of), we're able to much more easily prove all the expected properties in the standard case where `f` is a normal function.
Finally, we do some drive-by API cleanup.
---
- [ ] depends on: #21860
- [ ] depends on: #21970
[](https://gitpod.io/from-referrer/)
|
t-set-theory
merge-conflict
|
216/262 |
Mathlib/Logic/Equiv/List.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean,Mathlib/SetTheory/Ordinal/Enum.lean,Mathlib/SetTheory/Ordinal/FixedPoint.lean,Mathlib/SetTheory/Ordinal/Principal.lean,Mathlib/SetTheory/Ordinal/Veblen.lean |
6 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
36-80369 1 month ago |
36-80371 1 month ago |
0-1601 26 minutes |
22701 |
ctchou author:ctchou |
feat(Combinatorics): the Katona circle method |
This file formalizes the Katona circle method.
From PlainCombi (LeanCamCombi): https://github.com/YaelDillies/LeanCamCombi/blob/master/LeanCamCombi/PlainCombi/KatonaCircle.lean
Co-authored-by: Yaël Dillies
|
new-contributor
t-combinatorics
merge-conflict
|
121/0 |
Mathlib.lean,Mathlib/Combinatorics/KatonaCircle.lean |
2 |
1 |
['github-actions'] |
nobody |
36-78084 1 month ago |
36-78084 1 month ago |
30-8337 30 days |
23411 |
PatrickMassot author:PatrickMassot |
chore: remove finiteness from Order.Filter.Lift |
Co-authored-by: Anatole Dedecker
---
[](https://gitpod.io/from-referrer/)
|
longest-pole
t-topology
merge-conflict
|
48/21 |
Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean,Mathlib/Order/Filter/Basic.lean,Mathlib/Order/Filter/Finite.lean,Mathlib/Order/Filter/Lift.lean,Mathlib/Order/Filter/SmallSets.lean,Mathlib/Topology/Algebra/ContinuousMonoidHom.lean,Mathlib/Topology/Basic.lean |
7 |
4 |
['Vierkantor', 'github-actions', 'kim-em', 'leanprover-community-bot-assistant'] |
nobody |
35-38398 1 month ago |
35-57967 1 month ago |
10-21608 10 days |
21488 |
imbrem author:imbrem |
feat(CategoryTheory/Monoidal): premonoidal categories |
Add support for premonoidal categories
---
Still want to add support for:
- Premonoidal braided/symmetric categories
- The monoidal coherence theorem, which I've already ported in my `discretion` library
- The `coherence` tactic, which should work fine for premonoidal categories too
but wanted to get this in front of reviewers ASAP to make sure my general approach was alright
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
merge-conflict
|
900/361 |
Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean,Mathlib/CategoryTheory/Bicategory/End.lean,Mathlib/CategoryTheory/GradedObject/Monoidal.lean,Mathlib/CategoryTheory/Localization/Monoidal.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Center.lean,Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/CategoryTheory/Monoidal/End.lean,Mathlib/CategoryTheory/Monoidal/Free/Basic.lean,Mathlib/CategoryTheory/Monoidal/Functor.lean,Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/CategoryTheory/Monoidal/Opposite.lean,Mathlib/CategoryTheory/Monoidal/Transport.lean,Mathlib/Tactic/CategoryTheory/Monoidal/Datatypes.lean,Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean,Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean,Mathlib/Tactic/CategoryTheory/MonoidalComp.lean,MathlibTest/StringDiagram.lean |
21 |
9 |
['YaelDillies', 'github-actions', 'grunweg', 'imbrem', 'kim-em', 'leanprover-community-bot-assistant'] |
nobody |
34-24317 1 month ago |
34-24318 1 month ago |
58-20339 58 days |
21525 |
sinhp author:sinhp |
feat(CategoryTheory): Locally Cartesian Closed Categories (Prelim) |
This PR defines the basic preliminaries for defining locally cartesian closed categories (LCCCs). In particular, using the calculus of mates we define certain natural isomorphisms involving `Over.star` and `Over.pullback` which will be crucial in defining the right adjoint to the pullback functor in the development of LCCCs.
---
[](https://gitpod.io/from-referrer/)
|
large-import
t-category-theory
merge-conflict
|
338/24 |
Mathlib/CategoryTheory/Comma/Over/Basic.lean,Mathlib/CategoryTheory/Comma/Over/Pullback.lean,Mathlib/CategoryTheory/Galois/Examples.lean |
3 |
13 |
['b-mehta', 'github-actions', 'joelriou', 'leanprover-community-bot-assistant', 'sinhp'] |
nobody |
34-24315 1 month ago |
34-24317 1 month ago |
43-83249 43 days |
21673 |
erdOne author:erdOne |
feat: `∑ z ∈ L, ‖z - x‖⁻ʳ` converges for lattices `L` |
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
merge-conflict
|
329/0 |
Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Disjoint.lean,Mathlib/Algebra/Module/ZLattice/Summable.lean,Mathlib/Order/Disjointed.lean |
4 |
4 |
['github-actions', 'leanprover-community-bot-assistant', 'xroblot'] |
nobody |
33-51713 1 month ago |
33-51715 1 month ago |
27-73279 27 days |
16314 |
FR-vdash-bot author:FR-vdash-bot |
chore(Data/Quot): deprecate `ind*'` APIs |
---
- [x] depends on: #16264
[](https://gitpod.io/from-referrer/)
|
t-data
merge-conflict
|
247/287 |
Counterexamples/CliffordAlgebraNotInjective.lean,Mathlib/Algebra/Colimit/Module.lean,Mathlib/Algebra/Lie/Quotient.lean,Mathlib/Algebra/Module/Torsion.lean,Mathlib/Algebra/RingQuot.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/CategoryTheory/ConnectedComponents.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/Computability/Reduce.lean,Mathlib/Computability/Tape.lean,Mathlib/Data/List/Cycle.lean,Mathlib/Data/Multiset/MapFold.lean,Mathlib/Data/Multiset/ZeroCons.lean,Mathlib/Data/Quot.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/FieldTheory/Fixed.lean,Mathlib/GroupTheory/Complement.lean,Mathlib/GroupTheory/Congruence/Basic.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/GroupTheory/Congruence/Hom.lean,Mathlib/GroupTheory/Coset/Basic.lean,Mathlib/GroupTheory/Coset/Defs.lean,Mathlib/GroupTheory/FreeAbelianGroup.lean,Mathlib/GroupTheory/GroupAction/Basic.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/GroupTheory/Index.lean,Mathlib/GroupTheory/MonoidLocalization/Basic.lean,Mathlib/GroupTheory/PGroup.lean,Mathlib/GroupTheory/Perm/Cycle/Concrete.lean,Mathlib/GroupTheory/PresentedGroup.lean,Mathlib/GroupTheory/QuotientGroup/Basic.lean,Mathlib/GroupTheory/QuotientGroup/Defs.lean,Mathlib/GroupTheory/SchurZassenhaus.lean,Mathlib/GroupTheory/Sylow.lean,Mathlib/LinearAlgebra/Alternating/DomCoprod.lean,Mathlib/LinearAlgebra/Projectivization/Basic.lean,Mathlib/LinearAlgebra/Quotient/Basic.lean,Mathlib/LinearAlgebra/Quotient/Defs.lean,Mathlib/MeasureTheory/Function/AEEqFun.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/NumberTheory/RamificationInertia/Basic.lean,Mathlib/Order/Antisymmetrization.lean,Mathlib/Order/Category/PartOrd.lean,Mathlib/Order/Filter/Germ/Basic.lean,Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean,Mathlib/RingTheory/AdicCompletion/Algebra.lean,Mathlib/RingTheory/AdicCompletion/Basic.lean,Mathlib/RingTheory/AdicCompletion/Functoriality.lean,Mathlib/RingTheory/AdjoinRoot.lean,Mathlib/RingTheory/Congruence/Basic.lean,Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean,Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean,Mathlib/RingTheory/Ideal/Cotangent.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/RingTheory/Ideal/Quotient/Basic.lean,Mathlib/RingTheory/Ideal/Quotient/Defs.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/Valuation/Quotient.lean,Mathlib/Topology/Algebra/Group/TopologicalAbelianization.lean,Mathlib/Topology/Algebra/InfiniteSum/Module.lean,Mathlib/Topology/Separation/Basic.lean |
65 |
4 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
28-49281 28 days ago |
28-49283 28 days ago |
55-52030 55 days |
23211 |
Parcly-Taxel author:Parcly-Taxel |
chore: automatically deprime common `induction'` uses |
Replace `induction'` with `induction` for the following targets:
```python
rep_dict = {("Nat", "~", 2): [("zero", 0), ("succ", 2)],
("Nat", "strong_induction_on", 1): [("h", 2)],
("Nat", "case_strong_induction_on", 2): [("hz", 0), ("hi", 2)],
("Nat", "le_induction", 2): [("base", 0), ("succ", 3)],
("List", "~", 2): [("nil", 0), ("cons", 3)],
("List", "reverseRecOn", 2): [("nil", 0), ("append_singleton", 3)],
("Multiset", "induction_on", 2): [("empty", 0), ("cons", 3)],
("Finset", "induction", 2): [("empty", 0), ("@insert", 4)],
("Finset", "induction_on", 2): [("empty", 0), ("@insert", 4)],
("MvPolynomial", "induction_on'", 2): [("monomial", 2), ("add", 4)],
("MvPolynomial", "induction_on", 3): [("C", 1), ("add", 4), ("mul_X", 3)]}
```
The script and the data file used can be found [here](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/The.20plan.20to.20remove.20induction'/near/508218834). |
tech debt
merge-conflict
|
2189/1565 |
Archive/Imo/Imo1977Q6.lean,Archive/Imo/Imo2006Q5.lean,Archive/Imo/Imo2013Q1.lean,Archive/Imo/Imo2013Q5.lean,Archive/Imo/Imo2019Q4.lean,Archive/Imo/Imo2024Q1.lean,Archive/MiuLanguage/DecisionSuf.lean,Archive/Sensitivity.lean,Archive/Wiedijk100Theorems/FriendshipGraphs.lean,Archive/Wiedijk100Theorems/Partition.lean,Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean,Mathlib/Algebra/Group/Conj.lean,Mathlib/Algebra/Group/ForwardDiff.lean,Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean,Mathlib/Algebra/Group/Pointwise/Set/Finite.lean,Mathlib/Algebra/Group/Pointwise/Set/ListOfFn.lean,Mathlib/Algebra/Lie/Solvable.lean,Mathlib/Algebra/Module/PID.lean,Mathlib/Algebra/Order/BigOperators/Group/List.lean,Mathlib/Algebra/Order/CauSeq/BigOperators.lean,Mathlib/Algebra/Order/Group/Multiset.lean,Mathlib/Algebra/Polynomial/BigOperators.lean,Mathlib/Algebra/Polynomial/Degree/Lemmas.lean,Mathlib/Algebra/Polynomial/Derivative.lean,Mathlib/Algebra/Polynomial/EraseLead.lean,Mathlib/Algebra/Polynomial/Eval/Defs.lean,Mathlib/Algebra/Polynomial/HasseDeriv.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Tropical/BigOperators.lean,Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean,Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/AlgebraicTopology/DoldKan/Projections.lean,Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean,Mathlib/Analysis/BoxIntegral/Partition/Additive.lean,Mathlib/Analysis/BoxIntegral/Partition/Split.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/Analysis/CStarAlgebra/Multiplier.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/Deriv/ZPow.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/Analysis/Calculus/SmoothSeries.lean,Mathlib/Analysis/Convex/Combination.lean,Mathlib/Analysis/Convex/Radon.lean,Mathlib/Analysis/InnerProductSpace/Projection.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Log/Base.lean,Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean,Mathlib/CategoryTheory/ComposableArrows.lean,Mathlib/CategoryTheory/Extensive.lean,Mathlib/CategoryTheory/Filtered/Basic.lean,Mathlib/CategoryTheory/Limits/VanKampen.lean,Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean,Mathlib/Computability/Ackermann.lean,Mathlib/Computability/DFA.lean,Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/Partrec.lean,Mathlib/Computability/PartrecCode.lean,Mathlib/Computability/PostTuringMachine.lean,Mathlib/Computability/Primrec.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Computability/TMConfig.lean,Mathlib/Computability/TMToPartrec.lean,Mathlib/Computability/Tape.lean,Mathlib/Control/LawfulFix.lean,Mathlib/Data/Complex/Exponential.lean,Mathlib/Data/Countable/Basic.lean,Mathlib/Data/DFinsupp/Defs.lean,Mathlib/Data/DFinsupp/WellFounded.lean,Mathlib/Data/Fin/Tuple/Basic.lean,Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean,Mathlib/Data/Finmap.lean,Mathlib/Data/Finset/Fold.lean,Mathlib/Data/Finset/Image.lean,Mathlib/Data/Finset/Lattice/Fold.lean,Mathlib/Data/Finset/Lattice/Lemmas.lean,Mathlib/Data/Finset/Lattice/Pi.lean,Mathlib/Data/Finset/Max.lean,Mathlib/Data/Finset/NAry.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Finset/Sym.lean,Mathlib/Data/Finsupp/BigOperators.lean,Mathlib/Data/Fintype/Basic.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/Data/Fintype/EquivFin.lean,Mathlib/Data/Fintype/Fin.lean |
283 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
28-47455 28 days ago |
28-47457 28 days ago |
10-65025 10 days |
13795 |
FR-vdash-bot author:FR-vdash-bot |
perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything |
---
- [ ] depends on: #15192
- [ ] depends on: #15476
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
340/194 |
Mathlib/Algebra/Equiv/TransferInstance.lean,Mathlib/Algebra/Group/InjSurj.lean,Mathlib/Algebra/GroupWithZero/Action/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/End.lean,Mathlib/Algebra/GroupWithZero/InjSurj.lean,Mathlib/Algebra/Module/Defs.lean,Mathlib/Algebra/Module/RingHom.lean,Mathlib/Algebra/Ring/InjSurj.lean,scripts/noshake.json |
9 |
35 |
['FR-vdash-bot', 'MichaelStollBayreuth', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mattrobball'] |
nobody |
28-41596 28 days ago |
28-41598 28 days ago |
52-31623 52 days |
15483 |
FR-vdash-bot author:FR-vdash-bot |
chore(GroupTheory/Coset): reduce defeq abuse |
---
- [x] depends on: #15482
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
114/60 |
Mathlib/GroupTheory/Commensurable.lean,Mathlib/GroupTheory/Coset.lean,Mathlib/GroupTheory/QuotientGroup.lean,Mathlib/LinearAlgebra/Alternating/DomCoprod.lean,Mathlib/MeasureTheory/Measure/Haar/Quotient.lean,Mathlib/Topology/Algebra/Group/Compact.lean |
6 |
14 |
['FR-vdash-bot', 'eric-wieser', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mattrobball', 'mergify', 'urkud'] |
nobody |
27-80574 27 days ago |
276-32504 9 months ago |
4-79214 4 days |
20567 |
grunweg author:grunweg |
feat(Cache): two small features |
- add an informational message to the get command (when run without arguments):
when more than 80% of all cache files present were not used in the last command,
tell the user about the `clean` command
---
- [ ] depends on #20568 (for the first feature)
- [ ] TODO: re-design this feature and the clean command: if there are N local copies of mathlib, cache should have a pointer to all of them - to avoid clearing all N-1 from inside the last local copy
[](https://gitpod.io/from-referrer/)
|
t-meta
merge-conflict
|
38/2 |
Cache/Main.lean |
1 |
11 |
['Julian', 'arthurpaulino', 'fpvandoorn', 'github-actions', 'grunweg'] |
nobody |
25-84677 25 days ago |
25-84677 25 days ago |
1-17369 1 day |
22153 |
smmercuri author:smmercuri |
feat: weak approximation theorems for infinite places of a number field |
The number field $K$ is dense in $\prod_v (K, v)$ and in the infinite adele ring $\prod_v K_v$, where $v$ ranges over the infinite places, $(K, v)$ denotes $K$ equipped with the topology induced by $v$, and $K_v$ is the completion of $K$ at $v$.
---
- [ ] depends on #22147
[](https://gitpod.io/from-referrer/)
|
large-import
t-algebra
t-analysis
t-number-theory
merge-conflict
label:t-algebra$ |
576/2 |
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean,Mathlib/Analysis/AbsoluteValue/Equivalence.lean,Mathlib/Analysis/Normed/Ring/WithAbs.lean,Mathlib/Data/Fin/Basic.lean,Mathlib/Data/Finset/Lattice/Fold.lean,Mathlib/Logic/Pairwise.lean,Mathlib/NumberTheory/NumberField/AdeleRing.lean,Mathlib/NumberTheory/NumberField/Embeddings.lean |
8 |
1 |
['github-actions'] |
nobody |
25-84497 25 days ago |
25-84497 25 days ago |
11-23591 11 days |
23859 |
urkud author:urkud |
feat(Topology/../Order/Field): generalize to `Semifield` |
.. from a linear ordered field to a linear ordered semifield---
- [ ] depends on: #23857
[](https://gitpod.io/from-referrer/)
|
t-topology
merge-conflict
|
245/219 |
Mathlib/Algebra/Order/Group/Pointwise/Interval.lean,Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean,Mathlib/Topology/Algebra/Order/Field.lean,Mathlib/Topology/Order/Basic.lean |
4 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
21-37191 21 days ago |
21-37194 21 days ago |
0-265 4 minutes |
17672 |
urkud author:urkud |
refactor: turn `IsTorsionFree` into a typeclass |
Rename `Monoid.IsTorsionFree` to `IsMulTorsionFree` and turn it into a typeclass.
Generalize some lemmas from (linear) ordered groups to `IsMulTorsionFree`.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
256/130 |
Mathlib.lean,Mathlib/Algebra/CharZero/Lemmas.lean,Mathlib/Algebra/Group/IsTorsionFree/Basic.lean,Mathlib/Algebra/Group/IsTorsionFree/Defs.lean,Mathlib/Algebra/Group/IsTorsionFree/Instances.lean,Mathlib/Algebra/Module/Defs.lean,Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean,Mathlib/Algebra/Order/Group/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean,Mathlib/Algebra/Order/Ring/Basic.lean,Mathlib/Algebra/Order/ToIntervalMod.lean,Mathlib/Combinatorics/Additive/CauchyDavenport.lean,Mathlib/Data/Nat/Prime/Pow.lean,Mathlib/FieldTheory/Finite/GaloisField.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean,Mathlib/GroupTheory/Order/Min.lean,Mathlib/GroupTheory/Torsion.lean,Mathlib/NumberTheory/ArithmeticFunction.lean,Mathlib/SetTheory/Surreal/Dyadic.lean,Mathlib/Topology/Instances/AddCircle.lean,Mathlib/Topology/Instances/ZMultiples.lean |
21 |
15 |
['YaelDillies', 'eric-wieser', 'github-actions', 'j-loreaux', 'leanprover-bot', 'urkud'] |
YaelDillies assignee:YaelDillies |
19-86231 19 days ago |
19-86237 19 days ago |
24-67723 24 days |
23810 |
b-reinke author:b-reinke |
chore(Order/Interval): generalize succ/pred lemmas to partial orders |
Many lemmas in `Mathlib/Order/Interval/Set/SuccPred.lean`and `Mathlib/Order/Interval/Finset/SuccPred.lean` also work for partial orders. They are generalized in this PR by introducing different sections for `PartialOrder` and `LinearOrder` assumptions in the respective files.
---
[](https://gitpod.io/from-referrer/)
|
t-order
merge-conflict
|
231/89 |
Mathlib/Order/Interval/Finset/SuccPred.lean,Mathlib/Order/Interval/Set/SuccPred.lean |
2 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
19-13966 19 days ago |
19-13968 19 days ago |
16-29623 16 days |
24285 |
madvorak author:madvorak |
chore(Algebra/*-{Category,Homology}): remove unnecessary universe variables |
Discussions:
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Call.20for.20help.3A.20technical.2F.20organisational.20debt/with/513620128
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Algebra.20and.20.60Type*.60/with/513558902
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Task.2026.3A.20Replace.20Type.20u.20by.20Type*.20wherever.20possible/with/513592993
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
542/916 |
Mathlib/Algebra/AddTorsor/Basic.lean,Mathlib/Algebra/Algebra/Defs.lean,Mathlib/Algebra/Algebra/Equiv.lean,Mathlib/Algebra/Algebra/Field.lean,Mathlib/Algebra/Algebra/Hom.lean,Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Algebra/Algebra/Spectrum/Basic.lean,Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/Algebra/Algebra/Subalgebra/Tower.lean,Mathlib/Algebra/Algebra/Tower.lean,Mathlib/Algebra/Central/Basic.lean,Mathlib/Algebra/Central/Defs.lean,Mathlib/Algebra/Central/TensorProduct.lean,Mathlib/Algebra/CharP/Pi.lean,Mathlib/Algebra/CharP/Quotient.lean,Mathlib/Algebra/CharP/Subring.lean,Mathlib/Algebra/DirectSum/Algebra.lean,Mathlib/Algebra/DirectSum/Basic.lean,Mathlib/Algebra/DirectSum/Finsupp.lean,Mathlib/Algebra/DirectSum/Module.lean,Mathlib/Algebra/EuclideanDomain/Basic.lean,Mathlib/Algebra/EuclideanDomain/Defs.lean,Mathlib/Algebra/Field/Basic.lean,Mathlib/Algebra/Field/Defs.lean,Mathlib/Algebra/Field/IsField.lean,Mathlib/Algebra/Field/MinimalAxioms.lean,Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/Field/Subfield/Defs.lean,Mathlib/Algebra/FreeNonUnitalNonAssocAlgebra.lean,Mathlib/Algebra/Group/Conj.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Equiv/Finite.lean,Mathlib/Algebra/Group/Ext.lean,Mathlib/Algebra/Group/Hom/End.lean,Mathlib/Algebra/Group/Hom/Instances.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/Algebra/Group/Invertible/Defs.lean,Mathlib/Algebra/Group/Pi/Basic.lean,Mathlib/Algebra/Group/Pi/Lemmas.lean,Mathlib/Algebra/Group/TypeTags/Basic.lean,Mathlib/Algebra/Group/TypeTags/Finite.lean,Mathlib/Algebra/Group/TypeTags/Hom.lean,Mathlib/Algebra/Group/Units/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/Algebra/Group/WithOne/Basic.lean,Mathlib/Algebra/Group/WithOne/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/Pi.lean,Mathlib/Algebra/GroupWithZero/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/NeZero.lean,Mathlib/Algebra/Lie/Abelian.lean,Mathlib/Algebra/Lie/Basic.lean,Mathlib/Algebra/Lie/CartanMatrix.lean,Mathlib/Algebra/Lie/CartanSubalgebra.lean,Mathlib/Algebra/Lie/Character.lean,Mathlib/Algebra/Lie/Classical.lean,Mathlib/Algebra/Lie/DirectSum.lean,Mathlib/Algebra/Lie/Free.lean,Mathlib/Algebra/Lie/Ideal.lean,Mathlib/Algebra/Lie/IdealOperations.lean,Mathlib/Algebra/Lie/Matrix.lean,Mathlib/Algebra/Lie/Nilpotent.lean,Mathlib/Algebra/Lie/NonUnitalNonAssocAlgebra.lean,Mathlib/Algebra/Lie/OfAssociative.lean,Mathlib/Algebra/Lie/Quotient.lean,Mathlib/Algebra/Lie/SkewAdjoint.lean,Mathlib/Algebra/Lie/Solvable.lean,Mathlib/Algebra/Lie/Subalgebra.lean,Mathlib/Algebra/Lie/Submodule.lean,Mathlib/Algebra/Lie/TensorProduct.lean,Mathlib/Algebra/Lie/UniversalEnveloping.lean,Mathlib/Algebra/Module/Basic.lean,Mathlib/Algebra/Module/CharacterModule.lean,Mathlib/Algebra/Module/DedekindDomain.lean,Mathlib/Algebra/Module/Defs.lean,Mathlib/Algebra/Module/End.lean,Mathlib/Algebra/Module/Equiv/Opposite.lean,Mathlib/Algebra/Module/Lattice.lean,Mathlib/Algebra/Module/LinearMap/Basic.lean,Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/Module/LinearMap/End.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Module/MinimalAxioms.lean,Mathlib/Algebra/Module/NatInt.lean,Mathlib/Algebra/Module/Opposite.lean,Mathlib/Algebra/Module/Pi.lean,Mathlib/Algebra/Module/Presentation/Differentials.lean,Mathlib/Algebra/Module/Presentation/Tensor.lean,Mathlib/Algebra/Module/Rat.lean,Mathlib/Algebra/Module/RingHom.lean,Mathlib/Algebra/Module/Submodule/Basic.lean,Mathlib/Algebra/Module/Torsion.lean,Mathlib/Algebra/MonoidAlgebra/Basic.lean,Mathlib/Algebra/MonoidAlgebra/Defs.lean,Mathlib/Algebra/MonoidAlgebra/Support.lean,Mathlib/Algebra/MvPolynomial/Basic.lean,Mathlib/Algebra/MvPolynomial/CommRing.lean,Mathlib/Algebra/MvPolynomial/Degrees.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean |
182 |
22 |
['erdOne', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'madvorak', 'mattrobball'] |
nobody |
19-2663 19 days ago |
19-2664 19 days ago |
2-12022 2 days |
23621 |
FR-vdash-bot author:FR-vdash-bot |
chore: deprecate `LinearOrderedComm{Monoid, Group}WithZero` |
---
[](https://gitpod.io/from-referrer/)
- [x] depends on: #20676
|
t-order
t-algebra
merge-conflict
label:t-algebra$ |
261/205 |
Archive/Imo/Imo1998Q2.lean,Counterexamples/LinearOrderWithPosMulPosEqZero.lean,Mathlib/Algebra/Order/Field/Canonical.lean,Mathlib/Algebra/Order/Field/Rat.lean,Mathlib/Algebra/Order/Floor/Ring.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Finset.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Order/Nonneg/Field.lean,Mathlib/Algebra/Order/Nonneg/Ring.lean,Mathlib/Algebra/Order/Ring/Nat.lean,Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean,Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean,Mathlib/Data/ENNReal/Basic.lean,Mathlib/Data/NNRat/Lemmas.lean,Mathlib/Data/NNReal/Defs.lean,Mathlib/Data/Rat/Cast/Order.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean,Mathlib/FieldTheory/RatFunc/AsPolynomial.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean,Mathlib/NumberTheory/EllipticDivisibilitySequence.lean,Mathlib/NumberTheory/FunctionField.lean,Mathlib/NumberTheory/Ostrowski.lean,Mathlib/RingTheory/Valuation/Archimedean.lean,Mathlib/RingTheory/Valuation/Basic.lean,Mathlib/RingTheory/Valuation/ExtendToLocalization.lean,Mathlib/RingTheory/Valuation/Integers.lean,Mathlib/RingTheory/Valuation/Integral.lean,Mathlib/RingTheory/Valuation/Minpoly.lean,Mathlib/RingTheory/Valuation/Quotient.lean,Mathlib/RingTheory/Valuation/RankOne.lean,Mathlib/RingTheory/Valuation/ValExtension.lean,Mathlib/RingTheory/Valuation/ValuationRing.lean,Mathlib/RingTheory/Valuation/ValuationSubring.lean,Mathlib/SetTheory/Cardinal/Order.lean,Mathlib/Topology/Algebra/Valued/LocallyCompact.lean,Mathlib/Topology/Algebra/Valued/NormedValued.lean,Mathlib/Topology/Algebra/Valued/ValuationTopology.lean,Mathlib/Topology/Algebra/Valued/ValuedField.lean,Mathlib/Topology/Algebra/Valued/WithVal.lean,Mathlib/Topology/Algebra/WithZeroTopology.lean,Mathlib/Topology/UnitInterval.lean,MathlibTest/instance_diamonds.lean,scripts/noshake.json |
44 |
n/a |
['FR-vdash-bot', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
kbuzzard assignee:kbuzzard |
18-2233 18 days ago |
unknown |
unknown |
24354 |
grunweg author:grunweg |
chore(HasFiniteIntegral): rename three lemmas |
Discovered in #24343.
---
- [ ] depends on: #24343 (to avoid merge conflicts)
[](https://gitpod.io/from-referrer/)
|
t-measure-probability
merge-conflict
|
108/30 |
Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean |
1 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
14-7067 14 days ago |
14-7068 14 days ago |
0-4604 1 hour |
13649 |
FR-vdash-bot author:FR-vdash-bot |
chore: redefine `Nat.div2` `Nat.bodd` |
The new definitions are faster than the old ones. `Nat.binaryRec` will be moved to batteries (https://github.com/leanprover-community/batteries/pull/799) or core (https://github.com/leanprover/lean4/pull/3756), so relevant contents are moved to a new file temporarily.
---
- [x] depends on: #15567
- [x] depends on: #19666
[](https://gitpod.io/from-referrer/)
|
merge-conflict |
63/88 |
Mathlib/Computability/Primrec.lean,Mathlib/Data/Int/Bitwise.lean,Mathlib/Data/Nat/Bits.lean,Mathlib/Data/Nat/Bitwise.lean,Mathlib/Data/Nat/Size.lean,Mathlib/Logic/Denumerable.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/Logic/Equiv/Nat.lean |
8 |
15 |
['FR-vdash-bot', 'digama0', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'urkud'] |
digama0 assignee:digama0 |
10-72613 10 days ago |
10-72615 10 days ago |
87-51692 87 days |
22052 |
FLDutchmann author:FLDutchmann |
feat(NumberTheory/SelbergSieve): define Lambda-squared sieves and prove important properties |
This PR:
* Defines lambda-squared sieves.
* Proves they are upper bound sieves.
* Proves that the corresponding main sum is a quadratic form.
---
- [x] depends on: #21880
[](https://gitpod.io/from-referrer/)
|
t-analysis
t-number-theory
merge-conflict
|
247/1 |
Mathlib/Data/Nat/GCD/Basic.lean,Mathlib/NumberTheory/SelbergSieve.lean |
2 |
7 |
['Ruben-VandeVelde', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
10-70135 10 days ago |
10-70138 10 days ago |
44-35375 44 days |
24109 |
grunweg author:grunweg |
feat(Tactic/Linter/DirectoryDependency): add an allow-list for directories with few imports |
Add an allow-list mechanism to the `directoryDependency` linter: modules covered by that list may only have imports listed in that list --- i.e., new top-level directory imports are *forbidden* by default.
To prove the implementation works, we add entries for the `Lean`, `Util` and `Tactic/Linter` directories in mathlib.
A future PR will convert the entries for e.g. `Logic`, `Control` or `Testable` to this allow-list.
This PR is a follow-up to #23088. Further refactorings (such as parsing the lists of exceptions from a JSON file)
can happen in subsequent PRs.
---
Open question: instead of manually filtering for imports of external projects, should I instead just lint only mathlib imports?
Future question: add further tests; this mechanism is somewhat undertested. I'm happy to work on this, but am not sure if this should block this PR. The lack of tests is certainly pre-existing.
[](https://gitpod.io/from-referrer/)
|
large-import
tech debt
t-linter
merge-conflict
|
211/30 |
Mathlib/Tactic/Linter/DirectoryDependency.lean,Mathlib/Tactic/Linter/Header.lean,MathlibTest/DirectoryDependencyLinter/Test.lean,MathlibTest/Header.lean,scripts/lint-style.lean |
5 |
16 |
['Vierkantor', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] |
nobody |
10-59803 10 days ago |
10-59804 10 days ago |
10-8423 10 days |
14023 |
mattrobball author:mattrobball |
perf(RingTheory.OreLocalization): make data irreducible |
We generally do not want to unfold operations passing through `Quotient` if we can avoid it for performance reasons.
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict |
43/32 |
Mathlib/GroupTheory/MonoidLocalization.lean,Mathlib/RingTheory/OreLocalization/Basic.lean,Mathlib/RingTheory/OreLocalization/Ring.lean |
3 |
5 |
['github-actions', 'grunweg', 'leanprover-bot', 'mattrobball'] |
nobody |
10-44746 10 days ago |
318-34569 10 months ago |
0-0 0 seconds |
4979 |
mhk119 author:mhk119 |
doc(Data/Nat/Bitblast): initial commit |
Initial commit of Bitblast.lean where we prove equivalence of bitblast unsigned less than and bitblast addition.
---
[](https://gitpod.io/from-referrer/)
|
t-data
merge-conflict
|
202/4 |
Mathlib/Data/Bool/Basic.lean,Mathlib/Data/Nat/Bitwise.lean,Mathlib/Data/Nat/Pow.lean |
3 |
49 |
['ChrisHughes24', 'digama0', 'goens', 'grunweg', 'j-loreaux', 'kim-em', 'mhk119'] |
nobody |
10-44448 10 days ago |
10-44448 10 days ago |
7-68358 7 days |
24064 |
kim-em author:kim-em |
chore: replace `norm_num` with `simp` where applicable |
Consider replacing a tactic with a (ahem) simpler alternative.
Fairly neutral performance implications, just depends on whether we would like to encourage people to use `simp` where applicable. |
merge-conflict |
345/345 |
Archive/Examples/MersennePrimes.lean,Archive/Imo/Imo1959Q2.lean,Archive/Imo/Imo1960Q1.lean,Archive/Imo/Imo1962Q1.lean,Archive/Imo/Imo1962Q4.lean,Archive/Imo/Imo1981Q3.lean,Archive/Imo/Imo1982Q1.lean,Archive/Imo/Imo2001Q2.lean,Archive/Imo/Imo2005Q4.lean,Archive/Imo/Imo2006Q3.lean,Archive/Imo/Imo2008Q4.lean,Archive/Imo/Imo2024Q1.lean,Archive/Imo/Imo2024Q5.lean,Archive/Imo/Imo2024Q6.lean,Archive/Wiedijk100Theorems/AbelRuffini.lean,Archive/Wiedijk100Theorems/CubingACube.lean,Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean,Counterexamples/Cyclotomic105.lean,Counterexamples/Phillips.lean,Mathlib/Algebra/Field/NegOnePow.lean,Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean,Mathlib/Algebra/Order/CauSeq/BigOperators.lean,Mathlib/Algebra/Polynomial/FieldDivision.lean,Mathlib/Algebra/Polynomial/Roots.lean,Mathlib/Algebra/Polynomial/SpecificDegree.lean,Mathlib/Algebra/Ring/BooleanRing.lean,Mathlib/Algebra/Star/CHSH.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicTopology/DoldKan/Faces.lean,Mathlib/Analysis/Analytic/Inverse.lean,Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean,Mathlib/Analysis/BoxIntegral/UnitPartition.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean,Mathlib/Analysis/CStarAlgebra/Module/Defs.lean,Mathlib/Analysis/Calculus/FDeriv/Measurable.lean,Mathlib/Analysis/Calculus/FDeriv/Norm.lean,Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean,Mathlib/Analysis/Complex/AbelLimit.lean,Mathlib/Analysis/Convex/Between.lean,Mathlib/Analysis/Convex/Function.lean,Mathlib/Analysis/Convolution.lean,Mathlib/Analysis/Fourier/AddCircle.lean,Mathlib/Analysis/Fourier/AddCircleMulti.lean,Mathlib/Analysis/Fourier/Inversion.lean,Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean,Mathlib/Analysis/InnerProductSpace/NormPow.lean,Mathlib/Analysis/InnerProductSpace/Projection.lean,Mathlib/Analysis/InnerProductSpace/l2Space.lean,Mathlib/Analysis/MeanInequalities.lean,Mathlib/Analysis/MellinInversion.lean,Mathlib/Analysis/Normed/Affine/Simplex.lean,Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean,Mathlib/Analysis/Normed/Group/ControlledClosure.lean,Mathlib/Analysis/Normed/Lp/lpSpace.lean,Mathlib/Analysis/Normed/Operator/Banach.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean,Mathlib/Analysis/NormedSpace/MStructure.lean,Mathlib/Analysis/NormedSpace/RieszLemma.lean,Mathlib/Analysis/Oscillation.lean,Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean,Mathlib/Analysis/SpecialFunctions/Complex/Log.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Isometric.lean,Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean,Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean,Mathlib/Analysis/SpecialFunctions/Integrals.lean,Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean,Mathlib/Analysis/SpecialFunctions/Pow/Real.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean,Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean,Mathlib/Combinatorics/Additive/SmallTripling.lean,Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean,Mathlib/Combinatorics/SimpleGraph/Density.lean,Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean,Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean,Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean,Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean,Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean,Mathlib/Computability/Ackermann.lean,Mathlib/Computability/AkraBazzi/AkraBazzi.lean,Mathlib/Computability/DFA.lean,Mathlib/Data/Complex/Basic.lean,Mathlib/Data/Complex/Trigonometric.lean,Mathlib/Data/Nat/Bits.lean,Mathlib/Data/Nat/Choose/Central.lean,Mathlib/Data/Nat/Choose/Sum.lean,Mathlib/Data/Nat/Digits.lean,Mathlib/Data/Nat/Prime/Defs.lean,Mathlib/Data/Real/GoldenRatio.lean,Mathlib/Data/Real/Pi/Bounds.lean,Mathlib/Data/Real/Pi/Irrational.lean |
171 |
9 |
['github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'leanprover-community-mathlib4-bot'] |
nobody |
10-5738 10 days ago |
10-5739 10 days ago |
11-65652 11 days |
23546 |
JovanGerb author:JovanGerb |
feat(LinearAlgebra/AffineSpace/AffineSubspace): rename `AffineSubspace.mk'` to `Submodule.shift` |
In addition to renaming, I've refactored the code a bit:
- `mem_mk'_iff_vsub_mem` was obsolete since it was the same as `mem_mk'`, so I removed it (this is due to a change in the definition I made recently)
- I added a nonempty instance for `shift`
- I added a simp lemma that `shift` isn't equal to `⊥` (the empty affine subspace). I need this for the next point.
- Edit: I'll leave this for a later PR.
~I proved a simp lemma that a `shift` is parallel to a `shift` if and only if the linear subspaces are the same.~
- I renamed `mk'_eq` to `shift_direction_eq_self `.
- I renamed `eq_or_eq_secondInter_of_mem_mk'_span_singleton_iff_mem` to `eq_or_eq_secondInter_iff_mem_of_mem_shift_span_singleton`. I think it is better to put the `of_mem_mk'_span_singleton` at the end of the name.
---
[](https://gitpod.io/from-referrer/)
|
t-euclidean-geometry
merge-conflict
|
128/99 |
Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Geometry/Euclidean/Basic.lean,Mathlib/Geometry/Euclidean/MongePoint.lean,Mathlib/Geometry/Euclidean/PerpBisector.lean,Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean,Mathlib/Geometry/Euclidean/Sphere/Tangent.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean |
7 |
4 |
['JovanGerb', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
9-19195 9 days ago |
9-19196 9 days ago |
26-25420 26 days |
24483 |
Parcly-Taxel author:Parcly-Taxel |
chore: delete >6 month old deprecations (2024-10) |
See #24271 for the general pattern of regex used in the first (automated) commit. The date range used in this PR is `2024-10-..`. |
tech debt
merge-conflict
|
2/1182 |
Mathlib/Algebra/BigOperators/Group/List/Basic.lean,Mathlib/Algebra/CharP/Two.lean,Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean,Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean,Mathlib/AlgebraicGeometry/Restrict.lean,Mathlib/Analysis/Analytic/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Defs.lean,Mathlib/Analysis/Calculus/Deriv/Basic.lean,Mathlib/Analysis/Calculus/Deriv/Comp.lean,Mathlib/Analysis/Calculus/FDeriv/Basic.lean,Mathlib/Analysis/Calculus/FDeriv/Comp.lean,Mathlib/Analysis/Calculus/LineDeriv/Basic.lean,Mathlib/Analysis/Complex/ReImTopology.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean,Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean,Mathlib/Analysis/LocallyConvex/WithSeminorms.lean,Mathlib/Analysis/Normed/Operator/Banach.lean,Mathlib/Analysis/Normed/Operator/LinearIsometry.lean,Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean,Mathlib/CategoryTheory/Limits/Preserves/Limits.lean,Mathlib/CategoryTheory/Sites/Canonical.lean,Mathlib/Data/ENNReal/Inv.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/List/Flatten.lean,Mathlib/Data/List/SplitBy.lean,Mathlib/Data/Nat/Factorization/Basic.lean,Mathlib/Data/Nat/Factorization/Defs.lean,Mathlib/Data/Nat/Factorization/PrimePow.lean,Mathlib/Data/Set/Subset.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean,Mathlib/Geometry/Manifold/ContMDiff/Defs.lean,Mathlib/Geometry/Manifold/LocalInvariantProperties.lean,Mathlib/Geometry/Manifold/MFDeriv/Basic.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/GroupTheory/GroupAction/Blocks.lean,Mathlib/LinearAlgebra/Eigenspace/Basic.lean,Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean,Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean,Mathlib/MeasureTheory/Measure/DiracProba.lean,Mathlib/MeasureTheory/Measure/FiniteMeasure.lean,Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean,Mathlib/NumberTheory/NumberField/Embeddings.lean,Mathlib/Order/InitialSeg.lean,Mathlib/Order/WellFounded.lean,Mathlib/Probability/Density.lean,Mathlib/RingTheory/Finiteness/Cardinality.lean,Mathlib/RingTheory/Finiteness/Ideal.lean,Mathlib/RingTheory/Jacobson/Ring.lean,Mathlib/RingTheory/Localization/Cardinality.lean,Mathlib/RingTheory/PowerSeries/Basic.lean,Mathlib/RingTheory/Spectrum/Prime/TensorProduct.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/SetTheory/Game/Nim.lean,Mathlib/SetTheory/PGame/Algebra.lean,Mathlib/Tactic/FunProp/ContDiff.lean,Mathlib/Topology/AlexandrovDiscrete.lean,Mathlib/Topology/Algebra/ConstMulAction.lean,Mathlib/Topology/Algebra/Constructions.lean,Mathlib/Topology/Algebra/Constructions/DomMulAct.lean,Mathlib/Topology/Algebra/Group/Basic.lean,Mathlib/Topology/Algebra/Group/CompactOpen.lean,Mathlib/Topology/Algebra/Group/Quotient.lean,Mathlib/Topology/Algebra/GroupWithZero.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean,Mathlib/Topology/Algebra/Module/Alternating/Topology.lean,Mathlib/Topology/Algebra/Module/Equiv.lean,Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean,Mathlib/Topology/Algebra/Module/StrongTopology.lean,Mathlib/Topology/Algebra/Module/WeakBilin.lean,Mathlib/Topology/Algebra/Monoid.lean,Mathlib/Topology/Algebra/MulAction.lean,Mathlib/Topology/Algebra/Ring/Ideal.lean,Mathlib/Topology/Algebra/SeparationQuotient/Section.lean,Mathlib/Topology/Algebra/StarSubalgebra.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/Category/Profinite/Nobeling/Induction.lean,Mathlib/Topology/Category/TopCat/EffectiveEpi.lean,Mathlib/Topology/Category/TopCat/Limits/Products.lean,Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean,Mathlib/Topology/Clopen.lean,Mathlib/Topology/CompactOpen.lean,Mathlib/Topology/Compactness/Compact.lean,Mathlib/Topology/Compactness/Lindelof.lean,Mathlib/Topology/Compactness/LocallyCompact.lean,Mathlib/Topology/Compactness/SigmaCompact.lean,Mathlib/Topology/Connected/Basic.lean,Mathlib/Topology/Connected/Clopen.lean,Mathlib/Topology/Connected/PathConnected.lean,Mathlib/Topology/Connected/TotallyDisconnected.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/Constructions/SumProd.lean,Mathlib/Topology/ContinuousMap/Bounded/Basic.lean,Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean,Mathlib/Topology/ContinuousMap/Sigma.lean,Mathlib/Topology/ContinuousMap/T0Sierpinski.lean,Mathlib/Topology/ContinuousOn.lean,Mathlib/Topology/Covering.lean,Mathlib/Topology/Defs/Induced.lean |
139 |
3 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
8-41152 8 days ago |
8-41154 8 days ago |
4-54091 4 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-8772 7 days ago |
14-14338 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 |
6-79826 6 days ago |
53-58453 1 month ago |
36-50134 36 days |
9273 |
grunweg author:grunweg |
feat: extended charts are local diffeomorphisms on their source |
---
TODO: I think this should hold at any interior point - as the inverse of the extended chart, restricted to the interior of its source, will be a local inverse.
The analogous result for un-extended charts is shown in #8160.
Unresolved questions
- are all the tiny API lemmas useful; are any more missing?
- do I want similar results for `extChartAt`? (In any case, they are easy to deduce.)
- [ ] depends on: #8738 for simplicity
[](https://gitpod.io/from-referrer/)
|
t-differential-geometry
merge-conflict
|
225/12 |
Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean,Mathlib/Geometry/Manifold/LocalDiffeomorph.lean,Mathlib/Topology/Algebra/Module/Basic.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
4-81003 4 days ago |
unknown |
unknown |
19985 |
vihdzp author:vihdzp |
feat(SetTheory/ZFC/Ordinal): Lean ordinals to ZFC ordinals |
We define `Ordinal.toZFSet` and prove that its outputs are precisely the ZFC ordinals.
---
- [ ] depends on: #19946
- [x] depends on: #19970
[](https://gitpod.io/from-referrer/)
|
large-import
t-set-theory
merge-conflict
|
208/6 |
Mathlib/Order/SuccPred/CompleteLinearOrder.lean,Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/SetTheory/ZFC/Ordinal.lean,Mathlib/SetTheory/ZFC/Rank.lean |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
4-13277 4 days ago |
4-13280 4 days ago |
0-562 9 minutes |
17027 |
vihdzp author:vihdzp |
feat(SetTheory/ZFC/Ordinal): von Neumann hierarchy of sets |
---
- [x] depends on: #16996
- [x] depends on: #17016
- [x] depends on: #17026
- [x] depends on: #18239
- [ ] depends on: #19946
- [x] depends on: #19967
[](https://gitpod.io/from-referrer/)
|
t-set-theory
merge-conflict
|
204/29 |
Mathlib.lean,Mathlib/SetTheory/Ordinal/Basic.lean,Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/SetTheory/ZFC/Neumann.lean,Mathlib/SetTheory/ZFC/Rank.lean |
5 |
8 |
['alreadydone', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp'] |
nobody |
4-13228 4 days ago |
4-13230 4 days ago |
0-344 5 minutes |
21732 |
101damnations author:101damnations |
feat(RepresentationTheory/*): representations on `Finsupp` |
Given a type `α` and a representation `A`, this PR defines `Rep.finsupp`, the representation defined pointwise on `α →₀ A`, and specializes this to `Rep.free`, when `A = leftRegular k G`.
We define `Rep.freeLiftLEquiv α A`, the `k`-linear equivalence between functions `α → A` and representation morphisms `Rep.free k G α ⟶ A`.
We also define representation isomorphisms `(α →₀ A) ⊗ B ≅ (A ⊗ B) →₀ α ≅ A ⊗ (α →₀ B)` given representations `A` and `B`, and finally `k[G] ⊗ (α →₀ k) ≅ free k G α` where `α →₀ k` is equipped with the trivial representation.
---
- [x] depends on: #21652
- [x] depends on: #22335
- [x] depends on: #22338
- [x] depends on: #23021
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
199/13 |
Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/RepresentationTheory/Basic.lean,Mathlib/RepresentationTheory/Rep.lean,Mathlib/RingTheory/Coalgebra/TensorProduct.lean,Mathlib/Tactic/Attr/Register.lean |
7 |
16 |
['101damnations', 'Whysoserioushah', 'github-actions', 'kbuzzard', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
2-76990 2 days ago |
2-76992 2 days ago |
10-61263 10 days |
24490 |
dagurtomas author:dagurtomas |
feat(CategoryTheory): transport symmetric monoidal structure along equivalence |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
merge-conflict
|
87/0 |
Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean |
3 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
2-31298 2 days ago |
2-31300 2 days ago |
9-66885 9 days |
24778 |
YaelDillies author:YaelDillies |
feat: `CommGrp`-valued Yoneda embedding |
From Toric
Co-authored-by: Andrew Yang
---
[](https://gitpod.io/from-referrer/)
|
toric
large-import
t-category-theory
merge-conflict
|
60/6 |
Mathlib/Algebra/Category/Grp/Basic.lean,Mathlib/Algebra/Category/Grp/ForgetCorepresentable.lean,Mathlib/Algebra/Category/MonCat/Basic.lean,Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean |
4 |
3 |
['TwoFX', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
1-36701 1 day ago |
1-36702 1 day ago |
0-68103 18 hours |
22503 |
Kevew author:Kevew |
chore(Nat): Nat factorization multiplicity |
Ported lemmas from `Data/Nat/Multiplicity` to into a new file called `Data/Nat/Factorization/Multiplicity`, re-written in terms of `factorization`.
---
- [x] depends on: #24576 for resolving the large import increase
[](https://gitpod.io/from-referrer/)
|
large-import
t-data
new-contributor
merge-conflict
|
327/102 |
Mathlib.lean,Mathlib/Data/Nat/Factorization/Basic.lean,Mathlib/Data/Nat/Factorization/LCM.lean,Mathlib/Data/Nat/Factorization/Multiplicity.lean,Mathlib/Data/Nat/Multiplicity.lean,Mathlib/GroupTheory/Exponent.lean,Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean,Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean |
8 |
40 |
['Kevew', 'Paul-Lez', 'YaelDillies', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
Kevew assignee:Kevew |
1-21053 1 day ago |
1-28830 1 day ago |
59-84303 59 days |
24485 |
dagurtomas author:dagurtomas |
feat(CategoryTheory): localization preserves braided structure |
---
[](https://gitpod.io/from-referrer/)
|
t-category-theory
merge-conflict
|
300/3 |
Mathlib.lean,Mathlib/CategoryTheory/Localization/Monoidal/Basic.lean,Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Sites/Monoidal.lean |
5 |
5 |
['github-actions', 'joelriou', 'leanprover-community-bot-assistant'] |
nobody |
1-18497 1 day ago |
1-18499 1 day ago |
10-38751 10 days |
22882 |
xroblot author:xroblot |
feat(NumberField/Units): add `regOfFamily` and refactor `regulator` |
This is a refactor of `NumberField.regulator`.
We introduce `regOfFamily` which is the regulator of a family of units indexed by `Fin (Units.rank K)`. It is equal to `0` if the family is not `isMaxRank`. This a `Prop` that says that the image of the family in the `logSpace K` is linearly independent and thus generates a full lattice. All the results about computing the `regulator` by some matrix determinant computation are now proved more generally for `regOfFamily`.
The `regulator` of a number field is still defined as the covolume of the `unitLattice` and we prove that is is also equal to `regOfFamily` of the system of fundamental units `fundSystem K`. Together with the results about computing `regOfFamily`, we recover that way the results about computing the regulator.
---
- [x] depends on: #22868
[](https://gitpod.io/from-referrer/)
|
t-number-theory
merge-conflict
|
186/56 |
Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean,Mathlib/NumberTheory/NumberField/Units/Regulator.lean |
3 |
5 |
['alreadydone', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
1-8294 1 day ago |
1-8295 1 day ago |
56-20698 56 days |
24764 |
YaelDillies author:YaelDillies |
doc: replace `Mathlib/Folder/file.lean` with `Mathlib.Folder.File` |
... for consistency. This is correctly interpreted by doc-gen. See eg https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Submonoid/Pointwise.html.
Replacement was done using the regex `Mathlib/([^/]*)/([^/]*)/([^/]*)/([^/]*)/([^/]*).lean` -> `Mathlib.$1.$2.$3.$4.$5` and similarly for smaller values of 5.
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
documentation
|
227/229 |
Archive/Examples/PropEncodable.lean,Archive/Wiedijk100Theorems/AbelRuffini.lean,Mathlib/Algebra/Category/HopfAlgebraCat/Monoidal.lean,Mathlib/Algebra/Category/Ring/Colimits.lean,Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean,Mathlib/Algebra/Module/SnakeLemma.lean,Mathlib/Algebra/Module/Submodule/Lattice.lean,Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean,Mathlib/Algebra/Order/Module/OrderedSMul.lean,Mathlib/Algebra/Quotient.lean,Mathlib/Algebra/Ring/Action/Basic.lean,Mathlib/Algebra/Ring/Action/End.lean,Mathlib/Algebra/Ring/Defs.lean,Mathlib/Algebra/Ring/Ext.lean,Mathlib/Algebra/Symmetrized.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Basic.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Basic.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Point.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Basic.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Point.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean,Mathlib/AlgebraicGeometry/Spec.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/AlgebraicTopology/Quasicategory/Basic.lean,Mathlib/AlgebraicTopology/SimplicialSet/KanComplex.lean,Mathlib/Analysis/Analytic/CPolynomialDef.lean,Mathlib/Analysis/Calculus/Deriv/Prod.lean,Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean,Mathlib/Analysis/Calculus/FDeriv/Equiv.lean,Mathlib/Analysis/Calculus/FDeriv/Mul.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/Analysis/Calculus/ParametricIntegral.lean,Mathlib/Analysis/Convex/Cone/Basic.lean,Mathlib/Analysis/Convex/EGauge.lean,Mathlib/Analysis/Normed/Group/Lemmas.lean,Mathlib/Analysis/Normed/Group/Uniform.lean,Mathlib/Analysis/ODE/PicardLindelof.lean,Mathlib/Analysis/RCLike/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Pow/Real.lean,Mathlib/CategoryTheory/Bicategory/Adjunction/Mate.lean,Mathlib/CategoryTheory/Closed/Enrichment.lean,Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean,Mathlib/CategoryTheory/Enriched/HomCongr.lean,Mathlib/CategoryTheory/Functor/Basic.lean,Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean,Mathlib/CategoryTheory/Limits/Preserves/Over.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean,Mathlib/CategoryTheory/MorphismProperty/Representable.lean,Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean,Mathlib/CategoryTheory/Sites/Grothendieck.lean,Mathlib/CategoryTheory/Sites/SheafOfTypes.lean,Mathlib/CategoryTheory/Types.lean,Mathlib/Condensed/Explicit.lean,Mathlib/Condensed/Light/Explicit.lean,Mathlib/Data/Complex/Order.lean,Mathlib/Data/Finset/Basic.lean,Mathlib/Data/Finset/Defs.lean,Mathlib/Data/Finset/Lattice/Basic.lean,Mathlib/Data/Finset/Lattice/Fold.lean,Mathlib/Data/Finsupp/Defs.lean,Mathlib/Data/Finsupp/MonomialOrder.lean,Mathlib/Data/Finsupp/Single.lean,Mathlib/Data/List/Intervals.lean,Mathlib/Data/List/Shortlex.lean,Mathlib/Data/Matrix/Defs.lean,Mathlib/Data/Matrix/Mul.lean,Mathlib/Data/Nat/Prime/Int.lean,Mathlib/Data/Real/Basic.lean,Mathlib/Data/Real/Pi/Bounds.lean,Mathlib/Data/Set/Finite/Basic.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/FieldTheory/LinearDisjoint.lean,Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean,Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean,Mathlib/GroupTheory/Coxeter/Inversion.lean,Mathlib/GroupTheory/Coxeter/Length.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/GroupTheory/GroupExtension/Basic.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/GroupTheory/Perm/Finite.lean,Mathlib/LinearAlgebra/BilinearForm/Properties.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean,Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean,Mathlib/LinearAlgebra/FreeModule/StrongRankCondition.lean,Mathlib/LinearAlgebra/InvariantBasisNumber.lean,Mathlib/LinearAlgebra/LinearDisjoint.lean,Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean,Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean,Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Symmetric.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/Logic/Equiv/Prod.lean,Mathlib/Logic/Equiv/Sum.lean,Mathlib/MeasureTheory/Function/ContinuousMapDense.lean,Mathlib/MeasureTheory/Group/Prod.lean |
161 |
4 |
['Ruben-VandeVelde', 'YaelDillies', 'github-actions', 'leanprover-community-bot-assistant'] |
nobody |
0-43267 12 hours ago |
0-43267 12 hours ago |
1-40488 1 day |
24107 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(GroupTheory/GroupAction/Basic): equivalences between stabilizers |
Define equivalence between stabilizers.
This is concurrent PR to #24039
with a diffferent syntax that fits better my later applications.
This one a `MulEquiv`from `stabilizer G a` to `stabilizer G b` associated with `g : G`
and an equality `hg : b = g · a`.
(The first commit gave the other direction, this one looks preferable.)
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
label:t-algebra$ |
93/17 |
Mathlib/Algebra/Group/End.lean,Mathlib/GroupTheory/GroupAction/Basic.lean,Mathlib/GroupTheory/GroupAction/ConjAct.lean |
3 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
riccardobrasca assignee:riccardobrasca |
0-21218 5 hours ago |
0-21219 5 hours ago |
27-24599 27 days |
24296 |
Ruben-VandeVelde author:Ruben-VandeVelde |
chore: deprecate ltByCases and ltTrichotomy |
These are unused in mathlib and don't seem likely to become useful in the future.
---
[](https://gitpod.io/from-referrer/)
|
t-order
merge-conflict
|
43/6 |
Mathlib/Order/Basic.lean,Mathlib/Order/Defs/LinearOrder.lean |
2 |
2 |
['github-actions', 'leanprover-community-bot-assistant'] |
nobody |
0-8649 2 hours ago |
0-8650 2 hours ago |
20-75899 20 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 |
15224 |
AnthonyBordg author:AnthonyBordg |
feat(CategoryTheory/Sites): covering families and their associated Grothendieck topology |
Define covering families on a category and their associated Grothendieck topology by using the API for `Coverage`.
Give an explicit characterization of the covering sieves of the said topology.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
awaiting-author
|
112/0 |
Mathlib.lean,Mathlib/CategoryTheory/Sites/CoveringFamilies.lean |
2 |
20 |
['AnthonyBordg', 'adamtopaz', 'dagurtomas', 'github-actions', 'joelriou'] |
nobody |
281-17810 9 months ago |
286-11475 9 months ago |
1-48443 1 day |
14563 |
awueth author:awueth |
feat: if-then-else of exclusive or statement |
---
If `¬(P ∧ Q)` then `ite (P ∨ Q) a 1 = (ite P a 1) * (ite Q a 1)`
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
awaiting-author
label:t-algebra$ |
5/0 |
Mathlib/Algebra/Group/Basic.lean |
1 |
3 |
['eric-wieser', 'github-actions', 'kim-em'] |
nobody |
271-35186 8 months ago |
271-35186 8 months ago |
6-38745 6 days |
11207 |
luigi-massacci author:luigi-massacci |
feat(Topology/MetricSpace): Add new file with type of Katetov maps |
add a type of Katetov maps (one point extensions of a metric) and related notation and FunLike coercions.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
WIP
|
138/0 |
Mathlib.lean,Mathlib/Topology/MetricSpace/Katetov.lean,docs/references.bib |
3 |
16 |
['fpvandoorn', 'jcommelin', 'kim-em', 'luigi-massacci', 'urkud'] |
nobody |
267-19563 8 months ago |
369-21648 1 year ago |
26-83567 26 days |
11090 |
pangelinos author:pangelinos |
feat: define spectral spaces and prove that a quasi-compact open of a spectral space is spectral |
Define spectral spaces and prove that a quasi-compact open of a spectral space is spectral.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
please-adopt
good first issue
|
69/0 |
Topology/Spectral/basic.lean |
1 |
15 |
['YaelDillies', 'adomani', 'j-loreaux', 'jcommelin', 'kim-em', 'pangelinos'] |
nobody |
267-19438 8 months ago |
271-32364 8 months ago |
16-44803 16 days |
15121 |
Eloitor author:Eloitor |
feat: iff theorems for IsSplitEpi and IsSplitMono in opposite category |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
awaiting-author
|
40/0 |
Mathlib/CategoryTheory/EpiMono.lean |
1 |
3 |
['github-actions', 'joelriou', 'mattrobball'] |
nobody |
253-81330 8 months ago |
285-40589 9 months ago |
7-3203 7 days |
16773 |
arulandu author:arulandu |
feat(Probability/Distributions): formalize Beta distribution |
Formalize Beta distribution, using Gamma distribution as a reference. Added real-valued beta wrapper, in the manner of gamma. Thanks to @EtienneC30 for help with casting real <-> complex.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-measure-probability
awaiting-author
|
286/1 |
Mathlib.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Probability/Distributions/Beta.lean |
3 |
48 |
['EtienneC30', 'arulandu', 'github-actions', 'vihdzp'] |
arulandu assignee:arulandu |
235-41547 7 months ago |
240-38265 7 months ago |
1-21124 1 day |
14237 |
js2357 author:js2357 |
feat: Define the localization of a fractional ideal at a prime ideal |
Define the localization of a fractional ideal at a prime ideal, and prove some basic properties.
---
This PR is part 3 out of 4 of a proof of `isDedekindDomain_iff_isDedekindDomainDvr`.
Part 4 is available here: #14242
- [x] depends on: #14099 Part 1
- [x] depends on: #14216 Part 2
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
awaiting-author
label:t-algebra$ |
230/0 |
Mathlib.lean,Mathlib/RingTheory/FractionalIdeal/LocalizedAtPrime.lean,Mathlib/RingTheory/Localization/Basic.lean |
3 |
20 |
['Vierkantor', 'YaelDillies', 'github-actions', 'js2357', 'kbuzzard', 'leanprover-community-mathlib4-bot'] |
Vierkantor assignee:Vierkantor |
231-20391 7 months ago |
231-20509 7 months ago |
26-39463 26 days |
14603 |
awueth author:awueth |
feat: degree is invariant under graph isomorphism |
---
Mathlib has the definition `SimpleGraph.Iso.mapNeighborSet` which is an equivalence between neighbor sets induced by an isomorphism. Would it be beneficial to add the same equivalence for `neighborFinset`?
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
WIP
|
24/0 |
Mathlib/Combinatorics/SimpleGraph/Map/Finite.lean |
1 |
11 |
['awueth', 'github-actions', 'jcommelin', 'kim-em', 'urkud'] |
nobody |
203-13932 6 months ago |
203-13932 6 months ago |
31-44440 31 days |
12799 |
jstoobysmith author:jstoobysmith |
feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group |
Add properties of the special unitary group, mirroring the properties of found in Algebra/Star/Unitary.lean. In particular, I add an instance of `specialUnitaryGroup` as a `Group`, `Star`, `InvolutiveStar`, and `StarMul`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
please-adopt
awaiting-author
label:t-algebra$ |
78/0 |
Mathlib/LinearAlgebra/UnitaryGroup.lean |
1 |
7 |
['chrisflav', 'jcommelin'] |
nobody |
195-19550 6 months ago |
195-19550 6 months ago |
9-22007 9 days |
15809 |
archiebrowne author:archiebrowne |
feat(RingTheory/MvPolynomial/Ideal): introduce new lemmas about MvPolynomial Ideals |
Four new lemmas about MvPolynomialIdeals `sub_span_span_sub`, `span_eq_iff_basis_sub`, `mem_basis_mem_span`, `mem_span_exists_dvd_mem_basis`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
awaiting-author
label:t-algebra$ |
38/0 |
Mathlib/RingTheory/MvPolynomial/Ideal.lean |
1 |
6 |
['Ruben-VandeVelde', 'github-actions', 'riccardobrasca'] |
riccardobrasca assignee:riccardobrasca |
176-16716 5 months ago |
231-18636 7 months ago |
41-7533 41 days |
20029 |
FrederickPu author:FrederickPu |
Allow for Config attributes to be set directly |
Allow for Config attributes to be set directly when using initialize_simp_projection as per issue #19895
Basically modified initialize_simp_projection so that the user has the option of specifying a tuple of config option values.
Ex:
```
initialize_simp_projection MulEquiv (toFun → apply, invFun → symm_apply) (fullyApplied := false)
```
These config options are then converted into projections.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
WIP
|
34/4 |
Mathlib/Tactic/Simps/Basic.lean |
1 |
10 |
['FrederickPu', 'YaelDillies', 'fpvandoorn', 'github-actions'] |
nobody |
145-85174 4 months ago |
146-33883 4 months ago |
0-34081 9 hours |
18461 |
hannahfechtner author:hannahfechtner |
feat: left and right common multiples mixins |
add mixins for left and right common multiples. These carry the data of what factors are used to create the common multiples
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
awaiting-author
label:t-algebra$ |
78/0 |
Mathlib/Algebra/Group/Defs.lean |
1 |
13 |
['github-actions', 'hannahfechtner', 'jcommelin', 'kbuzzard', 'kim-em', 'trivial1711'] |
nobody |
113-38467 3 months ago |
113-38467 3 months ago |
69-35596 69 days |
20797 |
vbeffara author:vbeffara |
feat(Topology/Covering): CM version of eq_of_comp_eq |
Add equivalents of the lemmas `IsCoveringMap.eq_of_comp_eq` and `IsCoveringMap.const_of_comp_CM` for the case of bundled `ContinuousMap` parameters.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
easy
awaiting-author
|
9/1 |
Mathlib/Topology/Covering.lean |
1 |
4 |
['github-actions', 'ocfnash', 'vbeffara'] |
nobody |
113-25232 3 months ago |
114-26185 3 months ago |
2-77310 2 days |
13685 |
niklasmohrin author:niklasmohrin |
feat(Combinatorics): add definitions for network flows |
Although we might not have any super-interesting results ready for mathlib yet, I feel that the definitions from this commit are already mature enough to include.
These definitions are ported from last semester's work we did at https://github.com/niklasmohrin/lean-seminar-2023 and I have put some time in to refactor our code to `Int` and now to any parameter `R`. In the linked repository, there is some more stuff that I can send in.
One obstacle without integer values is that it is not clear why a maximum flow would exist. I think the best way to tackle this would be to prove max-flow-min-cut theorem and implement the Ford-Fulkerson algorithm. It has been pointed out on Zulip that there is an [Isabelle formalization of the Edmonds Karp Algorithm](https://www.isa-afp.org/entries/EdmondsKarp_Maxflow.html).
I feel that the definitions are pretty solid and it makes sense to include them, even if just for unifying definitions across downstream projects.
---
[](https://gitpod.io/from-referrer/) |
new-contributor
t-combinatorics
awaiting-author
|
244/0 |
Mathlib.lean,Mathlib/Combinatorics/Flow/Basic.lean,docs/references.bib |
3 |
56 |
['Shreyas4991', 'YaelDillies', 'b-mehta', 'github-actions', 'madvorak', 'niklasmohrin'] |
nobody |
91-46258 3 months ago |
91-46258 3 months ago |
86-21072 86 days |
19582 |
yu-yama author:yu-yama |
feat(GroupExtension/Abelian): define `OfMulDistribMulAction.equivH2` |
Mainly defines:
- `structure GroupExtension.OfMulDistribMulAction N G [MulDistribMulAction G N]`: group extensions of `G` by `N` where the multiplicative action of `G` on `N` is the conjugation
- `structure GroupExtension.OfMulDistribMulActionWithSection N G [MulDistribMulAction G N]`: group extensions with specific choices of sections
- `def GroupExtension.OfMulDistribMulAction.equivH2`: a bijection between the equivalence classes of group extensions and $H^2 (G, N)$
- [x] depends on: #20802 (split PR: contains changes to the `Defs` file)
- [x] depends on: #20998 (split PR: mainly adds the `Basic` file)
- [ ] depends on: #21837 (split PR: adds the first part of the `Abelian` file)
---
Here is a relevant TODO in Mathlib:
https://github.com/leanprover-community/mathlib4/blob/4e9fa40d7c480937e09cd6e47a591bd6f3b8be42/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean#L46-L48
I would appreciate your comments.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
blocked-by-other-PR
label:t-algebra$ |
736/14 |
Mathlib.lean,Mathlib/GroupTheory/GroupExtension/Abelian.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,docs/references.bib |
4 |
3 |
['erdOne', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
89-3173 3 months ago |
89-6947 3 months ago |
43-23183 43 days |
13442 |
dignissimus author:dignissimus |
feat: mabel tactic for multiplicative abelian groups |
Mabel tactic for multiplicative abelian groups (#10361)
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
modifies-tactic-syntax
awaiting-author
help-wanted
|
439/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/MAbel.lean,MathlibTest/mabel.lean |
4 |
10 |
['BoltonBailey', 'dignissimus', 'github-actions', 'joneugster', 'kbuzzard'] |
joneugster assignee:joneugster |
82-77395 2 months ago |
87-58991 2 months ago |
0-16 16 seconds |
21501 |
sksgurdldi author:sksgurdldi |
feat(List): add sum_zipWith_eq_finset_sum |
### **Description:**
This PR adds the lemma `List.sum_zipWith_eq_finset_sum` to `Mathlib.Algebra.BigOperators.Group.Finset.Basic`.
#### **Statement:**
The sum of the `zipWith` operation on two lists equals the sum of applying the operation to corresponding elements of the two lists, indexed over the minimum of their lengths.
#### **Formal Statement:**
```lean
lemma sum_zipWith_eq_finset_sum [Inhabited α] [Inhabited β] [AddCommMonoid γ]
{op : α → β → γ}
(l : List α) (m : List β) :
(List.zipWith op l m).sum =
∑ x ∈ (Finset.range (Nat.min l.length m.length)), op (l[x]!) (m[x]!)
```
#### **Remarks:**
- This lemma provides a useful equivalence between `List.zipWith` and summation over a `Finset.range` indexed by `Nat.min l.length m.length`.
- It can be helpful in algebraic manipulations involving list-based summations.
#### **Dependencies:**
No additional dependencies.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
awaiting-author
label:t-algebra$ |
43/0 |
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean |
1 |
1 |
['github-actions', 'j-loreaux'] |
nobody |
82-76474 2 months ago |
82-76474 2 months ago |
13-33168 13 days |
22302 |
CharredLee author:CharredLee |
feat: add `CategoryTheory.Topos.Power` |
This is a continuation of #21281 with the end goal of defining topoi in Mathlib. It introduces the notion of a power object in a category with a subobject classifier, which is a special case of an internal hom.
The definition `HasPowerObjects C` contained in this PR is all that remains before `IsTopos C` can be defined.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
awaiting-author
|
312/0 |
Mathlib.lean,Mathlib/CategoryTheory/Topos/Power.lean |
2 |
2 |
['github-actions', 'joelriou'] |
b-mehta assignee:b-mehta |
76-77670 2 months ago |
76-78797 2 months ago |
0-1528 25 minutes |
22390 |
YunkaiZhang233 author:YunkaiZhang233 |
feat(CategoryTheory): implemented proofs for factorisation categories being equivalent to iterated comma categories in two ways |
Completed one of the tasks in TODOs, shown and implemented the details for `(X/C)/f ≌ Factorisation f ≌ f/(C/Y)`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
awaiting-author
|
112/1 |
Mathlib/CategoryTheory/Category/Factorisation.lean |
1 |
9 |
['YunkaiZhang233', 'github-actions', 'joelriou'] |
nobody |
71-31903 2 months ago |
74-27375 2 months ago |
0-6513 1 hour |
22159 |
shetzl author:shetzl |
feat: add definition of pushdown automata |
Add the definition of pushdown automata and their two acceptance conditions: acceptance based on empty stack and acceptance based on final state.
Co-authored-by: Tobias Leichtfried
---
[](https://gitpod.io/from-referrer/)
|
t-computability
new-contributor
awaiting-author
|
70/0 |
Mathlib.lean,Mathlib/Computability/PDA.lean |
2 |
34 |
['YaelDillies', 'github-actions', 'madvorak', 'shetzl'] |
nobody |
57-38817 1 month ago |
57-38817 1 month ago |
20-81771 20 days |
18091 |
tukamilano author:tukamilano |
feat: Hoeffding's lemma |
Formalize Hoeffding's lemma using the property of cumulant.
Co-authored-by: Yuma Mizuno [mizuno.y.aj@gmail.com](mailto:mizuno.y.aj@gmail.com)
---
- [x] depends on: #20151 |
large-import
new-contributor
t-measure-probability
awaiting-author
|
339/0 |
Mathlib.lean,Mathlib/Probability/Hoeffding.lean,Mathlib/Probability/Moments/Basic.lean,Mathlib/Probability/Moments/MGFAnalytic.lean,docs/references.bib |
5 |
55 |
['RemyDegenne', 'YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'tukamilano', 'yuma-mizuno'] |
tukamilano assignee:tukamilano |
54-30433 1 month ago |
54-30441 1 month ago |
1-58489 1 day |
22137 |
grunweg author:grunweg |
feat: `IsEmbedding.sumElim_of_separatingNhds` |
Characterise when the `Sum.elim` of two inducing maps resp. embeddings is an embedding,
and deduce that the ranges of the two maps lying in separated neighbourhoods suffices.
This will be used in my bordism theory project.
------------
- [x] depends on: #22827 (for breaking the import cycle)
- [ ] depends on: #22969
- [ ] depends on: #22964
- [ ] depends on: #23371 (for the previous PR)
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
awaiting-author
blocked-by-other-PR
|
209/10 |
Mathlib/Data/Set/Image.lean,Mathlib/Data/Sum/Basic.lean,Mathlib/Order/Filter/Map.lean,Mathlib/Topology/Constructions/SumProd.lean |
4 |
22 |
['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'plp127'] |
nobody |
47-21804 1 month ago |
47-21807 1 month ago |
0-0 0 seconds |
22355 |
xyzw12345 author:xyzw12345 |
feat(Algebra/RingQuot): Some lemmas about `RingQuot.mkAlgHom` and `RingQuot.mkRingHom` |
This PR provides a few basic lemmas about `RingQuot.mkRingHom` and `RingQuot.mkAlgHom`. These lemmas are about when are two elements mapped to the same one under these two maps, and they correspond to the lemma `Quot.eq`.
PR #22279 depends on these lemmas.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
awaiting-author
label:t-algebra$ |
16/0 |
Mathlib/Algebra/RingQuot.lean |
1 |
13 |
['Paul-Lez', 'erdOne', 'eric-wieser', 'github-actions', 'ocfnash', 'xyzw12345'] |
nobody |
41-52050 1 month ago |
42-39373 1 month ago |
32-33842 32 days |
22639 |
b-reinke author:b-reinke |
feat(Mathlib/GroupTheory/FreeGroup): theory of (cyclically) reduced words |
Upstreamed from the [EquationalTheories](https://github.com/teorth/equational_theories) project.
This PR defines in the new file `Mathlib/GroupTheory/FreeGroup/ReducedWords.lean` some extra lemmas for free groups, in particular about (cyclically) reduced words.
## Main declarations
* `FreeGroup.Red.reduced`: the predicate for reduced words
* `FreeGroup.Red.cyclicallyReduced`: the predicate for cyclically reduced words
## Main statements
* `FreeGroup.infinite_order`: nontrivial elements of a free group have infinite order
* `FreeGroup.zpow_left_injective`: taking n-th powers is an injective function on the free group
Co-authored-by: Amir Livne Bar-on
- [ ] depends on: #23366
- [ ] depends on: #23367
- [ ] depends on: #23368
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
blocked-by-other-PR
label:t-algebra$ |
429/0 |
Mathlib.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/GroupTheory/FreeGroup/Reduce.lean,Mathlib/GroupTheory/FreeGroup/ReducedWords.lean |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
37-2078 1 month ago |
47-33526 1 month ago |
20-75471 20 days |
20671 |
thefundamentaltheor3m author:thefundamentaltheor3m |
feat(Analysis/Asymptotics/SpecificAsymptotics): Proving that 𝛔ₖ(n) = O(nᵏ⁺¹) |
This PR proves a result about the $\sigma_k(n)$ arithmetic function, namely, that it is $O\left(n^{k+1}\right)$. Main theorem:
`theorem sigma_asymptotic (k : ℕ) : (fun n ↦ (σ k n : ℝ)) =O[atTop] (fun n ↦ (n ^ (k + 1) : ℝ))`
This result was proved as part of the sphere packing project.
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-number-theory
awaiting-author
|
29/0 |
Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean |
1 |
2 |
['b-mehta', 'github-actions'] |
b-mehta assignee:b-mehta |
36-21333 1 month ago |
46-15810 1 month ago |
9-59130 9 days |
21903 |
yhtq author:yhtq |
feat: add from/toList between `FreeSemigroup` and `List` with relative theorems |
Add from/toList between `FreeSemigroup` and `List` with relative theorems, as well as an incidental definition of lexicographic order on `FreeSemigroup`.
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-algebra
awaiting-CI
label:t-algebra$ |
169/0 |
Mathlib/Algebra/Free.lean |
1 |
11 |
['YaelDillies', 'github-actions'] |
nobody |
35-54143 1 month ago |
35-54143 1 month ago |
51-9403 51 days |
22657 |
Xmask19 author:Xmask19 |
feat: a graph is maximally acyclic iff it is a tree |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
|
86/0 |
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean |
1 |
6 |
['Rida-Hamadani', 'b-mehta', 'github-actions', 'grunweg'] |
b-mehta assignee:b-mehta |
35-19800 1 month ago |
35-19821 1 month ago |
57-10498 57 days |
22018 |
maddycrim author:maddycrim |
feat(RingTheory/Localization/Pi): localization of a finite direct product where each semiring in product has maximal nilradical is a projection |
For noncomputable def `surjectivePiNilradicalIsMaximal` : Let `M` be a submonoid of a direct product of commutative rings `R i`.
If each `R i` has maximal nilradical then the direct product `∏ R i` surjects onto the
localization of `∏ R i` at `M`.
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-algebra
label:t-algebra$ |
28/0 |
Mathlib/RingTheory/Localization/Pi.lean |
1 |
24 |
['Paul-Lez', 'alreadydone', 'erdOne', 'github-actions', 'grunweg', 'jcommelin', 'maddycrim'] |
nobody |
35-17646 1 month ago |
37-12714 1 month ago |
83-85939 83 days |
22790 |
mhk119 author:mhk119 |
feat: Extend `taylor_mean_remainder_lagrange` to `x < x_0` |
The `taylor_mean_remainder_lagrange` theorem has the assumption that $x_0 < x$. In many applications, we need $x < x_0$ and one cannot use the current version to obtain this (see [zulip](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Taylor's.20theorem)). This PR introduces a set of theorems that push negations through Taylor expansions so that one can extend `taylor_mean_remainder_lagrange` to the case when $x < x_0$. These theorems should also be useful elsewhere since they are quite general. |
new-contributor
t-analysis
awaiting-author
|
92/1 |
Mathlib/Analysis/Calculus/Deriv/Basic.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/Analysis/Calculus/Taylor.lean |
3 |
10 |
['Paul-Lez', 'github-actions', 'grunweg'] |
nobody |
33-27296 1 month ago |
33-27296 1 month ago |
30-77130 30 days |
23949 |
Louddy author:Louddy |
feat: SkewPolynomial |
# Univariate skew polynomials
Skew polynomials are represented as `SkewMonoidAlgebra R (Multiplicative ℕ)`, where `R` is usually at least a Semiring.
In this file, we define `SkewPolynomial` and provide basic instances.
This is currently missing the definition of `coeff` and `single` as they require a more advance interface of `SkewMonoidAlgebra` which is still WIP (See TODOs in file).
Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)>
---
- [ ] depends on: #22078
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-algebra
blocked-by-other-PR
label:t-algebra$ |
600/42 |
Mathlib.lean,Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean,Mathlib/Algebra/SkewPolynomial/Basic.lean,docs/references.bib |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
32-20750 1 month ago |
32-20751 1 month ago |
0-2389 39 minutes |
24041 |
YuvalFilmus author:YuvalFilmus |
feat: add support for bigop binders of the form "not in" and "not equal" |
feat: add support for bigop binders of the form "not in" and "not equal"
Added two new binders which can be used with big operators (product and summation).
The first, "not in", translates into "in ... complement".
The second, "not equal to", translates to `univ.erase ...`.
Also, improved documentation in the file header.
Delaboration updates can be considered next if wanted (to be coordinated with #22048).
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
7/0 |
Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean |
1 |
1 |
['github-actions'] |
nobody |
29-18426 29 days ago |
29-19727 29 days ago |
29-19782 29 days |
23637 |
kirilvino author:kirilvino |
feat(Combinatorics/SimpleGraph): every circuit contains a cycle proof |
circuit to cycle proof
---
This PR uses the bypass definition in a new function for closed walks that removes repeated vertices. Then proves if the closed walk given is a circuit, that the result from this function is a cycle. This is then packaged up similar to the existing ToPath definition, creating a way of transforming a circuit into a cycle.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-combinatorics
awaiting-author
|
26/0 |
Mathlib/Combinatorics/SimpleGraph/Path.lean |
1 |
8 |
['b-mehta', 'github-actions', 'kirilvino'] |
nobody |
26-37232 26 days ago |
26-83853 26 days ago |
13-19789 13 days |
22582 |
vlad902 author:vlad902 |
feat: generalize theorems with linter fixes |
This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile. Otherwise, the type class is not being generalized, but can simply be replaced by implicit type class synthesis (or an implicit type class in a variable block being pulled in.)
The linter currently output debug statements indicating source file positions where type classes should be generalized, and a script then makes those edits. This file contains a subset of those generalizations. The linter and the script performing re-writes is available in commit 7b436512017640c3c33aea50b2435b2ee0d995c9.
Note that this PR specifically generalizes theorems across a range of files and type classes, the common theme is that the resulting changes all cause type classes in variable declarations to go unused.
Also see discussion on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855 |
new-contributor
t-algebra
t-analysis
label:t-algebra$ |
30/50 |
Mathlib.lean,Mathlib/Algebra/Algebra/Basic.lean,Mathlib/Algebra/Group/Action/Faithful.lean,Mathlib/Algebra/GroupWithZero/Action/Faithful.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Operator/Compact.lean,Mathlib/GroupTheory/Perm/Subgroup.lean,Mathlib/Topology/Algebra/ConstMulAction.lean |
8 |
11 |
['github-actions', 'urkud', 'vlad902'] |
urkud assignee:urkud |
25-85142 25 days ago |
25-85142 25 days ago |
68-66074 68 days |
22925 |
ggranberry author:ggranberry |
feat(Mathlib/PlaceHolder/ToeplitzHausdorff): Toeplitz-Hausdorff |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-analysis
awaiting-author
WIP
help-wanted
|
411/0 |
Mathlib/PlaceHolder/ToeplitzHausdorff.lean,Mathlib/PlaceHolder/ToeplitzHausdorff_v2.lean |
2 |
10 |
['faenuccio', 'ggranberry', 'github-actions'] |
faenuccio assignee:faenuccio |
25-84030 25 days ago |
25-84030 25 days ago |
4-24257 4 days |
11968 |
JovanGerb author:JovanGerb |
feat: improvements to RefinedDiscrTree |
This PR defines `RefinedDiscrTree`, which is an improved version of `DiscrTree` with many new features, such as
- indexing lambda terms, dependent forall terms, and bound variables.
- giving a score to matches, in order to sort them
- indexing star patterns so that `a+b` and `a+a` are indexed differently
- taking into account eta reductions, so that `exp` can still be matched with the library pattern `fun x => exp (f x)`.
This PR makes `RefinedDiscrTree` into a lazy data structure, meaning that it can be used without a cache, just like `LazyDiscrTree`.
This PR also removes these features:
- indexing `fun x => x` as `id`
- indexing `fun x => f x + g x` as `f + g`, and similarly for `-`, `*`, `/`, `⁻¹`, `^`.
- indexing `fun _ => 42` as `42`
These equivalent indexings do not hold definitionally in the `reducible` transparency, which is the transparency that is used for unification when using a discrimination tree. Therefore, indexing these different expressions the same is actually inefficient rather than helpful.
This is part of the bigger #11768, which uses this discrimination tree for a library rewriting tactic.
This replaces an older version of `RefinedDiscrTree`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
|
1631/1242 |
Mathlib.lean,Mathlib/Lean/Meta/RefinedDiscrTree.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Pi.lean,Mathlib/Tactic.lean,Mathlib/Tactic/FunProp.lean,Mathlib/Tactic/FunProp/Elab.lean,Mathlib/Tactic/FunProp/StateList.lean,Mathlib/Tactic/FunProp/Theorems.lean,Mathlib/Tactic/FunProp/Types.lean,Mathlib/Topology/Defs/Basic.lean,MathlibTest/RefinedDiscrTree.lean,scripts/noshake.json |
16 |
78 |
['0art0', 'JovanGerb', 'eric-wieser', 'github-actions', 'grunweg', 'joneugster', 'leanprover-bot', 'rosborn'] |
nobody |
25-79663 25 days ago |
36-77566 1 month ago |
211-15928 211 days |
23338 |
WilliamCoram author:WilliamCoram |
feat: restricted power series form a ring |
We define restricted powerseries over a normed ring R, and show they form a ring when R has the ultrametric property.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-number-theory
|
186/0 |
Mathlib.lean,Mathlib/RingTheory/PowerSeries/Restricted.lean |
2 |
17 |
['Paul-Lez', 'WilliamCoram', 'github-actions', 'grunweg'] |
nobody |
22-82283 22 days ago |
48-24010 1 month ago |
48-24131 48 days |
23990 |
robertmaxton42 author:robertmaxton42 |
feat (Types.Colimits): Quot is functorial and colimitEquivQuot is natural |
Add `Functor.quotFunctor` to parallel `Functor.sectionsFunctor`, witnessing that `Quot` is functorial; add `colimNatIsoQuotFunctor` to parallel `limNatIsoSectionsFunctor`, witnessing that `colimitEquivQuot` is natural in the diagram $F$.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
awaiting-author
|
33/0 |
Mathlib/CategoryTheory/Limits/Types/Colimits.lean |
1 |
4 |
['github-actions', 'joelriou', 'robertmaxton42'] |
nobody |
22-15425 22 days ago |
22-15425 22 days ago |
8-28043 8 days |
22620 |
ahhwuhu author:ahhwuhu |
feat: Define shifted Legendre polynomials and prove some basic properties |
Define shifted Legendre polynomials and prove that it is integer polynomial. In the same time, its evaluation on x is equal to the evaluation on 1 - x.
|
new-contributor
t-analysis
awaiting-author
|
123/0 |
Mathlib.lean,Mathlib/Analysis/ShiftedLegendrePoly.lean |
2 |
20 |
['acmepjz', 'ahhwuhu', 'b-mehta', 'github-actions', 'riccardobrasca'] |
nobody |
21-41482 21 days ago |
24-80266 24 days ago |
43-62882 43 days |
18693 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: add ConjRootClass |
Co-authored-by: FR
---
From #6718
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
213/0 |
Mathlib.lean,Mathlib/FieldTheory/Minpoly/ConjRootClass.lean,Mathlib/FieldTheory/Minpoly/IsConjRoot.lean |
3 |
13 |
['LessnessRandomness', 'Vierkantor', 'alreadydone', 'github-actions', 'grunweg'] |
nobody |
19-8043 19 days ago |
19-45806 19 days ago |
81-27551 81 days |
22349 |
dtumad author:dtumad |
feat(Control): Laws for monads with compatible `failure` operation |
Add a class for a `Monad` that also has an `Alternative` instance, and a class `LawfulAlternative` for types where the failure and monad structures are compatible in the expected way.
---
I'm not sure if this should instead go in `Batteries.Control` instead of mathlib, or at least lemmas like `OptionT.run_failure` maybe should. Some of the instances like `Set` would still need to be added in mathlib either way.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
WIP
|
74/3 |
Mathlib.lean,Mathlib/Control/Lawful.lean,Mathlib/Control/Monad/AlternativeMonad.lean |
3 |
8 |
['dtumad', 'eric-wieser', 'github-actions', 'quangvdao'] |
nobody |
17-55324 17 days ago |
17-55478 17 days ago |
1-20563 1 day |
20913 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): Define the associated graded ring to filtered ring. |
Define the associated graded ring to a filtered ring.
---
- [x] depends on: #20900
- [x] depends on: #22230
- [ ] depends on: #22631
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
blocked-by-other-PR
label:t-algebra$ |
442/0 |
Mathlib.lean,Mathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
17-41616 17 days ago |
68-28913 2 months ago |
0-70480 19 hours |
21806 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): associated graded algebra |
Define the associated graded algebra of a filtered algebra, constructed from a special case of associated graded ring.
---
- [x] depends on: #20900
- [ ] depends on: #20913
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
blocked-by-other-PR
WIP
label:t-algebra$ |
552/0 |
Mathlib.lean,Mathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean |
2 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
17-41583 17 days ago |
unknown |
unknown |
20940 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): Associated graded module |
Define the associated graded module to a filtered module.
---
- [x] depends on: #20900
- [ ] depends on: #20913
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
blocked-by-other-PR
WIP
label:t-algebra$ |
656/0 |
Mathlib.lean,Mathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean |
2 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
17-41555 17 days ago |
79-29617 2 months ago |
0-1265 21 minutes |
22632 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): define filtered add group hom |
In this file we define filtered hom and the corresponding associated graded hom for abelian groups.
Co-authored-by: Huanyu Zheng @Yu-Misaka
Co-authored-by: Yi Yuan @yuanyi-350
Co-authored-by: Weichen Jiao @AlbertJ-314
---
- [ ] depends on: #22631
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
blocked-by-other-PR
label:t-algebra$ |
378/0 |
Mathlib.lean,Mathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean,Mathlib/RingTheory/FilteredAlgebra/FilteredHom.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
17-41209 17 days ago |
68-15676 2 months ago |
0-1204 20 minutes |
22208 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra):filtered ring hom |
In this PR, we define the filtered ring morphisms on rings and prove some basic properties of
them.
Co-authored-by: Huanyu Zheng @Yu-Misaka
Co-authored-by: Yi Yuan @yuanyi-350
Co-authored-by: Weichen Jiao @AlbertJ-314
---
- [ ] depends on: #20913
- [ ] depends on: #22632
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
blocked-by-other-PR
label:t-algebra$ |
812/0 |
Mathlib.lean,Mathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean,Mathlib/RingTheory/FilteredAlgebra/FilteredHom.lean |
3 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
17-41181 17 days ago |
unknown |
unknown |
22972 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): exact of associated graded exact |
We proved that a chain complex is exact if its associated graded complex is exact.
Co-authored-by: Huanyu Zheng @Yu-Misaka
Co-authored-by: Yi Yuan @yuanyi-350
Co-authored-by: Weichen Jiao @AlbertJ-314
---
- [ ] depends on: #22632
- [x] depends on: #22705
- [ ] depends on: #22707
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
blocked-by-other-PR
label:t-algebra$ |
729/0 |
Mathlib.lean,Mathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean,Mathlib/RingTheory/FilteredAlgebra/Exactness.lean,Mathlib/RingTheory/FilteredAlgebra/FilteredHom.lean |
4 |
n/a |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
17-40954 17 days ago |
unknown |
unknown |
22707 |
Thmoas-Guan author:Thmoas-Guan |
feat(Algebra): associated graded exact of exact and strict |
In this file, we define the concept of exhaustive filtrations.
We also prove a AssociatedGradedRingHom sequence is exact iff each GradedPieceHom is exact.
And when a sequence is strict exact, the corresponding AssociatedGradedRingHom sequence is also exact.
Co-authored-by: Huanyu Zheng @Yu-Misaka
Co-authored-by: Yi Yuan @yuanyi-350
Co-authored-by: Weichen Jiao @AlbertJ-314
---
- [ ] depends on: #22632
- [x] depends on: #22705
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
blocked-by-other-PR
label:t-algebra$ |
534/0 |
Mathlib.lean,Mathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean,Mathlib/RingTheory/FilteredAlgebra/Exactness.lean,Mathlib/RingTheory/FilteredAlgebra/FilteredHom.lean |
4 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
17-40933 17 days ago |
66-39936 2 months ago |
0-464 7 minutes |
24394 |
wwylele author:wwylele |
feat(Analysis/Asymptotics): Add filter operation theorems to `IsEquivalent` |
These are simply restating the corresponding theorems for `isLittleO`, but adding them provides better discovery when one is not familiar with how `IsEquivalent` is defined.
I tagged `isEquivalent_map` as `@[simp]` because all of `isBigOWith/isBigO/isLittleO_map` are tagged, but I am not sure if this appropriate. Please let me know if I should remove the tag
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-analysis
|
13/0 |
Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean |
1 |
1 |
['github-actions'] |
nobody |
17-3342 17 days ago |
17-3342 17 days ago |
17-3401 17 days |
24448 |
Hagb author:Hagb |
feat(RingTheory/Ideal/Span.lean): some lemmas about zero and span |
`simp` would be able to solve them.
Notice that `span_singleton_zero : span {(0 : R)} = ⊥` itself can be solved by `simp` without this commit, which uses `span_singleton_eq_bot : span ({x} : Set α) = ⊥ ↔ x = 0`, while `simp` cannot solve goals like `f (Ideal.span {(0 : R)}) = f ⊥`, which would be solvable by `simp` with `span_singleton_zero` marked with `@[simp]`.
Without adding also `Ideal.dvd_span_bot` to `Mathlib/RingTheory/DedekindDomain/Ideal.lean`, these lemmas on `Span.lean` would make the following failed, since `simp` would rewrite `{0}` with `⊥` and result in a goal `v.asIdeal ∣ ⊥` that it can't solve.
https://github.com/leanprover-community/mathlib4/blob/3f2556372f27171259a381d4d57db71440700cd8/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean#L123
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
16/1 |
Mathlib/Algebra/Module/PID.lean,Mathlib/RingTheory/DedekindDomain/Ideal.lean,Mathlib/RingTheory/Ideal/Span.lean |
3 |
1 |
['github-actions'] |
nobody |
14-17445 14 days ago |
14-27436 14 days ago |
14-27489 14 days |
23992 |
robertmaxton42 author:robertmaxton42 |
feat (Limits.FunctorCategory): limitIsoFlipCompLim and colimitIsoFlipCompColim are natural |
Add `limIsoFlipCompWhiskerLim`, `limCompFlipIsoWhiskerLim`, `colimIsoFlipCompWhiskerColim`, `colimCompFlipIsoWhiskerColim`, each witnessing that their corresponding families of isomorphisms are natural in the diagram $F$.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
|
41/0 |
Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean |
1 |
2 |
['adomani', 'github-actions'] |
nobody |
11-45506 11 days ago |
30-39336 1 month ago |
30-39389 30 days |
24543 |
pfaffelh author:pfaffelh |
feat (Topology/Compactness/CompactSystem): Set system of finite unions of sets in a compact system is again a compact system |
feat (Topology/Compactness/CompactSystem): The set system of finite unions of sets in a compact system is a compact system
A compact system is a set system with the following property: If all finite intersections of a sequence in the set system is non-empty, the countable intersection is not empty.
Starting with a compact system, consider the finite unions of sets in the copact system. Such sets again form a compact system (`IsCompactSystem.union.isCompactSystem`).
---
- [x] depends on: #24541
- [x] depends on: #24542
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
blocked-by-other-PR
|
286/2 |
Mathlib/Topology/Compactness/CompactSystem.lean |
1 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
10-45552 10 days ago |
10-45552 10 days ago |
0-1830 30 minutes |
24542 |
pfaffelh author:pfaffelh |
feat (Topology/Compactness/CompactSystem): Closed and compact square cylinders form a compact system. |
feat (Topology/Compactness/CompactSystem): Closed and compact square cylinders form a
compact system.
A square cylinder is a set of the form `s.pi t` in a product space. A closed compact square cylinder has `IsClosed (t i)` and `IsCompact (t i)` for all `i ∈ s`. This set system is a compact system (as introduced in PR #24541).
Streamline the definition of square cylinders in MeasureTheory/Constructions/Cylinders on the way.
Co-authors: Rémy Degenne remy.degenne@inria.fr
---
- [x] depends on: #24541
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
blocked-by-other-PR
|
287/66 |
Mathlib/Data/Set/Prod.lean,Mathlib/MeasureTheory/Constructions/Cylinders.lean,Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean,Mathlib/Topology/Compactness/CompactSystem.lean |
4 |
3 |
['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot'] |
nobody |
10-45547 10 days ago |
10-45547 10 days ago |
0-192 3 minutes |
22809 |
b-reinke author:b-reinke |
feat: Category algebras and path algebras |
This PR defines the category algebra of a linear category and path algebras of quivers.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
t-category-theory
WIP
label:t-algebra$ |
218/0 |
Mathlib/Algebra/Ring/Assoc.lean,Mathlib/CategoryTheory/Linear/CategoryAlgebra.lean,Mathlib/Combinatorics/Quiver/PathAlgebra.lean,Mathlib/Data/DFinsupp/BigOperators.lean |
4 |
2 |
['b-reinke', 'github-actions'] |
nobody |
10-45214 10 days ago |
10-45214 10 days ago |
0-0 0 seconds |
24527 |
matthewjasper author:matthewjasper |
feat(Topology/Algebra/Module): Add more theorems for IsModuleTopology |
Add theorems that surjective linear maps to the module topology are open.
Add IsModuleTopology instance for quotients.
Add IsModuleTopology instance for finite dimensional T2 vector spaces over a complete normed field and use it to shorten some proofs.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
t-topology
label:t-algebra$ |
48/24 |
Mathlib/Topology/Algebra/Module/FiniteDimension.lean,Mathlib/Topology/Algebra/Module/ModuleTopology.lean |
2 |
5 |
['erdOne', 'github-actions', 'matthewjasper'] |
nobody |
10-13349 10 days ago |
10-30419 10 days ago |
11-85118 11 days |
23117 |
pfaffelh author:pfaffelh |
feat(MeasureTheory): finite unions of sets in a semi-ring (in terms of measure theory) form a ring |
: Finite unions of sets in a semi-ring (in terms of measure theory) form a ring
The set containing finite unions of sets in a semi-ring are a ring.
Part of `MeasureTheory.SetSemiring` is moved to the new file `MeasureTheory.SetRing`.
---
- [ ] depends on: #22714 [contains changes in `SetSemiring` as well]
|
large-import
new-contributor
t-measure-probability
blocked-by-other-PR
|
447/104 |
Mathlib.lean,Mathlib/Data/Set/Lattice.lean,Mathlib/Data/Set/Pairwise/Lattice.lean,Mathlib/Data/Set/Prod.lean,Mathlib/MeasureTheory/MeasurableSpace/Pi.lean,Mathlib/MeasureTheory/Measure/AddContent.lean,Mathlib/MeasureTheory/PiSystem.lean,Mathlib/MeasureTheory/SetAlgebra.lean,Mathlib/MeasureTheory/SetRing.lean,Mathlib/MeasureTheory/SetSemiring.lean |
10 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
9-48342 9 days ago |
11-36791 11 days ago |
0-1301 21 minutes |
23500 |
DrLSimon author:DrLSimon |
feat(MeasureTheory/Decomposition): link the clipped sub of positive measures to Jordan decomposition |
This introduces a new file `Mathlib/MeasureTheory/Decomposition/JordanSub.lean` which develops the Jordan decomposition of the signed measure `μ.toSignedMeasure - ν.toSignedMeasure` for finite measures `μ`
and `ν`, expressing it as the pair `(μ - ν, ν - μ)` of mutually singular finite measures.
The key tool is the Hahn decomposition theorem, which yields a measurable partition of the space
where `μ ≥ ν` and `ν ≥ μ`.
Some basic results of `VectorMeasure` are also provided such as `restrict_neg`, `restrict_sub` `restrict_add_restrict_compl` and `Measure.toSignedMeasure_le_iff` within the `JordanSub.lean` file. They could be moved to another more central place (I guess `VectorMeasure/Basic.lean`). Similarly, `Measure.sub_zero` could go to `Sub.lean`.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-measure-probability
help-wanted
|
218/2 |
Mathlib.lean,Mathlib/MeasureTheory/Function/Jacobian.lean,Mathlib/MeasureTheory/Measure/Decomposition/Hahn.lean,Mathlib/MeasureTheory/Measure/Sub.lean,Mathlib/MeasureTheory/VectorMeasure/Basic.lean,Mathlib/MeasureTheory/VectorMeasure/Decomposition/JordanSub.lean |
6 |
62 |
['DrLSimon', 'EtienneC30', 'github-actions', 'grunweg', 'urkud'] |
EtienneC30 assignee:EtienneC30 |
8-22711 8 days ago |
8-28558 8 days ago |
19-34493 19 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-78064 7 days ago |
7-78146 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-77933 7 days ago |
7-77942 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-77911 7 days ago |
7-77916 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-77838 7 days ago |
7-77843 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-77244 7 days ago |
7-77879 7 days ago |
75-77754 75 days |
24139 |
yuanyi-350 author:yuanyi-350 |
feat: add `Fin.cycleIcc` which rotates `range(i, j)` |
In this file, I define permutation `cycleIcc i j hij`, which is the cycle `(i i+1 .... j)` leaving `(0 ... i-1)` and `(j+1 ... n-1)` unchanged. In other words, it rotates elements in `[i, j]` one step to the right. Also I prove some properties of `cycleIcc i j hij` such as it is a cycle and its cycleType is `j - i`
**This definition is used to prove the following result:**
```
theorem succAbove_comp_cycleIcc [NeZero n] (x : Fin (n + 1) → L) (i j : Fin (n + 1)) (eq : x i = x j) (lt : i < j)
x ∘ i.succAbove = x ∘ j.succAbove ∘ (cycleIcc hij)
```
More clearly, `x ∘ i.succAbove` and `x ∘ j.succAbove` are `Fin n → L` types. For example, when `n = 6, i = 2, j = 5` and `x i = x j`
```
x ∘ i.succAbove = (x 0, x 1, x 3, x 4, x 5, x 6)
x ∘ j.succAbove = (x 0, x 1, x 2, x 3, x 4, x 6)
```
We have
```
(x 0, x 1, x 3, x 4, x 5, x 6)
--(cycleIcc)--->(x 0, x 1, x 5, x 3, x 4, x 6) = (x 0, x 1, x 2, x 3, x 4, x 6)
```
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
label:t-algebra$ |
132/1 |
Mathlib/Algebra/Group/Fin/Basic.lean,Mathlib/Data/Fin/Basic.lean,Mathlib/Data/Nat/SuccPred.lean,Mathlib/GroupTheory/Perm/Fin.lean |
4 |
26 |
['acmepjz', 'faenuccio', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'mbkybky', 'yuanyi-350'] |
nobody |
7-61338 7 days ago |
11-70024 11 days ago |
25-84327 25 days |
24616 |
bwehlin author:bwehlin |
feat(MeasureTheory/Measure/Dirac): Dirac measure applied to a measurable set is either 0 or 1 |
The Dirac measure at a point `a`, applied to a set `s`, is either 0 or 1. This feature provides two if and only ifs that can be used to turn statements in terms of `\ne` into statements in terms of `=`, as well as a "0 or 1 theorem".
(The reason for adding these is to avoid having to simplify in terms of `Set.indicator` over and over while working with Dirac) |
new-contributor
t-measure-probability
|
15/0 |
Mathlib/MeasureTheory/Measure/Dirac.lean |
1 |
1 |
['github-actions'] |
nobody |
7-32262 7 days ago |
8-7759 8 days ago |
8-7813 8 days |
19796 |
peakpoint author:peakpoint |
feat: Peano form of Taylor's theorem |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-analysis
awaiting-author
|
329/19 |
Mathlib/Algebra/Polynomial/Module/Basic.lean,Mathlib/Analysis/Calculus/LHopital.lean,Mathlib/Analysis/Calculus/MeanValue.lean,Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Convex/Topology.lean,Mathlib/Analysis/Normed/Module/Convex.lean,Mathlib/Geometry/Manifold/Instances/Real.lean,Mathlib/Order/Interval/Set/Basic.lean,Mathlib/Topology/Algebra/Module/LocallyConvex.lean |
9 |
n/a |
['RemyDegenne', 'github-actions', 'leanprover-community-bot-assistant', 'peakpoint', 'sgouezel'] |
sgouezel assignee:sgouezel |
0-25460 7 hours ago |
unknown |
unknown |
11021 |
jstoobysmith author:jstoobysmith |
feat(AlgebraicTopology) : add join of augmented SSets |
This pull-request adds the definition of the join of augmented SSets defined as contravariant functors from `WithInitial SimplexCategory` to `Type u`. In addition it shows that the join of two standard augmented SSets is again an augmented SSets.
From this the definition of the join of simplicial sets should follow easily.
To aid the above theory, an api for `WithInitial SimplexCategory` has been created, with the notion of the `join` and `split` (forming a sort of inverse to join) of objects in this category are defined.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
merge-conflict
WIP
|
2137/1 |
.gitignore,Mathlib.lean,Mathlib/AlgebraicTopology/Join.lean,Mathlib/AlgebraicTopology/SimplexCategory.lean,Mathlib/AlgebraicTopology/SimplexCategoryWithInitial.lean,Mathlib/AlgebraicTopology/SimplicialSet.lean |
6 |
47 |
['github-actions', 'jcommelin'] |
nobody |
286-42796 9 months ago |
342-37842 11 months ago |
1-20125 1 day |
12751 |
Command-Master author:Command-Master |
feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size |
Remove `@[simp]` from `Nat.bit_false` and `Nat.bit_true`, as `bit0` and `bit1` are deprecated, and add some lemmas to `Bits`, `Bitwise` and `Size`.
---
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
merge-conflict
|
66/7 |
Mathlib/Data/Nat/Bits.lean,Mathlib/Data/Nat/Bitwise.lean,Mathlib/Data/Nat/Multiplicity.lean,Mathlib/Data/Nat/Size.lean |
4 |
26 |
['Command-Master', 'Rida-Hamadani', 'Ruben-VandeVelde', 'YaelDillies', 'github-actions', 'jcommelin'] |
nobody |
267-20095 8 months ago |
272-36337 8 months ago |
54-52408 54 days |
9935 |
jstoobysmith author:jstoobysmith |
feat(AlgebraicTopology): add constructors for horns |
Added a function that given a simplicial set S and a set of n-1 simplexes satisfying certain conditions, creates a morphism in SSet from a n horn to a simplicial set S.
Included also are a series of lemmas and definitions used in this construction. In particular I define a function that takes a m-simplex in a horn, and returns the smallest 'index' of face it factors through, and give a series of lemmas related to this.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
t-topology
merge-conflict
awaiting-author
label:t-algebra$ |
462/2 |
Mathlib/AlgebraicTopology/SimplicialSet.lean |
1 |
15 |
['YaelDillies', 'jcommelin', 'jstoobysmith', 'kim-em', 'linesthatinterlace'] |
nobody |
267-19929 8 months ago |
298-21254 9 months ago |
14-58814 14 days |
10006 |
jstoobysmith author:jstoobysmith |
feat(AlgebraicTopology): homotopy in quasicategories |
Defined a homotopy between two 1-simplicies in a quasicategories, and proved the property of being homotopic forms an equivalence relation.
---
- [ ] depends on: #9935
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
merge-conflict
awaiting-author
blocked-by-other-PR
|
898/1 |
Mathlib.lean,Mathlib/AlgebraicTopology/Homotopy.lean,Mathlib/AlgebraicTopology/SimplexCategory.lean,Mathlib/AlgebraicTopology/SimplicialSet.lean |
4 |
3 |
['joelriou', 'leanprover-community-mathlib4-bot'] |
nobody |
231-45514 7 months ago |
231-45514 7 months ago |
0-0 0 seconds |
14242 |
js2357 author:js2357 |
feat: Prove equivalence of `isDedekindDomain` and `isDedekindDomainDvr` |
Prove that `isDedekindDomainDvr` is equivalent to both `isDedekindDomain` and `isDedekindDomainInv`.
Specifically, prove `isDedekindDomainDvr A → isDedekindDomainInv A`, because `isDedekindDomain A → isDedekindDomainDvr A` and `IsDedekindDomain A ↔ IsDedekindDomainInv A` are already in Mathlib.
- [x] depends on: #14099
- [x] depends on: #14216
- [ ] depends on: #14237
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
merge-conflict
blocked-by-other-PR
label:t-algebra$ |
269/1 |
Mathlib.lean,Mathlib/RingTheory/DedekindDomain/Dvr.lean,Mathlib/RingTheory/FractionalIdeal/LocalizedAtPrime.lean,Mathlib/RingTheory/Localization/Basic.lean |
4 |
2 |
['github-actions', 'leanprover-community-mathlib4-bot'] |
nobody |
231-5989 7 months ago |
231-5989 7 months ago |
0-0 0 seconds |
16888 |
metinersin author:metinersin |
feat(ModelTheory/Complexity): Define conjunctive and disjunctive normal forms |
Define `FirstOrder.Language.BoundedFormula.IsDNF` and `FirstOrder.Language.BoundedFormula.IsCNF`.
---
- [ ] depends on: #16887
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-logic
merge-conflict
blocked-by-other-PR
|
415/7 |
Mathlib/ModelTheory/Complexity.lean,Mathlib/ModelTheory/Equivalence.lean,Mathlib/ModelTheory/Syntax.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
223-1967 7 months ago |
223-1967 7 months ago |
0-1045 17 minutes |
16887 |
metinersin author:metinersin |
feat(ModelTheory/Complexity): define conjunctive and disjunctive formulas |
Defines `FirstOrder.Language.BoundedFormula.IsConjunctive` and `FirstOrder.Language.BoundedFormula.IsDisjunctive`.
---
- [ ] depends on: #16885
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-logic
merge-conflict
blocked-by-other-PR
|
300/7 |
Mathlib/ModelTheory/Complexity.lean,Mathlib/ModelTheory/Equivalence.lean,Mathlib/ModelTheory/Syntax.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
223-1967 7 months ago |
223-1968 7 months ago |
0-1299 21 minutes |
16889 |
metinersin author:metinersin |
feat(ModelTheory/Complexity): Normal forms |
Defines `FirstOrder.Language.BoundedFormula.toDNF` and `FirstOrder.Language.BoundedFormula.toCNF` - given a quantifier-free formula, these construct a semantically equivalent formula in disjunctive normal form and conjunctive normal form, respectively.
---
- [ ] depends on: #16888
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-logic
merge-conflict
blocked-by-other-PR
|
525/7 |
Mathlib/ModelTheory/Complexity.lean,Mathlib/ModelTheory/Equivalence.lean,Mathlib/ModelTheory/Syntax.lean |
3 |
2 |
['github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
223-1966 7 months ago |
223-1966 7 months ago |
0-613 10 minutes |
10190 |
jstoobysmith author:jstoobysmith |
feat(AlgebraicTopology): add Augmented Simplex Category |
- Added the definition of the category FinLinOrd of finite linear ordered sets.
- Added the definition of the augmented simplex category `AugmentedSimplexCategory`, and showed it is the Skeleton of FinLinOrd.
- Showed that the category of augmented simplicial objects defined as a comma category is equivalent to the category of functors from `AugmentedSimplexCategory^\op`
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
t-topology
t-category-theory
merge-conflict
WIP
label:t-algebra$ |
720/0 |
Mathlib.lean,Mathlib/AlgebraicTopology/AugmentedSimplexCategory.lean,Mathlib/AlgebraicTopology/SimplicialObject.lean,Mathlib/Order/Category/FinLinOrd.lean |
4 |
5 |
['TwoFX', 'YaelDillies', 'joelriou', 'jstoobysmith'] |
nobody |
216-12165 7 months ago |
216-12165 7 months ago |
7-63215 7 days |
12750 |
Command-Master author:Command-Master |
feat: define Gray code |
---
Define binary reflected gray code, both as a permutation of `Nat` and as a permutation of `BitVec n`, and prove some theorems about them. Additionally, remove `@[simp]` from `Nat.bit_false` and `Nat.bit_true`, as `bit0` and `bit1` are deprecated, and add some lemmas to `Bits`, `Bitwise` and `Size`.
- [ ] depends on: #12751
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
merge-conflict
awaiting-author
blocked-by-other-PR
|
226/0 |
Mathlib.lean,Mathlib/Data/Nat/Bits.lean,Mathlib/Data/Nat/Bitwise.lean,Mathlib/Data/Nat/GrayCode.lean,Mathlib/Data/Nat/Size.lean |
5 |
5 |
['Rida-Hamadani', 'alreadydone', 'github-actions', 'grunweg', 'leanprover-community-mathlib4-bot'] |
nobody |
205-24624 6 months ago |
205-24624 6 months ago |
6-8380 6 days |
9605 |
davikrehalt author:davikrehalt |
feat(Data/Finset & List): Add Lemmas for Sorting and Filtering |
This PR includes several useful lemmas to the Data/Finset and Data/List modules in Lean's mathlib:
1. `toFinset_filter` (List): Shows that filtering commutes with toFinset.
2. `toFinset_is_singleton_implies_replicate` (List): Shows a list with a singleton toFinset is a List.replicate.
3. `filter_sort_commute` (Finset): Sorting and filtering can be interchanged in Finsets.
4. `Sorted.filter` (List): A sorted list stays sorted after filtering.
5. `Sorted.append_largest` (List): Appending the largest element keeps a list sorted.
6. `sort_monotone_map` (Finset): Relates sorting of a Finset after mapping to sorting of a list.
7. `sort_insert_largest` (Finset): Sorting a Finset with an inserted largest element.
8. `sort_range` (Finset): Sorting a range in a Finset equals the corresponding range list.
9. ~~`filter_eval_true` (List): Filtering a list with a predicate always true keeps the list unchanged.~~
10. ~~`filter_eval_false` (List): Filtering with an always-false predicate gives an empty list.~~
11. ~~`pairwise_concat` (List): Iff condition for Pairwise relation in concatenated lists (similar to pairwise_join).~~
12. `list_map_toFinset` (Finset): toFinset commutes with map under injection
---
- [x] depends on: #15952
This is my first PR to mathlib, so I'm not too familiar with etiquette's and more specifically there are two proofs in the PR which uses aesop, and I am not sure if it's frowned upon. I kept the aesop in there for now as I couldn't construct very short proofs otherwise. The sort_range function proof was suggested in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Computing.20Finset.20sort.20of.20Finset.20range/near/410346731 by Ruben Van de Velde. Thanks for your time for improving this PR. |
t-data
new-contributor
merge-conflict
please-adopt
awaiting-author
|
71/0 |
Mathlib/Data/Finset/Basic.lean,Mathlib/Data/Finset/Image.lean,Mathlib/Data/Finset/Sort.lean,Mathlib/Data/List/Sort.lean |
4 |
30 |
['YaelDillies', 'davikrehalt', 'eric-wieser', 'github-actions', 'jcommelin', 'leanprover-community-mathlib4-bot', 'urkud', 'vihdzp'] |
YaelDillies assignee:YaelDillies |
194-82334 6 months ago |
221-51125 7 months ago |
12-48560 12 days |
14598 |
Command-Master author:Command-Master |
chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc. |
Add the four typeclasses `IsTopAbsorbing`, `IsBotAbsorbing`, `NoTopSum`, `NoBotSum`, as additive equivalents for `MulZeroClass` and `NoZeroDivisors`. Add instances of these for `ENNReal`, `WithTop α`, `WithBot α`, `PUnit`, `EReal`, `PartENat`, `Measure`, `Interval` and `Filter`.
Also split `Algebra/Order/AddGroupWithTop` to `Algebra/Order/Group/WithTop` and `Algebra/Order/Monoid/WithTop`
---
Previous usages of lemmas with quantified names like `WithTop.add_top` have to be changed to just `add_top`.
`add_lt_top` is `@[simp]`, in accordance with `ENNReal.add_lt_top` being `@[simp]`. This affects `WithTop.add_lt_top` which previously hadn't been `@[simp]`.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-order
t-algebra
merge-conflict
label:t-algebra$ |
264/195 |
Archive/Wiedijk100Theorems/BallotProblem.lean,Mathlib.lean,Mathlib/Algebra/Order/Group/WithTop.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Interval/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean,Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/Algebra/Order/Monoid/WithTop.lean,Mathlib/Algebra/PUnitInstances/Order.lean,Mathlib/Algebra/Polynomial/Degree/Definitions.lean,Mathlib/Algebra/Polynomial/Monic.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Analysis/Analytic/Meromorphic.lean,Mathlib/Analysis/Normed/Lp/ProdLp.lean,Mathlib/Analysis/NormedSpace/ENorm.lean,Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean,Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean,Mathlib/Data/ENNReal/Operations.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/Nat/WithBot.lean,Mathlib/Data/Real/EReal.lean,Mathlib/LinearAlgebra/Lagrange.lean,Mathlib/MeasureTheory/Covering/Differentiation.lean,Mathlib/MeasureTheory/Decomposition/Lebesgue.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean,Mathlib/MeasureTheory/Function/Jacobian.lean,Mathlib/MeasureTheory/Function/L1Space.lean,Mathlib/MeasureTheory/Function/L2Space.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Function/LpSpace.lean,Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean,Mathlib/MeasureTheory/Function/UniformIntegrable.lean,Mathlib/MeasureTheory/Integral/Bochner.lean,Mathlib/MeasureTheory/Integral/MeanInequalities.lean,Mathlib/MeasureTheory/Integral/SetIntegral.lean,Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean,Mathlib/MeasureTheory/Measure/Hausdorff.lean,Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/MeasureTheory/Measure/MeasureSpace.lean,Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean,Mathlib/MeasureTheory/Measure/Regular.lean,Mathlib/MeasureTheory/Measure/Typeclasses.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/Order/Filter/Pointwise.lean,Mathlib/Probability/Kernel/Defs.lean,Mathlib/Probability/Martingale/Convergence.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/UniqueFactorizationDomain.lean,Mathlib/Topology/EMetricSpace/Defs.lean,Mathlib/Topology/MetricSpace/Bounded.lean,Mathlib/Topology/MetricSpace/HausdorffDistance.lean,Mathlib/Topology/MetricSpace/Lipschitz.lean |
57 |
30 |
['Command-Master', 'YaelDillies', 'github-actions'] |
nobody |
188-52900 6 months ago |
188-52900 6 months ago |
7-45599 7 days |
16885 |
metinersin author:metinersin |
feat(ModelTheory/Complexity): define literals |
Defines `FirstOrder.Language.BoundedFormula.IsLiteral` and `FirstOrder.Language.BoundedFormula.simpleNot` - an auxiliary operation that takes the negation of a formula and does some simplification.
---
- [x] depends on: #16800
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-logic
merge-conflict
awaiting-author
|
148/5 |
Mathlib/ModelTheory/Complexity.lean,Mathlib/ModelTheory/Equivalence.lean,Mathlib/ModelTheory/Semantics.lean,Mathlib/ModelTheory/Syntax.lean |
4 |
20 |
['YaelDillies', 'awainverse', 'github-actions', 'mathlib4-dependent-issues-bot', 'metinersin'] |
nobody |
186-9021 6 months ago |
186-9021 6 months ago |
0-19926 5 hours |
13248 |
hcWang942 author:hcWang942 |
feat: basic concepts of auction theory |
## Description
Formalise some core concepts and results in auction theory: this includes definitions for first-price and second-price auctions, as well as several fundamental results and helping lemmas.
This is the very first PR of the project formalizing core concepts and results in auction theory.
Our group is working on more contributions on the formalization of game theory prefix.
Co-authored-by: Ma Jiajun
## Reference
Roughgarden, Tim. ***Twenty Lectures on Algorithmic Game Theory***. Cambridge University Press, 2020. [Link](https://www.cambridge.org/core/books/twenty-lectures-on-algorithmic-game-theory/A9D9427C8F43E7DAEF8C702755B6D72B)
---
- [x] Will depend on #14163 once that PR is merged. The Fintype lemmas introduced by this PR have been added in that PR and will be removed from here once that PR gets merged
## Current plan for formalization of Game Theory
The current plan for the formalizing of Game Theory include:
#### 1. Auction Theory. 🎉 _(200+ lines, this PR)_
- Essential definitions of Sealed-bid auction, First-price auction and Second-price auction.
- First-price auction has no dominant strategy.
- Second-price auction has dominant strategy. (Second-price auction is DSIC)
#### 2. Mechanism design & Myerson's Lemma. 🎉 (400+ lines, pending for modification to Mathlib Standard)
- Mechanism design
An allocation rule is implementable if there exists
- Dominant Strategy Incentive Compatible (DSIC) payment rule
- An allocation rule is monotone if for every bidder’s gain is nondecreasing w.r.t. her/his bid
- Myerson's Lemma
Implementable ⇔ Monotone
In the above case, the DSIC payment rule is unique.
#### 3. von Neumann‘s Minimax Theorem. 🎉 (800+ lines, pending for modification to Mathlib Standard)
- Equilibrium in zero sum game
- Formalization strategy: via Loomis’s theorem.
#### 4. Nash Equilibrium. 🎉 (pending for modification to Mathlib Standard)
#### 5. Brouwer fixed-point theorem. (Work in Progress)
#### 6. More Mechanism design. (Planning)
|
new-contributor
t-logic
merge-conflict
awaiting-author
|
204/0 |
Mathlib.lean,Mathlib/GameTheory/Auction/Basic.lean,docs/references.bib |
3 |
148 |
['Shreyas4991', 'YaelDillies', 'eric-wieser', 'faenuccio', 'github-actions', 'grunweg', 'hcWang942', 'tb65536', 'urkud', 'vihdzp'] |
hcWang942 assignee:hcWang942 |
181-47853 6 months ago |
unknown |
unknown |
16116 |
jjdishere author:jjdishere |
feat(Field): add theorems in Stacks Project Chapter 09FA Fields |
Add theorems in Stacks Project Chapter 09FA Fields that are not in mathlib.
Co-authored-by:
---
- [x] depends on: #16105
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
merge-conflict
WIP
label:t-algebra$ |
6/2 |
Mathlib/Algebra/Field/Defs.lean,Mathlib/Algebra/Field/Subfield.lean |
2 |
6 |
['github-actions', 'mathlib4-dependent-issues-bot', 'mergify'] |
nobody |
180-9447 5 months ago |
181-78255 6 months ago |
0-0 0 seconds |
16743 |
agjftucker author:agjftucker |
feat(Analysis/Calculus/Implicit): define HasStrictDerivAt.implicitFunOfBivariate |
In [this](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Implicit.20function.20theorem.20in.20familiar.20form) Zulip thread @Komyyy proved the "familiar" implicit function theorem. Then I wrote a proposal for a Mathlib PR. (Updated) it went:
1. `noncomputable def implicitFunOfBivariate {f : X × Y → Z} {p₀ : X × Y}
{fx : X →L[𝕜] Z} {fy : Y ≃L[𝕜] Z} (hf₀ : HasStrictFDerivAt f (fx.coprod fy) p₀) :
X → Y := ...`
2. `noncomputable def implicitFunOfBivariate'
{f : X → Y → Z} {x₀ : X} {y₀ : Y} {fx : X →L[𝕜] Z} {fy : Y ≃L[𝕜] Z}
(hfx : ContDiffAt 𝕜 1 (f · y₀) x₀) (hfy : ContDiffAt 𝕜 1 (f x₀ ·) y₀)
(hfx₀ : fderiv 𝕜 (f · y₀) x₀ = fx) (hfy₀ : fderiv 𝕜 (f x₀ ·) y₀ = fy) :
X → Y := ...`
3. `theorem image_eq_iff_implicitFunOfBivariate {f : X × Y → Z} {p₀ : X × Y}
{fx : X →L[𝕜] Z} {fy : Y ≃L[𝕜] Z} (hf₀ : HasStrictFDerivAt f (fx.coprod fy) p₀) :
∀ᶠ p in 𝓝 p₀, f p = f p₀ ↔ hf₀.implicitFunOfBivariate p.1 = p.2 := ...`
4. `theorem implicitFunOfBivariate_hasStrictFDerivAt {f : X × Y → Z} {x₀ : X} {y₀ : Y}
{fx : X →L[𝕜] Z} {fy : Y ≃L[𝕜] Z} (hf₀ : HasStrictFDerivAt f (fx.coprod fy) (x₀, y₀)) :
HasStrictFDerivAt hf₀.implicitFunOfBivariate (-fy.symm ∘L fx) x₀ := ...`
5. something on the second derivative (or higher).
Although my proposal elicited no response, I am making this micro-PR to address points 1, 3 and 4 since some limited enthusiasm had been shown earlier in that thread (admittedly for another proposal made by another person). I am testing the waters; if this PR gets anywhere I may continue to work on points 2 and 5.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-analysis
merge-conflict
awaiting-author
|
132/8 |
Mathlib/Analysis/Calculus/Implicit.lean,Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean,Mathlib/LinearAlgebra/Span.lean,Mathlib/Order/Filter/Prod.lean |
4 |
4 |
['github-actions', 'sgouezel'] |
sgouezel assignee:sgouezel |
169-38495 5 months ago |
169-38495 5 months ago |
63-71154 63 days |
18646 |
jxjwan author:jxjwan |
feat(RingTheory): isotypic components |
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
merge-conflict
label:t-algebra$ |
308/0 |
Mathlib/Order/CompactlyGenerated/Basic.lean,Mathlib/RingTheory/Isotypic.lean,Mathlib/RingTheory/SimpleModule.lean |
3 |
1 |
['github-actions'] |
nobody |
169-31025 5 months ago |
169-31025 5 months ago |
20-16585 20 days |
19299 |
javierlcontreras author:javierlcontreras |
feat(Algebra/CategoryTheory): Add CommAlgebraCat |
---
- [x] depends on: #19065
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
merge-conflict
WIP
label:t-algebra$ |
26/1 |
Mathlib/Algebra/Algebra/Defs.lean,Mathlib/Algebra/Category/AlgebraCat/Basic.lean |
2 |
4 |
['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot'] |
nobody |
169-17030 5 months ago |
169-33202 5 months ago |
0-2116 35 minutes |
19526 |
metakunt author:metakunt |
feat:closure properties of numbers that are introspective to polynomials |
Prove Part 1 of Claim 1.(i) of Theorem 6.1 in https://www3.nd.edu/~andyp/notes/AKS.pdf.
----
Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Aks.20primality.20Theorem.206.2E1.20Claim.20.28i.29.20proven |
new-contributor
t-number-theory
merge-conflict
awaiting-author
|
57/0 |
Mathlib.lean,Mathlib/NumberTheory/AKSPrimality.lean |
2 |
10 |
['Ruben-VandeVelde', 'github-actions', 'jcommelin', 'kim-em', 'metakunt'] |
nobody |
163-32358 5 months ago |
163-32358 5 months ago |
0-16072 4 hours |
19125 |
yhtq author:yhtq |
feat: add theorems to transfer `IsGalois` between pairs of fraction rings |
feat: add theorems to transfer `IsGalois` between pairs of fraction rings.
- [x] depends on: #18404
- [x] depends on: #19124
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
merge-conflict
label:t-algebra$ |
121/0 |
Mathlib.lean,Mathlib/FieldTheory/Galois/IsFractionRing.lean,Mathlib/RingTheory/Localization/FractionRing.lean |
3 |
3 |
['github-actions', 'mathlib4-dependent-issues-bot', 'tb65536'] |
nobody |
151-70270 5 months ago |
158-19293 5 months ago |
0-4534 1 hour |
11156 |
smorel394 author:smorel394 |
feat(LinearAlgebra/{TensorProductBasis,Dual}): basis and dual of `PiTensorProduct` |
Construct a basis of a `PiTensorProduct` of modules given bases of the modules, and relationship between the dual of a `PiTensorProduct` and the `PiTensorProduct` of the duals.
Main results:
* `Basis.piTensorProduct` (in `LinearAlgebra/TensorProductBasis.lean`): Let `ι` be a `Fintype` and `M` be a family of modules indexed by `ι`. If `b i : κ i → M i` is a basis for every `i` in `ι`, then `fun (p : Π i, κ i) ↦ ⨂ₜ[R] i, b i (p i)` is a basis of `⨂[R] i, M i`.
* `PiTensorProduct.dualDistrib` (in `LinearAlgebra/Dual.lean`): The canonical linear map from `⨂[R] i, Dual R (M i)` to `Dual R (⨂[R] i, M i)`, sending `⨂ₜ[R] i, f i` to the composition of `PiTensorProduct.map f` with the linear equivalence `⨂[R] i, R →ₗ R` given by multiplication.
* `PiTensorProduct.dualDistribEquiv` (also in `LinearAlgebra/Dual.lean`): A linear equivalence between `⨂[R] i, Dual R (M i)` and `Dual R (⨂[R] i, M i)` when all `M i` are finite free modules. If `f : (i : ι) → Dual R (M i)`, then this equivalence sends `⨂ₜ[R] i, f i` to the composition of `PiTensorProduct.map f` with the natural isomorphism `⨂[R] i, R ≃ R` given by multiplication.
- [ ] depends on: #11155 (currently used as the base branch; do not merge without switching it back to `master`!)
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-algebra
merge-conflict
please-adopt
blocked-by-other-PR
label:t-algebra$ |
166/2 |
Mathlib/LinearAlgebra/DirectSum/Finsupp.lean,Mathlib/LinearAlgebra/Dual.lean,Mathlib/LinearAlgebra/TensorProduct/Basis.lean |
3 |
4 |
['eric-wieser', 'github-actions', 'leanprover-community-mathlib4-bot'] |
nobody |
134-22701 4 months ago |
179-38329 5 months ago |
0-0 0 seconds |
17739 |
Aaron1011 author:Aaron1011 |
feat(Topology/Order/DenselyOrdered): prove Not (IsOpen) for intervals |
Prove that Iic/Ici/Ioc/Ico/Icc intervals are not open in densely ordered topologies with no min/max element
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
merge-conflict
awaiting-author
|
27/0 |
Mathlib/Topology/Order/DenselyOrdered.lean |
1 |
8 |
['github-actions', 'vihdzp'] |
nobody |
118-5882 3 months ago |
118-5882 3 months ago |
0-4704 1 hour |
15720 |
znssong author:znssong |
feat(SimpleGraph): The Bondy-Chvátal theorem |
The proof of the Bondy-Chvátal theorem, with Dirac's theorem and Ore's theorem as its corollary.
- [x] depends on: #15536
- [ ] depends on: #15711
- [ ] depends on: #15578 |
new-contributor
t-combinatorics
merge-conflict
blocked-by-other-PR
|
903/3 |
Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/BondyChvatal.lean,Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean,Mathlib/Combinatorics/SimpleGraph/Path.lean,Mathlib/Combinatorics/SimpleGraph/Walk.lean,Mathlib/Dynamics/FixedPoints/Basic.lean,Mathlib/Dynamics/FixedPoints/Increasing.lean |
8 |
3 |
['github-actions', 'grunweg', 'leanprover-community-mathlib4-bot'] |
YaelDillies assignee:YaelDillies |
117-24968 3 months ago |
117-24968 3 months ago |
0-1791 29 minutes |
15711 |
znssong author:znssong |
feat(Combinatorics/SimpleGraph): Some lemmas about walk, cycle and Hamiltonian cycle |
---
These lemmas are separated from the `meow-sister/BondyChvatal` branch and will be needed for the proof of the Bondy-Chvátal theorem.
- [x] depends on: #15536
- [x] depends on: #16294 |
new-contributor
t-combinatorics
merge-conflict
awaiting-author
|
407/3 |
Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean,Mathlib/Combinatorics/SimpleGraph/Path.lean,Mathlib/Combinatorics/SimpleGraph/Walk.lean |
4 |
22 |
['Rida-Hamadani', 'YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'znssong'] |
nobody |
117-24968 3 months ago |
117-24968 3 months ago |
9-13962 9 days |
18629 |
tomaz1502 author:tomaz1502 |
feat(Computability.Timed): Formalization of runtime complexity of List.merge |
This PR adds the formalization of the runtime complexity of the merge function, defined in `Data/List/Sort`.
Requires: https://github.com/leanprover-community/mathlib4/pull/15450
References:
- Previous PR on mathlib3: https://github.com/leanprover-community/mathlib3/pull/14494/
- First discussion on Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/BSc.20Final.20Project/near/220647062
- Second disussion on Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Formalization.20of.20Runtime.20Complexity.20of.20Sorting.20Algorithms/near/284184450
---
[](https://gitpod.io/from-referrer/)
|
t-computability
new-contributor
merge-conflict
awaiting-author
|
186/0 |
Mathlib.lean,Mathlib/Computability/Timed/InsertionSort.lean,Mathlib/Computability/Timed/Merge.lean |
3 |
2 |
['github-actions', 'trivial1711'] |
nobody |
116-77287 3 months ago |
116-77287 3 months ago |
33-11262 33 days |
19291 |
PieterCuijpers author:PieterCuijpers |
feat(Algebra/Order/Hom): add quantale homomorphism |
Definition of quantale homomorphisms as functions that are both semigroup homomorphisms and complete lattice homomorphisms.
---
- [x] depends on: #19810
- [x] depends on: #19811
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
merge-conflict
awaiting-author
label:t-algebra$ |
209/0 |
Mathlib.lean,Mathlib/Algebra/Order/Hom/Quantale.lean,scripts/noshake.json |
3 |
29 |
['PieterCuijpers', 'YaelDillies', 'github-actions', 'kim-em', 'mathlib4-dependent-issues-bot'] |
nobody |
112-12546 3 months ago |
112-12547 3 months ago |
36-2255 36 days |
20372 |
jvlmdr author:jvlmdr |
feat(MeasureTheory/Function): Add ContinuousLinearMap.bilinearCompLp(L) |
Introduce ContinuousLinearMap.bilinearCompLp and bilinearCompLpL.
Generalize eLpNorm_le_eLpNorm_mul_eLpNorm theorems to include constant C in bound condition.
---
Expect this may be useful for defining tempered distributions from functions in `L^p`.
The definitions more or less follow `ContinuousLinearMap.compLp...`. Names are loosely analogous to `ContinuousLinearMap.bilinearComp` and `SchwartzMap.bilinLeftCLM`.
Note: I preferred the spelling `hpqr : p⁻¹ + q⁻¹ = r⁻¹` with `f` in `L^p` and `g` in `L^q` to `hpqr : 1 / p = 1 / q + 1 / r`. It's easier to obtain from `ENNReal.IsConjExponent` too.
A few questions:
- [ ] I defined `bilinear{Left,Right}LpL` in addition to `bilinearCompLpL` because `LinearMap.mkContinuous₂` is marked as `noncomputable` and `LinearMap.mkContinuous` is not. Is this worth the extra definitions? (Note: This is not visible in the source due to `noncomputable section`.)
- [ ] Should I use `C : ℝ` instead of `C : NNReal` for `eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm'`?
- [ ] Is it going to be painful to have `[Fact (1 ≤ p)] [Fact (1 ≤ q)] [Fact (1 ≤ r)]`? I don't think there's a way to avoid it though. Maybe providing specialized versions for `p.IsConjExponent q` with `L^1`?
Naming:
- [ ] Is it satisfactory to add a `'` to the `eLpNorm_le_eLpNorm_mul_eLpNorm ` definitions in `CompareExp.lean` where `≤ ‖f x‖ * ‖g x‖` has been replaced with `≤ C * ‖f x‖ * ‖g x‖`? These could replace the existing theorems, although I don't want to break backwards compatibility. There are 5 instances: `eLpNorm_le_eLpNorm_top_mul_eLpNorm'`, `eLpNorm_le_eLpNorm_mul_eLpNorm_top'`, `eLpNorm'_le_eLpNorm'_mul_eLpNorm''`, `eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm'`, `eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm'` (I'm not sure why the existing theorem `eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm` has an internal `'`)
- [ ] Is `bilinearLeftLpL` a suitable name? Other options: `bilinearCompLpLeftL`, `bilinearCompLeftLpL`, `bilinLeftLpL` (analogous to `SchwartzMap.bilinLeftCLM`)
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-measure-probability
merge-conflict
|
203/40 |
Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSpace.lean |
2 |
1 |
['github-actions'] |
nobody |
105-29894 3 months ago |
105-29894 3 months ago |
27-43617 27 days |
17176 |
arulandu author:arulandu |
feat: integrals and integrability with .re |
Lemmas for swapping order of .re and integration/integrability.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-measure-probability
merge-conflict
awaiting-author
|
49/0 |
Mathlib/MeasureTheory/Function/L1Space.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral.lean,Mathlib/MeasureTheory/Integral/SetIntegral.lean |
4 |
30 |
['EtienneC30', 'arulandu', 'github-actions', 'loefflerd'] |
nobody |
104-4327 3 months ago |
104-4327 3 months ago |
9-73631 9 days |
14799 |
luigi-massacci author:luigi-massacci |
feat(Analysis/MeanInequalities): Weighted QM-AM inequality |
The inequality between the quadratic and arithmetic mean as a consequence of Jensen's inequality. Weighted version for positive real valued functions from a `Finset`. Fix notation for sums, switching to `∈` in place of `in`.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-analysis
easy
merge-conflict
awaiting-author
|
26/3 |
Mathlib/Analysis/MeanInequalities.lean |
1 |
8 |
['YaelDillies', 'acmepjz', 'github-actions', 'luigi-massacci', 'vihdzp'] |
nobody |
102-83898 3 months ago |
102-83898 3 months ago |
0-38862 10 hours |
20248 |
peabrainiac author:peabrainiac |
feat(Topology/Compactness): first-countable locally path-connected spaces are delta-generated |
Shows that all first-countable locally path-connected spaces are delta-generated (so in particular all normed spaces and convex subsets thereof are), and that delta-generated spaces are equivalently generated by the unit interval or standard simplices.
---
- [ ] depends on: #21616
In principle, this should be close to all that's required to show that all simplicial complexes and CW-complexes are delta-generated; I just haven't done it yet because I'm not sure which file to best do it in.
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-topology
merge-conflict
awaiting-author
blocked-by-other-PR
|
1189/813 |
Mathlib.lean,Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/Topology/Algebra/Module/LocallyConvex.lean,Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean,Mathlib/Topology/Connected/LocPathConnected.lean,Mathlib/Topology/Connected/PathConnected.lean,Mathlib/Topology/ContinuousOn.lean,Mathlib/Topology/Homotopy/HSpaces.lean,Mathlib/Topology/Path.lean |
9 |
22 |
['YaelDillies', 'github-actions', 'kbuzzard', 'mathlib4-dependent-issues-bot', 'peabrainiac'] |
nobody |
92-73604 3 months ago |
92-73604 3 months ago |
39-21495 39 days |
20334 |
miguelmarco author:miguelmarco |
feat: allow polyrith to use a local Singular/Sage install |
Try to call a local install of Singular (either standalone or inside Sage) to find the witness for polyrith before trying to call the online sage cell server.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
merge-conflict
awaiting-author
|
171/48 |
Mathlib/Tactic/Polyrith.lean,scripts/polyrith_sage.py |
2 |
13 |
['eric-wieser', 'github-actions', 'hanwenzhu', 'kim-em', 'miguelmarco'] |
nobody |
88-38281 2 months ago |
88-38281 2 months ago |
27-65384 27 days |
19943 |
AlexLoitzl author:AlexLoitzl |
feat(Computability): Add Chomsky Normal Form Grammar and translation |
- Define Chomsky normal form grammars
- Add language-preserving translation between context-free grammars and Chomsky normal form grammars
Co-authored-by: Martin Dvorak martin.dvorak@matfyz.cz
---
[](https://gitpod.io/from-referrer/)
|
t-computability
new-contributor
merge-conflict
awaiting-author
|
3151/0 |
Mathlib.lean,Mathlib/Computability/ChomskyNormalForm/Basic.lean,Mathlib/Computability/ChomskyNormalForm/EmptyElimination.lean,Mathlib/Computability/ChomskyNormalForm/LengthRestriction.lean,Mathlib/Computability/ChomskyNormalForm/TerminalRestriction.lean,Mathlib/Computability/ChomskyNormalForm/Translation.lean,Mathlib/Computability/ChomskyNormalForm/UnitElimination.lean,Mathlib/Computability/ContextFreeGrammar.lean |
8 |
59 |
['AlexLoitzl', 'YaelDillies', 'github-actions', 'kim-em', 'madvorak'] |
nobody |
88-21303 2 months ago |
88-21303 2 months ago |
37-29014 37 days |
10541 |
Louddy author:Louddy |
feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra |
# Skew Monoid algebras
This file presents a skewed version of `Mathlib.Algebra.MonoidAlgebra.Basic`.
## Definition
We define `SkewMonoidAlgebra k G := G →₀ k` attached with a skewed convolution product.
Here, the product of two elements `f g : SkewMonoidAlgebra k G` is the finitely supported
function whose value at `a` is the sum of `f x * (x • g y)` over all pairs `x, y`
such that `x * y = a`.
This will be used in a later PR to define skew polynomial rings.
Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)>
---
- [x] depends on: #15878
- [x] depends on: #19084
- [ ] depends on: #22078
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
merge-conflict
blocked-by-other-PR
WIP
label:t-algebra$ |
1624/0 |
Mathlib.lean,Mathlib/Algebra/Group/InjSurj.lean,Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean,Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean |
4 |
105 |
['AntoineChambert-Loir', 'Louddy', 'YaelDillies', 'eric-wieser', 'fpvandoorn', 'github-actions', 'mariainesdff', 'mathlib4-dependent-issues-bot', 'mattrobball'] |
AntoineChambert-Loir assignee:AntoineChambert-Loir |
83-24929 2 months ago |
83-24930 2 months ago |
179-12934 179 days |
21269 |
CharredLee author:CharredLee |
(WIP) feat (CategoryTheory/Topos): Add topos theory content |
This code contains basic definitions and results in topos theory, including the definition of a subobject classifier, power objects, and topoi. It is proved that every topos has exponential objects, i.e. "internal homs". The mathematical content follows chapter IV sections 1-2 of Mac Lane and Moerdijk's text "Sheaves in Geometry and Logic".
---
- [x] depends on: #21281
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
merge-conflict
awaiting-author
WIP
|
1269/0 |
Mathlib.lean,Mathlib/CategoryTheory/Topos/Basic.lean,Mathlib/CategoryTheory/Topos/Classifier.lean,Mathlib/CategoryTheory/Topos/Exponentials.lean,Mathlib/CategoryTheory/Topos/Power.lean |
5 |
10 |
['CharredLee', 'gio256', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot'] |
nobody |
77-73975 2 months ago |
77-73975 2 months ago |
0-13879 3 hours |
22245 |
Champitoad author:Champitoad |
feat(CategoryTheory/Subobject): add formalization of subobject classifier |
This introduces a file `Classifier.lean` defining the notion `Classifier C` of subobject classifier in any category `C` with a terminal object, following Section I.3 of "Sheaves in Geometry and Logic" [MM92]. This is related to but independent from #21281, because our definition associates a characteristic map to every _subobject_ rather than every _monomorphism_. Adopting this "extensional" rather than "intensional" definition allows us to formalize the proof of Proposition 1 in [MM92, Section I.3] (`hasClassifier_isRepresentable_iff`), that `C` has a subobject classifier if and only if the subobjects presheaf `sub C` is representable.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
merge-conflict
awaiting-author
|
5219/2536 |
Cache/Hashing.lean,Cache/IO.lean,Cache/Lean.lean,Mathlib.lean,Mathlib/Algebra/Algebra/Defs.lean,Mathlib/Algebra/Category/AlgebraCat/Limits.lean,Mathlib/Algebra/Category/BoolRing.lean,Mathlib/Algebra/Category/FGModuleCat/Basic.lean,Mathlib/Algebra/Category/Grp/AB.lean,Mathlib/Algebra/Category/Grp/EpiMono.lean,Mathlib/Algebra/Category/HopfAlgebraCat/Monoidal.lean,Mathlib/Algebra/Category/ModuleCat/Abelian.lean,Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean,Mathlib/Algebra/Category/ModuleCat/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Biproducts.lean,Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean,Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean,Mathlib/Algebra/Category/ModuleCat/EpiMono.lean,Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean,Mathlib/Algebra/Category/ModuleCat/Kernels.lean,Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean,Mathlib/Algebra/Category/ModuleCat/Subobject.lean,Mathlib/Algebra/Category/MonCat/FilteredColimits.lean,Mathlib/Algebra/Category/Ring/Colimits.lean,Mathlib/Algebra/Category/Ring/Limits.lean,Mathlib/Algebra/Group/Commute/Units.lean,Mathlib/Algebra/Group/Pointwise/Set/Card.lean,Mathlib/Algebra/Homology/ComplexShape.lean,Mathlib/Algebra/Homology/Double.lean,Mathlib/Algebra/Homology/HasNoLoop.lean,Mathlib/Algebra/Homology/Homotopy.lean,Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Algebra/Polynomial/Lifts.lean,Mathlib/Algebra/Polynomial/Sequence.lean,Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Complex/AbelLimit.lean,Mathlib/Analysis/Complex/AbsMax.lean,Mathlib/Analysis/Complex/Angle.lean,Mathlib/Analysis/Complex/Arg.lean,Mathlib/Analysis/Complex/Basic.lean,Mathlib/Analysis/Complex/CauchyIntegral.lean,Mathlib/Analysis/Complex/Circle.lean,Mathlib/Analysis/Complex/Hadamard.lean,Mathlib/Analysis/Complex/Isometry.lean,Mathlib/Analysis/Complex/Liouville.lean,Mathlib/Analysis/Complex/LocallyUniformLimit.lean,Mathlib/Analysis/Complex/OpenMapping.lean,Mathlib/Analysis/Complex/Periodic.lean,Mathlib/Analysis/Complex/PhragmenLindelof.lean,Mathlib/Analysis/Complex/Positivity.lean,Mathlib/Analysis/Complex/Schwarz.lean,Mathlib/Analysis/Complex/UnitDisc/Basic.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Exp.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean,Mathlib/Analysis/Fourier/AddCircle.lean,Mathlib/Analysis/Fourier/AddCircleMulti.lean,Mathlib/Analysis/Fourier/FourierTransformDeriv.lean,Mathlib/Analysis/Fourier/Inversion.lean,Mathlib/Analysis/Fourier/PoissonSummation.lean,Mathlib/Analysis/InnerProductSpace/TwoDim.lean,Mathlib/Analysis/MellinTransform.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/Normed/Lp/WithLp.lean,Mathlib/Analysis/PSeries.lean,Mathlib/Analysis/PSeriesComplex.lean,Mathlib/Analysis/SpecialFunctions/CompareExp.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Complex/Log.lean,Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean,Mathlib/Analysis/SpecialFunctions/Exp.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean,Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean,Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean,Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean,Mathlib/Analysis/SpecialFunctions/Integrals.lean,Mathlib/Analysis/SpecialFunctions/Log/Summable.lean,Mathlib/Analysis/SpecialFunctions/PolarCoord.lean,Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean,Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean,Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Pow/Real.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean,Mathlib/CategoryTheory/Abelian/FreydMitchell.lean,Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean,Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Coseparator.lean |
205 |
10 |
['Champitoad', 'github-actions', 'joelriou'] |
nobody |
76-83790 2 months ago |
76-85063 2 months ago |
0-38059 10 hours |
14313 |
grhkm21 author:grhkm21 |
feat(RepresentationTheory/FdRep): FdRep is a full subcategory of Rep |
```
/-- Equivalence between `FDRep` and the full subcategory of finite dimensional `Rep`. -/
def equivFiniteDimensional :
FDRep k G ≌ FullSubcategory (fun V : Rep k G ↦ FiniteDimensional k V)
``` |
new-contributor
t-algebra
t-category-theory
merge-conflict
label:t-algebra$ |
47/8 |
Mathlib/RepresentationTheory/FDRep.lean |
1 |
19 |
['github-actions', 'grhkm21', 'joelriou', 'kim-em', 'mathlib-bors'] |
nobody |
74-29901 2 months ago |
74-29901 2 months ago |
125-12755 125 days |
18626 |
hannahfechtner author:hannahfechtner |
feat : define Artin braid groups |
Define the Artin braid group on infinitely many strands. Includes a toGroup function which defines a function out of the braid group to any other group (given a function which satisfies the braid relations)
(more to come in this file; next up: Artin braid groups on finitely many strands)
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
merge-conflict
awaiting-author
label:t-algebra$ |
91/0 |
Mathlib.lean,Mathlib/GroupTheory/SpecificGroups/BraidGroup/Basic.lean |
2 |
22 |
['github-actions', 'hannahfechtner', 'jcommelin', 'joelriou'] |
nobody |
73-14212 2 months ago |
73-14212 2 months ago |
15-40648 15 days |
14060 |
YnirPaz author:YnirPaz |
feat(SetTheory/Ordinal/Clubs): define club sets and prove basic properties |
Create a file where club sets are defined and their basic properties are proven.
I also created a new recursion principle for ordinals, bounded recursion.
---
- [ ] depends on: #19189
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-logic
merge-conflict
blocked-by-other-PR
|
315/3 |
Mathlib.lean,Mathlib/Order/SuccPred/Limit.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Club.lean,Mathlib/SetTheory/Ordinal/Topology.lean |
6 |
93 |
['YaelDillies', 'YnirPaz', 'alreadydone', 'dupuisf', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp', 'zeramorphic'] |
nobody |
70-58725 2 months ago |
70-58725 2 months ago |
92-44198 92 days |
21959 |
BGuillemet author:BGuillemet |
feat(Topology/ContinuousMap): Stone-Weierstrass theorem for MvPolynomial |
Add the subalgebra of multivariate polynomials and prove it separates points, on the same model as `ContinuousMap/Polynomial.lean`.
Prove the Stone-Weierstrass theorem and some variations for multivariate polynomials.
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
merge-conflict
|
285/1 |
Mathlib.lean,Mathlib/Topology/ContinuousMap/MvPolynomial.lean,Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean |
3 |
1 |
['github-actions'] |
nobody |
69-15915 2 months ago |
69-15915 2 months ago |
16-76141 16 days |
15578 |
znssong author:znssong |
feat(Function): Fixed points of function `f` with `f(x) >= x` |
We added some lemmas of fixed points of function `f` with `f(x) >= x`, where `f : α → α` is a function on a finite type `α`. This will be needed in proof of Bondy-Chvátal theorem.
---
See also branch `meow-sister/BondyChvatal`.
[](https://gitpod.io/from-referrer/) |
new-contributor
t-analysis
merge-conflict
awaiting-author
|
82/0 |
Mathlib.lean,Mathlib/Dynamics/FixedPoints/Basic.lean,Mathlib/Dynamics/FixedPoints/Increasing.lean |
3 |
32 |
['Ruben-VandeVelde', 'YaelDillies', 'github-actions', 'urkud', 'vihdzp', 'znssong'] |
nobody |
61-11741 2 months ago |
61-11741 2 months ago |
29-48368 29 days |
21018 |
markimunro author:markimunro |
feat(Data/Matrix): add file with key definitions and theorems about elementary row operations |
Prove that each elementary row operation is equivalent to a multiplication by an elementary matrix, has another row operation which inverts it, and that each elementary matrix has a left inverse.
This is a very large PR and I understand it will take time. This is my first one and will likely have issues but I will be ready to answer questions/fix them as soon as possible.
Co-authored-by: Christopher Lynch
---
[](https://gitpod.io/from-referrer/)
|
t-data
new-contributor
merge-conflict
awaiting-author
enhancement
|
1230/0 |
Mathlib.lean,Mathlib/Data/Matrix/ElementaryRowOperations.lean,Mathlib/Data/Matrix/GaussianElimination.lean,Mathlib/Data/Matrix/GaussianEliminationOld,Mathlib/Data/Matrix/oldnames,et --hard 18533caba32,lean-toolchain |
7 |
n/a |
['chrisflav', 'eric-wieser', 'github-actions', 'j-loreaux', 'markimunro'] |
nobody |
42-47140 1 month ago |
unknown |
unknown |
11768 |
JovanGerb author:JovanGerb |
feat: Interactive Library Rewrite |
This PR defines the `rw??` library rewrite tactic that uses my `RefinedDiscrTree`.
This is a point&click tactic, letting the user click on subexpressions in the main goal. The results are sorted by relevance, and are separated into sections based on the matched pattern. It comes with a filter button that allows you to switch between the (default) filtered view, with removed duplicate lemmas and not showing lemma names, and the complete view. There is also a section for definitionally unfolding the selected expression - these rewrites do not correspond to a library lemma.
---
- [ ] depends on: #11968
- [x] depends on: #12016
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-meta
merge-conflict
blocked-by-other-PR
|
2788/1253 |
Mathlib.lean,Mathlib/Lean/GoalsLocation.lean,Mathlib/Lean/Meta/RefinedDiscrTree.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean,Mathlib/Lean/Meta/RefinedDiscrTree/Pi.lean,Mathlib/Tactic.lean,Mathlib/Tactic/FunProp.lean,Mathlib/Tactic/FunProp/Elab.lean,Mathlib/Tactic/FunProp/StateList.lean,Mathlib/Tactic/FunProp/Theorems.lean,Mathlib/Tactic/FunProp/Types.lean,Mathlib/Tactic/Widget/InteractiveUnfold.lean,Mathlib/Tactic/Widget/LibraryRewrite.lean,Mathlib/Topology/Defs/Basic.lean,MathlibTest/LibraryRewrite.lean,MathlibTest/RefinedDiscrTree.lean,scripts/noshake.json |
20 |
n/a |
['JovanGerb', 'eric-wieser', 'fpvandoorn', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot'] |
nobody |
41-28174 1 month ago |
unknown |
unknown |
15212 |
victorliu5296 author:victorliu5296 |
feat: Add fundamental theorem of calculus-2 for Banach spaces |
add the Mean Value Theorem for Banach spaces to the library and include reference for the theorem statement
This theorem states that if `f : X → Y` is differentiable along the line segment from `a` to `b`, then the change in `f` equals the integral of its derivative along this path. This extends the mean value theorem to Banach spaces. This can be used for the eventual proof of the Newton-Kantorovich theorem with 1 constant contained inside the added reference.
Here is the discussion on Zulipchat: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Contributing.20FTC-2.20for.20Banach.20spaces |
new-contributor
t-measure-probability
t-analysis
merge-conflict
awaiting-author
|
60/1 |
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean |
1 |
3 |
['github-actions', 'hrmacbeth', 'victorliu5296'] |
nobody |
37-42129 1 month ago |
37-42129 1 month ago |
51-85104 51 days |
22701 |
ctchou author:ctchou |
feat(Combinatorics): the Katona circle method |
This file formalizes the Katona circle method.
From PlainCombi (LeanCamCombi): https://github.com/YaelDillies/LeanCamCombi/blob/master/LeanCamCombi/PlainCombi/KatonaCircle.lean
Co-authored-by: Yaël Dillies
|
new-contributor
t-combinatorics
merge-conflict
|
121/0 |
Mathlib.lean,Mathlib/Combinatorics/KatonaCircle.lean |
2 |
1 |
['github-actions'] |
nobody |
36-78084 1 month ago |
36-78084 1 month ago |
30-8337 30 days |
21488 |
imbrem author:imbrem |
feat(CategoryTheory/Monoidal): premonoidal categories |
Add support for premonoidal categories
---
Still want to add support for:
- Premonoidal braided/symmetric categories
- The monoidal coherence theorem, which I've already ported in my `discretion` library
- The `coherence` tactic, which should work fine for premonoidal categories too
but wanted to get this in front of reviewers ASAP to make sure my general approach was alright
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-category-theory
merge-conflict
|
900/361 |
Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean,Mathlib/CategoryTheory/Bicategory/End.lean,Mathlib/CategoryTheory/GradedObject/Monoidal.lean,Mathlib/CategoryTheory/Localization/Monoidal.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Center.lean,Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/CategoryTheory/Monoidal/End.lean,Mathlib/CategoryTheory/Monoidal/Free/Basic.lean,Mathlib/CategoryTheory/Monoidal/Functor.lean,Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/CategoryTheory/Monoidal/Opposite.lean,Mathlib/CategoryTheory/Monoidal/Transport.lean,Mathlib/Tactic/CategoryTheory/Monoidal/Datatypes.lean,Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean,Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean,Mathlib/Tactic/CategoryTheory/MonoidalComp.lean,MathlibTest/StringDiagram.lean |
21 |
9 |
['YaelDillies', 'github-actions', 'grunweg', 'imbrem', 'kim-em', 'leanprover-community-bot-assistant'] |
nobody |
34-24317 1 month ago |
34-24318 1 month ago |
58-20339 58 days |
20873 |
vbeffara author:vbeffara |
feat(Topology/Covering): path lifting and homotopy lifting |
This proves the existence and uniqueness of path and homotopy lifts through covering maps.
---
I tried to separate as much of the proof as possible into separate PRs (which are already in Mathlib now), but the proof here relies on a monolithic construction of an explicit lift along a well-chosen subdivision, in `partial_lift`, with associated definitions. Only one standalone lean file added.
An older WIP PR #10084 by Junyan Xu @alreadydone proves similar results using a very similar construction for path lifting, with a different argument to obtain continuity for homotopy lifting.
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-topology
merge-conflict
awaiting-author
|
281/1 |
Mathlib.lean,Mathlib/Topology/Covering/Basic.lean,Mathlib/Topology/Covering/Lift.lean |
3 |
9 |
['alreadydone', 'github-actions', 'grunweg', 'vbeffara'] |
nobody |
33-27045 1 month ago |
33-27045 1 month ago |
55-53553 55 days |
20313 |
thefundamentaltheor3m author:thefundamentaltheor3m |
feat(Data/Complex/Exponential): prove some useful results about the complex exponential. |
This PR proves two basic results about the complex exponential:
* `abs_exp_mul_I (x : ℂ) : abs (Complex.exp (I * x)) = Real.exp (-x.im)`
* `one_sub_rexp_re_le_abs_one_sub_cexp (x : ℂ) : 1 - Real.exp x.re ≤ Complex.abs (1 - Complex.exp x)`
Both results were proved as part of the sphere packing project. There's a chance they're too specific for mathlib, but I thought they were worth PRing anyway. Would it also be a good idea to tag `abs_exp_mul_I` with `simp`? Feedback/suggestions welcome.
Note: `one_sub_rexp_re_le_abs_one_sub_cexp` was proved by Bhavik Mehta @b-mehta
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-analysis
merge-conflict
|
167/141 |
Mathlib.lean,Mathlib/Analysis/Complex/Basic.lean,Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean,Mathlib/Data/Complex/Exponential/Defs.lean,Mathlib/Data/Complex/Exponential/Lemmas.lean,Mathlib/Data/Complex/ExponentialBounds.lean,Mathlib/Tactic/FunProp.lean,MathlibTest/Recall.lean,MathlibTest/positivity.lean |
10 |
12 |
['b-mehta', 'github-actions', 'kim-em', 'thefundamentaltheor3m', 'trivial1711'] |
nobody |
25-84643 25 days ago |
25-84643 25 days ago |
25-60481 25 days |
20730 |
kuotsanhsu author:kuotsanhsu |
feat(LinearAlgebra/Matrix/SchurTriangulation): prove Schur decomposition/triangulation |
`Matrix.schur_triangulation` shows that a matrix over an algebraically closed field is unitarily similar to an upper triangular matrix
---
[](https://gitpod.io/from-referrer/)
|
new-contributor
t-algebra
merge-conflict
awaiting-author
label:t-algebra$ |
317/2 |
Mathlib.lean,Mathlib/LinearAlgebra/Matrix/Block.lean,Mathlib/LinearAlgebra/Matrix/SchurTriangulation.lean,Mathlib/Logic/Equiv/Basic.lean |
4 |
14 |
['eric-wieser', 'github-actions', 'kim-em', 'kuotsanhsu'] |
nobody |
25-80775 25 days ago |
25-80775 25 days ago |
13-60072 13 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-77893 7 days ago |
7-77898 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 |
19633 |
grunweg author:grunweg |
fix(CI): build the Archive and Counterexamples with --wfail also |
This appears to be an oversight --- which has no consequences right now (the check for noisy output later would catch any warnings), but fixing it doesn't hurt either.
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/No.20.60--wfail.60.20when.20building.20archive).
---
[](https://gitpod.io/from-referrer/)
|
CI
awaiting-CI
easy
delegated
|
20/8 |
.github/build.in.yml,.github/workflows/bors.yml,.github/workflows/build.yml,.github/workflows/build_fork.yml |
4 |
5 |
['adomani', 'github-actions', 'grunweg', 'kim-em', 'mathlib-bors'] |
nobody |
154-65684 5 months ago |
154-65684 5 months ago |
7-42070 7 days |
13483 |
adomani author:adomani |
feat: automatically replace deprecations |
This PR introduces `lake exe update_deprecations` that uses the cache to automatically replace deprecated declarations with the corresponding un-deprecated one.
The script handles namespacing, replacing a possibly non-fully-qualified, deprecated name with the fully-qualified non-deprecated name.
It is also possible to use
```bash
lake exe update_deprecations --mods One.Two.Three,Dd.Ee.Ff
```
to limit the scope of the replacements to the modules `One.Two.Three` and `Dd.Ee.Ff`.
This is intended to be a first step in automating updates: combining this with a linter that emits appropriate warnings, the functionality of `lake exe update_deprecations` can be extended to perform more complicated updates.
---
[](https://gitpod.io/from-referrer/)
|
t-meta
delegated
awaiting-author
|
306/0 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/UpdateDeprecations.lean,MathlibTest/UpdateDeprecations.lean,lakefile.lean,scripts/README.md,scripts/update_deprecations.lean |
7 |
15 |
['YaelDillies', 'adomani', 'github-actions', 'j-loreaux', 'jcommelin', 'mathlib-bors', 'sgouezel'] |
joneugster assignee:joneugster |
123-14076 4 months ago |
123-14076 4 months ago |
34-82472 34 days |
21265 |
ADedecker author:ADedecker |
feat: some lemmas about pointwise actions of units on filters and uniformities |
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
t-topology
delegated
label:t-algebra$ |
45/0 |
Mathlib/Order/Filter/Pointwise.lean,Mathlib/Topology/Algebra/UniformMulAction.lean |
2 |
7 |
['github-actions', 'mathlib-bors', 'ocfnash'] |
nobody |
87-84005 2 months ago |
87-84005 2 months ago |
15-25642 15 days |
23240 |
urkud author:urkud |
feat(Topology/Maps): `IsOpenMap` and `ClusterPt` |
---
[](https://gitpod.io/from-referrer/)
|
t-topology
delegated
|
17/4 |
Mathlib/Topology/Maps/Basic.lean |
1 |
6 |
['eric-wieser', 'github-actions', 'grunweg', 'mathlib-bors', 'urkud'] |
nobody |
50-69204 1 month ago |
50-76283 1 month ago |
0-12104 3 hours |
22366 |
kim-em author:kim-em |
feat: `check_equalities` tactic for diagnosing defeq problems |
The `check_equalities` tactic,
which checks the typing of equalities in the goal,
reporting discrepancies between the implicit type argument of the equality,
and the inferred types of the left and right hand sides,
at "instances and reducible" transparency.
Reports from this tactic do not necessarily indicate a problem,
although typically `simp` should reduce rather than increase the reported discrepancies.
`check_equalities` may be useful in diagnosing uses of `erw`. |
t-meta
delegated
|
119/3 |
Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Basic.lean,Mathlib/Tactic/CategoryTheory/CheckCompositions.lean,Mathlib/Tactic/CheckEqualities.lean,Mathlib/Tactic/Common.lean,MathlibTest/check_equalities.lean |
7 |
12 |
['adomani', 'b-mehta', 'eric-wieser', 'github-actions', 'mathlib-bors'] |
nobody |
39-27568 1 month ago |
60-17793 1 month ago |
15-14325 15 days |
17129 |
joneugster author:joneugster |
feat(Tactic/Linter): add unicode linter for unicode variant-selectors |
Unicode characters can be followed by one of the two "variant-selectors" `\FE0E` (text) or `\FE0F` (emoji).
These appear to the user as a single unicode character and they might copy them by accident. For example `✅️` (`\u2705\uFE0F`), `✅` (`\u2705`) and `✅︎` (`\u2705\uFE0E`) are three variants of the "same" unicode character. The one without variant-selector might display as either emoji or not, depending on the user's device and font.
Add unicode linter ensuring variant-selector only appear on specified characters and also ensuring these characters always have the correct variant selector to avoid confusions.
Everything flagged by this linter can be fixed fully automatically with `lake exe lint-style --fix` or by commenting `bot fix style` on the PR.
---
- tracking PR: #16215
## Zulip discussions:
- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Whitelist.20for.20Unicode.3F
- https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20specific.20font
## Related PRs:
- leanprover/lean4#5015 added some emoji-variant selectors to Emojis used in `Lean` itself.
[](https://gitpod.io/from-referrer/)
|
large-import
t-linter
delegated
awaiting-author
|
245/14 |
Mathlib.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/TextBased.lean,Mathlib/Tactic/Linter/UnicodeLinter.lean,Mathlib/Tactic/Widget/Calc.lean,Mathlib/Tactic/Widget/CongrM.lean,Mathlib/Tactic/Widget/Conv.lean,Mathlib/Tactic/Widget/GCongr.lean,Mathlib/Topology/ContinuousMap/Weierstrass.lean,MathlibTest/LintStyleTextBased.lean |
11 |
24 |
['YaelDillies', 'adomani', 'github-actions', 'grunweg', 'joneugster', 'kim-em'] |
nobody |
33-39564 1 month ago |
36-47730 1 month ago |
82-54712 82 days |
23600 |
mattrobball author:mattrobball |
perf(Quiver.Basic): make `IsThin` a `class` |
It seems problematic that `Quiver.IsThin` is an `abbrev` for (essentially) `Subsingleton`. We turn it in a one-field class.
---
[](https://gitpod.io/from-referrer/)
|
delegated |
27/21 |
Mathlib/CategoryTheory/Bicategory/Coherence.lean,Mathlib/CategoryTheory/Category/Preorder.lean,Mathlib/CategoryTheory/Generator/Basic.lean,Mathlib/CategoryTheory/Groupoid/Basic.lean,Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean,Mathlib/CategoryTheory/Limits/SmallComplete.lean,Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean,Mathlib/CategoryTheory/Skeletal.lean,Mathlib/CategoryTheory/Subobject/MonoOver.lean,Mathlib/CategoryTheory/Thin.lean,Mathlib/Combinatorics/Quiver/Basic.lean |
11 |
16 |
['b-mehta', 'github-actions', 'leanprover-bot', 'mathlib-bors', 'mattrobball'] |
nobody |
25-14925 25 days ago |
40-13729 1 month ago |
0-5717 1 hour |
23528 |
Ruben-VandeVelde author:Ruben-VandeVelde |
feat: add isOpen_setOf_affineIndependent |
From sphere-eversion.
---
[](https://gitpod.io/from-referrer/)
|
t-analysis
delegated
|
15/0 |
Mathlib/Analysis/Normed/Module/FiniteDimension.lean |
1 |
3 |
['github-actions', 'mathlib-bors', 'urkud'] |
nobody |
15-55654 15 days ago |
15-55655 15 days ago |
26-70139 26 days |
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-34276 14 days ago |
14-34276 14 days ago |
0-55045 15 hours |
23552 |
AntoineChambert-Loir author:AntoineChambert-Loir |
feat(RingTheory/PowerSeries/Substitution): define substitution of power series in power series |
This is the second part of the PR defining substitution of indeterminates by power series in power series.
This one is specific to univariate power series. Basically, the matter is just to remove `Unit ->` in definitions
and make the necessary adjustments.
---
- [x] depends on: #15158
- [x] depends on: #23607 (minor chore)
- [x] depends on: #23642
[](https://gitpod.io/from-referrer/)
|
t-algebra
delegated
label:t-algebra$ |
327/18 |
Mathlib.lean,Mathlib/RingTheory/MvPowerSeries/Substitution.lean,Mathlib/RingTheory/PowerSeries/Evaluation.lean,Mathlib/RingTheory/PowerSeries/Substitution.lean |
4 |
n/a |
['AntoineChambert-Loir', 'b-mehta', 'github-actions', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'riccardobrasca'] |
riccardobrasca assignee:riccardobrasca |
7-32792 7 days ago |
unknown |
unknown |
23213 |
mattrobball author:mattrobball |
chore(RingTheory.Derivation): add a `LinearMapClass` instance |
Often we want `simp` to call `map_zero` or `map_add` for a `Derivation`. To find the `ZeroHomClass` or `AddHomClass` instance necessary it starts to climb up the type class hierarchy including looking for a `LinearMapClass` instance which didn't exist. Consequently, sythesis would look in a lot of crazy places trying to summon ring structures on the module or on derivations itself. Here we add the missing `LinearMapClass` instance so that `simp` is more efficient.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
delegated
label:t-algebra$ |
5/3 |
Mathlib/RingTheory/Derivation/Basic.lean |
1 |
8 |
['github-actions', 'j-loreaux', 'leanprover-bot', 'mathlib-bors', 'mattrobball'] |
nobody |
4-78591 4 days ago |
4-78591 4 days ago |
47-39026 47 days |
23214 |
mattrobball author:mattrobball |
perf(Module.LinearMap.Defs): deprioritize projections to parents for `SemilinearMapClass` |
Trying to figure out if a given type has a `SemilinearMapClass` instance when all we want is an `AddHomClass` or a `MulActionSemiHomClass` can be quite expensive since there are multiple ways to crawl the algebraic hierarchy to generate `LinearMapClass` instances. If these fail, then they fail slowly. We deprioritize the projections from `SemilinearMapClass` to `AddHomClass` and `MulActionSemiHomClass` to make this one of the last choices.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
delegated
label:t-algebra$ |
6/0 |
Mathlib/Algebra/Module/LinearMap/Defs.lean |
1 |
6 |
['github-actions', 'j-loreaux', 'leanprover-bot', 'mathlib-bors', 'mattrobball'] |
nobody |
4-78357 4 days ago |
4-78357 4 days ago |
47-32152 47 days |
23137 |
grunweg author:grunweg |
chore(Topology): some more fun_prop tagging |
---
[](https://gitpod.io/from-referrer/)
|
t-topology
delegated
|
8/4 |
Mathlib/Dynamics/Flow.lean,Mathlib/Topology/Algebra/Monoid.lean |
2 |
10 |
['github-actions', 'grunweg', 'j-loreaux', 'mathlib-bors'] |
nobody |
3-80806 3 days ago |
3-80806 3 days ago |
34-32727 34 days |
22823 |
b-reinke author:b-reinke |
feat(Algebra/Ring): associator of a non-associative ring |
If `R` is a non-associative ring, then `(x * y) * z - x * (y * z)` is called the `associator` of
ring elements `x y z : R`.
The associator vanishes exactly when `R` is associative.
We prove variants of this statement also for the `AddMonoidHom` bundled version of the associator,
as well as the bundled version of `mulLeft₃` and `mulRight₃`, the multiplications `(x * y) * z` and
`x * (y * z)`.
---
[](https://gitpod.io/from-referrer/)
|
large-import
new-contributor
t-algebra
delegated
label:t-algebra$ |
133/8 |
Mathlib.lean,Mathlib/Algebra/DirectSum/Ring.lean,Mathlib/Algebra/Ring/Associator.lean |
3 |
52 |
['Paul-Lez', 'YaelDillies', 'b-reinke', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib-bors'] |
eric-wieser assignee:eric-wieser |
2-34048 2 days ago |
2-69841 2 days ago |
54-29177 54 days |
23487 |
YaelDillies author:YaelDillies |
refactor: spell results using `Minimal`/`MinimalFor` |
And move all the lemmas about existence of minimal/maximal elements in finite sets to a new file `Order.Preorder.Finite`.
From Toric
Moves:
* `Finite.exists_minimal_le` -> `Finite.exists_le_minimal`
---
- [x] depends on: #23586
- [x] depends on: #23592
- [x] depends on: #23624
- [x] depends on: #23706
- [x] depends on: #23737
[](https://gitpod.io/from-referrer/)
|
toric
t-data
delegated
|
236/182 |
Mathlib.lean,Mathlib/Combinatorics/Additive/Dissociation.lean,Mathlib/Combinatorics/Additive/RuzsaCovering.lean,Mathlib/Combinatorics/Colex.lean,Mathlib/Combinatorics/Pigeonhole.lean,Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Data/Fintype/EquivFin.lean,Mathlib/Data/Fintype/Order.lean,Mathlib/Data/Matroid/IndepAxioms.lean,Mathlib/Data/Set/Countable.lean,Mathlib/Data/Set/Finite/Basic.lean,Mathlib/Order/Atoms/Finite.lean,Mathlib/Order/Birkhoff.lean,Mathlib/Order/Interval/Finset/Basic.lean,Mathlib/Order/Interval/Finset/Nat.lean,Mathlib/Order/Interval/Set/OrdConnectedLinear.lean,Mathlib/Order/Minimal.lean,Mathlib/Order/Preorder/Finite.lean,Mathlib/Order/README.md,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/Topology/ShrinkingLemma.lean |
22 |
31 |
['YaelDillies', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib-bors', 'mathlib4-dependent-issues-bot'] |
nobody |
1-21164 1 day ago |
1-62043 1 day ago |
17-23178 17 days |
14712 |
FR-vdash-bot author:FR-vdash-bot |
perf: change instance priority and order about `OfNat` |
---
[](https://gitpod.io/from-referrer/)
|
slow-typeclass-synthesis
t-algebra
merge-conflict
delegated
label:t-algebra$ |
49/20 |
Mathlib/Algebra/Group/Nat.lean,Mathlib/Algebra/Group/ZeroOne.lean,Mathlib/Algebra/Homology/Embedding/Basic.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Data/BitVec.lean,Mathlib/Data/Nat/Cast/Defs.lean,Mathlib/Data/Rat/Defs.lean,Mathlib/Data/UInt.lean,Mathlib/NumberTheory/ArithmeticFunction.lean |
9 |
24 |
['FR-vdash-bot', 'MichaelStollBayreuth', 'eric-wieser', 'github-actions', 'j-loreaux', 'leanprover-bot', 'mathlib-bors'] |
nobody |
219-33987 7 months ago |
221-57463 7 months ago |
20-15089 20 days |
21761 |
JovanGerb author:JovanGerb |
feat(Algebra): add lemmas `mul_self` and `add_self` |
This is point (4) in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Possible.20improvements.20to.20Lean.2FMathlib/near/499085779
I decided to go with `n + n = 2 * n` instead of `n + n = n * 2` because it feels more natural. Feel free to suggest the opposite.
---
[](https://gitpod.io/from-referrer/)
|
t-algebra
merge-conflict
delegated
label:t-algebra$ |
206/196 |
Archive/Imo/Imo1959Q2.lean,Archive/Imo/Imo1961Q3.lean,Archive/Imo/Imo2008Q4.lean,Archive/Imo/Imo2013Q1.lean,Archive/Imo/Imo2024Q3.lean,Archive/MiuLanguage/DecisionSuf.lean,Archive/Wiedijk100Theorems/Partition.lean,Archive/ZagierTwoSquares.lean,Mathlib/Algebra/CharP/Two.lean,Mathlib/Algebra/CharZero/Lemmas.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Even.lean,Mathlib/Algebra/Lie/Weights/RootSystem.lean,Mathlib/Algebra/Order/Field/Basic.lean,Mathlib/Algebra/Order/Group/Lattice.lean,Mathlib/Algebra/Order/Group/Unbundled/Abs.lean,Mathlib/Algebra/Order/Ring/Basic.lean,Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean,Mathlib/Algebra/Order/Round.lean,Mathlib/Algebra/Polynomial/Taylor.lean,Mathlib/Algebra/Ring/BooleanRing.lean,Mathlib/Algebra/Ring/Defs.lean,Mathlib/Algebra/Ring/Hom/Defs.lean,Mathlib/Algebra/Ring/Int/Parity.lean,Mathlib/Algebra/Ring/Invertible.lean,Mathlib/Algebra/Ring/Parity.lean,Mathlib/Algebra/Ring/SumsOfSquares.lean,Mathlib/Algebra/Symmetrized.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean,Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean,Mathlib/Analysis/Complex/Isometry.lean,Mathlib/Analysis/Complex/PhragmenLindelof.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean,Mathlib/Analysis/Convex/Mul.lean,Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean,Mathlib/Analysis/InnerProductSpace/LinearMap.lean,Mathlib/Analysis/Normed/Lp/ProdLp.lean,Mathlib/Analysis/NormedSpace/MStructure.lean,Mathlib/Analysis/RCLike/Basic.lean,Mathlib/Analysis/SpecialFunctions/Bernstein.lean,Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean,Mathlib/Analysis/SpecialFunctions/PolarCoord.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean,Mathlib/Combinatorics/Additive/AP/Three/Defs.lean,Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean,Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean,Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Computability/AkraBazzi/AkraBazzi.lean,Mathlib/Computability/Language.lean,Mathlib/Data/Complex/Abs.lean,Mathlib/Data/Complex/Module.lean,Mathlib/Data/Complex/Norm.lean,Mathlib/Data/ENNReal/Holder.lean,Mathlib/Data/ENNReal/Inv.lean,Mathlib/Data/Nat/Bitwise.lean,Mathlib/Data/Nat/Cast/Order/Ring.lean,Mathlib/Data/Nat/Choose/Central.lean,Mathlib/Data/Num/Lemmas.lean,Mathlib/Data/Num/Prime.lean,Mathlib/Data/Real/Pi/Irrational.lean,Mathlib/Data/ZMod/Basic.lean,Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean,Mathlib/GroupTheory/Coxeter/Inversion.lean,Mathlib/GroupTheory/Perm/Cycle/Type.lean,Mathlib/GroupTheory/SpecificGroups/Alternating.lean,Mathlib/GroupTheory/SpecificGroups/Dihedral.lean,Mathlib/GroupTheory/SpecificGroups/KleinFour.lean,Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean,Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean,Mathlib/LinearAlgebra/Matrix/PosDef.lean,Mathlib/LinearAlgebra/QuadraticForm/Complex.lean,Mathlib/LinearAlgebra/SesquilinearForm.lean,Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean,Mathlib/MeasureTheory/Integral/Bochner.lean,Mathlib/MeasureTheory/Integral/Gamma.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/NumberTheory/Cyclotomic/Embeddings.lean,Mathlib/NumberTheory/FLT/Three.lean,Mathlib/NumberTheory/GaussSum.lean,Mathlib/NumberTheory/LegendreSymbol/Basic.lean,Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean,Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean,Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean,Mathlib/NumberTheory/Multiplicity.lean,Mathlib/NumberTheory/NumberField/Basic.lean,Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean,Mathlib/NumberTheory/PellMatiyasevic.lean,Mathlib/NumberTheory/SumPrimeReciprocals.lean |
117 |
13 |
['JovanGerb', 'YaelDillies', 'github-actions', 'grunweg', 'mathlib-bors', 'riccardobrasca'] |
nobody |
85-82281 2 months ago |
86-27052 2 months ago |
0-54729 15 hours |
21266 |
ADedecker author:ADedecker |
feat: restate uniformContinuous_mul in terms of convergence to uniformity |
This is convenient when working with [Filter.Tendsto.congr_uniformity](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/UniformSpace/Basic.html#Filter.Tendsto.congr_uniformity) or [Filter.Tendsto.uniformity_trans](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/UniformSpace/Basic.html#Filter.Tendsto.uniformity_trans), for example.
---
[](https://gitpod.io/from-referrer/)
|
t-topology
easy
merge-conflict
delegated
|
8/0 |
Mathlib/Topology/Algebra/UniformGroup/Defs.lean |
1 |
5 |
['ADedecker', 'github-actions', 'j-loreaux', 'mathlib-bors'] |
nobody |
43-24708 1 month ago |
43-24708 1 month ago |
0-18788 5 hours |
19275 |
eric-wieser author:eric-wieser |
fix: if nolint files change, do a full rebuild |
Otherwise CI will succeed when removing entries from the file, but fail later when someone changes something unrelated.
---
[](https://gitpod.io/from-referrer/)
|
merge-conflict
delegated
|
8/0 |
lakefile.lean |
1 |
20 |
['YaelDillies', 'adomani', 'eric-wieser', 'github-actions', 'grunweg', 'mathlib-bors'] |
nobody |
39-20331 1 month ago |
39-20331 1 month ago |
0-214 3 minutes |
24714 |
leanprover-community-mathlib4-bot author:leanprover-community-mathlib4-bot |
chore: adaptations for nightly-2025-05-09 |
|
merge-conflict
delegated
|
1085/203 |
Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean,Mathlib/Algebra/Module/Submodule/Defs.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/Pullbacks.lean,Mathlib/Analysis/Normed/Group/Uniform.lean,Mathlib/CategoryTheory/Monoidal/CommGrp_.lean,Mathlib/CategoryTheory/Monoidal/CommMon_.lean,Mathlib/CategoryTheory/Monoidal/Functor.lean,Mathlib/CategoryTheory/Monoidal/Grp_.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/CategoryTheory/Opposites.lean,Mathlib/CategoryTheory/WithTerminal/Cone.lean,Mathlib/Computability/TMComputable.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/RingTheory/HahnSeries/HEval.lean,Mathlib/RingTheory/HahnSeries/Summable.lean,Mathlib/RingTheory/Localization/Basic.lean,Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/SetTheory/ZFC/Class.lean,Mathlib/SetTheory/ZFC/PSet.lean,Mathlib/Tactic/Abel.lean,Mathlib/Tactic/Bound.lean,Mathlib/Tactic/Group.lean,Mathlib/Tactic/NoncommRing.lean,Mathlib/Tactic/NormNum.lean,Mathlib/Tactic/Positivity/Core.lean,Mathlib/Tactic/Ring.lean,Mathlib/Topology/MetricSpace/Isometry.lean,Mathlib/Topology/Order/Basic.lean,MathlibTest/BigOps.lean,MathlibTest/Check.lean,MathlibTest/Simps.lean,MathlibTest/StringDiagram.lean,MathlibTest/abel.lean,MathlibTest/fin_cases.lean,MathlibTest/fun_prop_dev.lean,MathlibTest/hint.lean,MathlibTest/lift.lean,MathlibTest/linear_combination'.lean,MathlibTest/linear_combination.lean,MathlibTest/notation3.lean,MathlibTest/renameBvar.lean,MathlibTest/ring.lean,lake-manifest.json,lean-toolchain,scripts/nolints_prime_decls.txt |
47 |
n/a |
['github-actions', 'kbuzzard', 'leanprover-community-bot-assistant', 'mathlib-bors'] |
nobody |
2-73092 2 days ago |
unknown |
unknown |