| Number |
Author |
Title |
Labels |
+/- |
📝 |
💬 |
Updated |
| #14809 |
jjaassoonn |
feat(AlgebraicGeometry/Tilde): add the map from `M` localising at `x` to the stalk of `M^~` at x |
workshop-AIM-AG-2024
t-algebraic-geometry
|
122/1 |
2 |
7 |
2024-08-06 13:13 (1 months ago) |
| #15452 |
tomaz1502 |
feat(Computability.Timed): Formalization of runtime complexity of List.mergeSort |
t-logic
|
526/0 |
5 |
0 |
2024-08-14 07:49 (1 months ago) |
| #15451 |
tomaz1502 |
feat(Computability.Timed): Formalization of runtime complexity of List.merge |
t-logic
|
287/0 |
4 |
0 |
2024-08-14 07:49 (1 months ago) |
| #15449 |
tomaz1502 |
feat(Computability.Timed): Formalization of runtime complexity of insertion sort |
t-logic
|
104/0 |
2 |
0 |
2024-08-14 07:50 (1 months ago) |
| #15028 |
apnelson1 |
feat(Data/Matroid/Closure): closure + insertion API |
t-data
|
113/2 |
1 |
7 |
2024-08-14 09:50 (1 months ago) |
| #15647 |
TpmKranz |
feat(Data/FinEnum): Option instance and Type recursor |
new-contributor
t-logic
|
69/0 |
2 |
1 |
2024-08-14 10:04 (1 months ago) |
| #15546 |
IvanRenison |
feat(Combinatorics/SimpleGraph): Add definition of disjoint sum of graphs |
t-combinatorics
|
78/0 |
2 |
2 |
2024-08-15 18:07 (1 months ago) |
| #15930 |
vihdzp |
feat(SetTheory/Ordinal/Exponential): `log b x = y ↔ x ∈ Set.Ico (b ^ y) (b ^ (succ y))` |
t-logic
|
50/26 |
1 |
1 |
2024-08-18 07:15 (29 days ago) |
| #15212 |
victorliu5296 |
feat: Add fundamental theorem of calculus-2 for Banach spaces |
new-contributor
t-measure-probability
t-analysis
|
60/1 |
1 |
1 |
2024-08-18 16:14 (29 days ago) |
| #15947 |
jsm28 |
feat(Data/Setoid/Basic): `prod` and `piSetoid` lemmas and equivs |
t-data
|
41/0 |
1 |
1 |
2024-08-18 19:08 (28 days ago) |
| #11090 |
pangelinos |
feat: define spectral spaces and prove that a quasi-compact open of a spectral space is spectral |
new-contributor
t-topology
please-adopt
good first issue
|
69/0 |
1 |
15 |
2024-08-19 14:43 (28 days ago) |
| #14981 |
AntoineChambert-Loir |
feat(MvPowerSeries.LexOrder): lexicographic order of multivariate power series |
t-algebra
|
215/1 |
5 |
11 |
2024-08-21 12:48 (26 days ago) |
| #14983 |
AntoineChambert-Loir |
feat(MvPowerSeries.Order): order of multivariate power series |
t-order
|
537/4 |
6 |
13 |
2024-08-21 12:48 (26 days ago) |
| #14990 |
AntoineChambert-Loir |
feat: define of linear topologies |
t-algebra
t-topology
|
235/0 |
2 |
1 |
2024-08-21 12:48 (26 days ago) |
| #16047 |
mattrobball |
chore(Algebra.Order.Monoid.TypeTags): split into unbundled and bundled ordered algebra |
|
115/103 |
4 |
1 |
2024-08-21 22:17 (25 days ago) |
| #15259 |
erdOne |
feat(AlgebraicGeometry): API for affine opens |
t-algebraic-geometry
|
98/25 |
2 |
1 |
2024-08-22 16:05 (25 days ago) |
| #16061 |
vihdzp |
feat(Data/Finsupp/Defs): `induction_on_max` |
t-data
|
46/0 |
1 |
2 |
2024-08-23 00:17 (24 days ago) |
| #15651 |
TpmKranz |
feat(Computability/NFA): operations for Thompson's construction |
t-computability
new-contributor
|
307/5 |
1 |
6 |
2024-08-23 13:44 (24 days ago) |
| #16106 |
ScottCarnahan |
feat(RingTheory/LaurentSeries): composition of Hasse Derivatives |
t-algebra
|
64/4 |
2 |
1 |
2024-08-25 11:01 (22 days ago) |
| #15686 |
robertmaxton42 |
refactor (LinearAlgebra/FreeProduct): move PowerAlgebra construction to its own namespace, minor simp opts |
new-contributor
|
141/11 |
1 |
1 |
2024-08-26 04:11 (21 days ago) |
| #13964 |
pechersky |
feat(Data/DigitExpansion): begin defining variant of reals without rationals |
t-data
|
518/0 |
3 |
5 |
2024-08-27 14:40 (20 days ago) |
| #13786 |
Multramate |
feat(NumberTheory/EllipticDivisibilitySequence): extend even-odd recursion to integers |
t-number-theory
|
211/96 |
4 |
8 |
2024-08-27 15:26 (20 days ago) |
| #9250 |
FR-vdash-bot |
chore(Algebra/Order/GroupWithZero/Unbundled): remove useless lemmas, use `ZeroLEOneClass` |
t-order
t-algebra
|
246/113 |
5 |
2 |
2024-08-28 03:18 (19 days ago) |
| #15894 |
dagurtomas |
feat(CategoryTheory/Monoidal): Day's reflection theorem |
t-category-theory
|
300/0 |
5 |
4 |
2024-08-28 10:55 (19 days ago) |
| #15915 |
vihdzp |
chore(SetTheory/Ordinal/CantorNormalForm): `CNF.exponents` and `CNF.coeffs` |
t-logic
|
86/58 |
2 |
9 |
2024-08-28 14:07 (19 days ago) |
| #16164 |
ScottCarnahan |
feat (RingTheory/HahnSeries) : coefficient-wise map |
t-algebra
|
81/19 |
4 |
3 |
2024-08-28 17:39 (18 days ago) |
| #16183 |
YaelDillies |
feat: The translation operator |
t-algebra
|
80/0 |
2 |
9 |
2024-08-29 08:04 (18 days ago) |
| #15418 |
LorenzoLuccioli |
feat: Results about `Countable` and `CountableOrCountablyGenerated` for products |
t-measure-probability
|
41/4 |
2 |
4 |
2024-08-29 16:12 (18 days ago) |
| #16267 |
FR-vdash-bot |
chore(Order/RelIso/Basic): `[s : Setoid α]` => `{s : Setoid α}` |
t-data
t-order
|
19/18 |
2 |
1 |
2024-08-29 16:31 (18 days ago) |
| #16087 |
YaelDillies |
chore: Rename `Topology.RestrictGenTopology` to `Topology.RestrictGen` |
t-topology
|
2/2 |
3 |
1 |
2024-08-30 14:35 (17 days ago) |
| #16254 |
FR-vdash-bot |
chore: add coercion for `Setoid` |
t-data
|
13/3 |
2 |
1 |
2024-08-30 16:10 (17 days ago) |
| #16278 |
b-mehta |
feat(Analysis/Convex): Birkhoff's theorem and doubly stochastic matrices |
t-analysis
|
306/0 |
3 |
9 |
2024-08-30 17:51 (16 days ago) |
| #15239 |
EtienneC30 |
feat: compactly generated spaces for proper maps and preimages of compact sets / proper and properly discontinuous actions |
t-topology
|
51/141 |
4 |
2 |
2024-08-30 21:12 (16 days ago) |
| #15904 |
vihdzp |
refactor: delete IsWellOrderLimitElement.lean |
t-order
t-category-theory
RFC
|
31/127 |
3 |
3 |
2024-08-31 04:36 (16 days ago) |
| #15773 |
kkytola |
feat: Add type class for ENat-valued floor functions |
t-order
|
231/0 |
3 |
2 |
2024-08-31 23:20 (15 days ago) |
| #15990 |
vihdzp |
feat(SetTheory/Ordinal/Exponential): more lemmas on `Ordinal.log` |
t-logic
|
44/6 |
1 |
1 |
2024-09-01 17:03 (15 days ago) |
| #15991 |
vihdzp |
feat(SetTheory/Ordinal/CantorNormalForm): induct on base `ω` CNF |
t-logic
|
45/0 |
2 |
1 |
2024-09-01 18:33 (14 days ago) |
| #16392 |
Ruben-VandeVelde |
chore: rename IsAlgClosure fields |
|
25/22 |
5 |
1 |
2024-09-01 19:47 (14 days ago) |
| #15522 |
PhoenixIra |
feat: monotonicity lemmas for OrdinalApprox |
new-contributor
t-logic
t-order
|
53/10 |
1 |
16 |
2024-09-02 09:20 (14 days ago) |
| #16409 |
Ruben-VandeVelde |
doc: fix some issues under RepresentationTheory |
|
14/15 |
5 |
1 |
2024-09-02 09:25 (14 days ago) |
| #16256 |
FR-vdash-bot |
chore(Data/Quot): `[s : Setoid α]` => `{s : Setoid α}` |
t-data
|
23/23 |
3 |
1 |
2024-09-02 10:08 (14 days ago) |
| #16305 |
adomani |
feat: `#guard_exceptions` -- like `#guard_msgs` but for parsers |
t-meta
|
69/0 |
3 |
2 |
2024-09-02 14:02 (14 days ago) |
| #16283 |
vihdzp |
doc(SetTheory/Ordinal/Notation): rewrap and improve docs |
t-logic
documentation
|
65/71 |
1 |
17 |
2024-09-02 18:40 (13 days ago) |
| #16065 |
marcusrossel |
feat: stability of `List.insertionSort` |
t-data
new-contributor
|
87/0 |
1 |
15 |
2024-09-03 08:42 (13 days ago) |
| #16406 |
PhoenixIra |
doc: Improve documentation of ordinal-indexed approximations |
new-contributor
t-logic
|
34/29 |
1 |
14 |
2024-09-03 12:14 (13 days ago) |
| #15346 |
acmepjz |
feat(RingTheory/LinearDisjoint): definition and properties of linearly disjoint of subalgebras |
t-algebra
|
606/1 |
3 |
9 |
2024-09-03 13:57 (13 days ago) |
| #12519 |
EtienneC30 |
feat: separable measure and sufficient condition for Lp spaces to be second-countable |
t-measure-probability
|
520/0 |
2 |
44 |
2024-09-03 17:05 (13 days ago) |
| #14237 |
js2357 |
feat: Define the localization of a fractional ideal at a prime ideal |
new-contributor
t-algebra
|
230/0 |
3 |
19 |
2024-09-04 04:16 (12 days ago) |
| #13248 |
hcWang942 |
feat: basic concepts of auction theory |
new-contributor
t-logic
|
204/0 |
3 |
123 |
2024-09-04 05:59 (12 days ago) |
| #15113 |
acmepjz |
feat: add `map_i[I]nf` for sub(semi)ring, subalgebra, subfield etc. |
t-algebra
|
143/0 |
13 |
4 |
2024-09-04 12:08 (12 days ago) |
| #16454 |
adomani |
test: CI bench |
|
375/0 |
3 |
2 |
2024-09-04 20:14 (11 days ago) |
| #16361 |
vihdzp |
chore(SetTheory/Ordinal/FixedPointApproximants): golf + better variable management |
t-logic
|
66/102 |
1 |
1 |
2024-09-05 04:03 (11 days ago) |
| #14986 |
MichaelStollBayreuth |
feat(LinearAlgebra/QuadraticForm/Basic): weaken invertibility hypothesis on 2 |
t-algebra
|
110/54 |
2 |
5 |
2024-09-05 06:35 (11 days ago) |
| #15466 |
LorenzoLuccioli |
feat (Probability.Kernel): Add definitions and API for `Kernel.fst'` and `snd'` |
t-measure-probability
|
98/0 |
2 |
3 |
2024-09-05 07:33 (11 days ago) |
| #16472 |
YaelDillies |
feat(ContextFreeGrammar): More lemmas about reversal |
t-computability
|
103/55 |
2 |
12 |
2024-09-05 07:51 (11 days ago) |
| #16489 |
Ruben-VandeVelde |
chore: split Topology.Algebra.Module.WeakDual |
|
175/126 |
7 |
2 |
2024-09-05 08:16 (11 days ago) |
| #16483 |
smmercuri |
feat: the completion of a number field at an infinite place |
new-contributor
t-algebra
t-number-theory
|
346/0 |
4 |
1 |
2024-09-05 10:17 (11 days ago) |
| #16503 |
ChrisHughes24 |
feat(ModelTheory): Turning polynomials into ring terms |
t-logic
t-algebra
|
94/0 |
2 |
2 |
2024-09-05 15:20 (11 days ago) |
| #14515 |
joelriou |
feat: the (covariant) long exact sequence of Ext |
t-category-theory
|
176/1 |
5 |
4 |
2024-09-05 16:22 (11 days ago) |
| #16447 |
YaelDillies |
feat: L2 inner product of finite sequences |
t-analysis
|
172/0 |
2 |
3 |
2024-09-05 20:04 (10 days ago) |
| #15764 |
vihdzp |
feat(Counterexamples/GameMultiplication): pre-game product cannot be lifted to games |
t-logic
|
93/8 |
3 |
6 |
2024-09-06 02:23 (10 days ago) |
| #16293 |
vihdzp |
feat(MeasureTheory/MeasurableSpace/Basic): sigma-algebra generated by an element |
t-measure-probability
|
28/1 |
3 |
4 |
2024-09-06 05:56 (10 days ago) |
| #15779 |
vihdzp |
feat(SetTheory/Game/PGame): Improve `insertLeft` / `insertRight` API |
t-logic
|
178/70 |
2 |
2 |
2024-09-06 06:03 (10 days ago) |
| #15443 |
YaelDillies |
feat: The Marcinkiewicz-Zygmund inequality |
t-analysis
|
341/19 |
6 |
26 |
2024-09-06 08:38 (10 days ago) |
| #15527 |
dagurtomas |
feat(Topology): the partition of a space into fibers of a function |
t-topology
|
142/0 |
3 |
6 |
2024-09-06 14:54 (10 days ago) |
| #15705 |
YaelDillies |
feat: The Erdős–Ko–Rado theorem |
t-combinatorics
|
109/0 |
1 |
5 |
2024-09-06 15:10 (10 days ago) |
| #15793 |
vihdzp |
feat(SetTheory/ZFC/Ordinal): Initial development of ordinals in ZFSet |
t-logic
|
58/15 |
1 |
8 |
2024-09-06 17:14 (10 days ago) |
| #16569 |
JonBannon |
feat: (Analysis.InnerProductSpace) Decomposition of Finite-Dimensional Inner Product Space as Direct Sum of Joint Eigenspaces of Commuting Finite Tuples of Symmetric Operators |
t-analysis
|
132/4 |
1 |
1 |
2024-09-07 12:36 (9 days ago) |
| #16579 |
madvorak |
chore(Archive/IMO): refactoring 2021Q1 |
IMO
|
19/22 |
1 |
13 |
2024-09-07 18:13 (8 days ago) |
| #15425 |
pechersky |
feat(QuotientGroup,Ideal/Quotient): group is finite if quotient is finite |
t-algebra
|
60/0 |
4 |
15 |
2024-09-08 18:07 (7 days ago) |
| #14768 |
pechersky |
feat(MetricSpace/Ultra/Normed): Nonarchimedean norms from ultrametrics |
t-algebra
t-topology
t-number-theory
|
460/4 |
7 |
2 |
2024-09-09 01:11 (7 days ago) |
| #14999 |
YaelDillies |
feat: Convex functions are continuous |
t-analysis
|
225/2 |
4 |
19 |
2024-09-09 05:33 (7 days ago) |
| #16543 |
CBirkbeck |
feat(Analysis/NormedSpace/FunctionSeries): add eventually versions |
t-analysis
|
69/1 |
1 |
16 |
2024-09-09 08:22 (7 days ago) |
| #16542 |
CBirkbeck |
feat(Analysis): integer complement in `ℂ` |
t-analysis
|
61/0 |
2 |
3 |
2024-09-09 08:25 (7 days ago) |
| #15741 |
mariainesdff |
feat(Data/Int/WithZero): add WithZeroMultIntToNNReal |
t-algebra
|
95/0 |
2 |
3 |
2024-09-09 08:35 (7 days ago) |
| #15906 |
grunweg |
feat: define singular `n`-manifolds |
t-differential-geometry
|
212/0 |
2 |
4 |
2024-09-09 08:41 (7 days ago) |
| #15723 |
mariainesdff |
feat(FieldTheory): add lemmas about minpoly |
t-algebra
|
29/0 |
2 |
3 |
2024-09-09 08:45 (7 days ago) |
| #16632 |
urkud |
feat(Filter/Ker): prove `ker_iSup` etc |
t-order
|
17/0 |
1 |
1 |
2024-09-09 13:43 (7 days ago) |
| #15053 |
joelriou |
feat(CategoryTheory): the short exact sequence of abelian sheaves of a Mayer-Vietoris square |
t-category-theory
|
137/9 |
4 |
2 |
2024-09-09 13:44 (7 days ago) |
| #16298 |
joelriou |
feat(Algebra/Homology): study of the source of the associator isomorphism for the action of bifunctors on homological complexes |
t-category-theory
|
207/1 |
1 |
1 |
2024-09-09 13:45 (7 days ago) |
| #15939 |
pechersky |
feat(RingTheory): `Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing` |
t-algebra
|
62/0 |
1 |
3 |
2024-09-09 15:47 (7 days ago) |
| #16122 |
kbuzzard |
feat: tensoring with R^n, n finite. |
t-algebra
|
175/0 |
3 |
3 |
2024-09-09 20:40 (6 days ago) |
| #16574 |
adomani |
feat: the header linter |
t-linter
|
442/0 |
6 |
17 |
2024-09-09 20:54 (6 days ago) |
| #16649 |
ScottCarnahan |
feat (RingTheory/HahnSeries/Summable) : coeff fcn, singleton family, family equiv |
t-algebra
|
54/5 |
1 |
1 |
2024-09-10 01:52 (6 days ago) |
| #15914 |
vihdzp |
feat(Data/List/Sort): `List.Sorted.cons` |
t-data
t-order
|
12/0 |
1 |
14 |
2024-09-10 03:07 (6 days ago) |
| #12982 |
callesonne |
feat(FiberCategory/Fibered): define fibered categories |
new-contributor
t-category-theory
|
146/6 |
3 |
13 |
2024-09-10 03:16 (6 days ago) |
| #16282 |
Felix-Weilacher |
feat(Algebra/Group/Action): add definition of equidecomposition |
t-algebra
|
219/0 |
2 |
2 |
2024-09-10 04:16 (6 days ago) |
| #15711 |
znssong |
feat(Combinatorics/SimpleGraph): Some lemmas about walk, cycle and Hamiltonian cycle |
new-contributor
t-combinatorics
|
407/3 |
4 |
20 |
2024-09-10 12:37 (6 days ago) |
| #15033 |
chrisflav |
feat(AlgebraicGeometry): factorization of morphisms with affine target |
t-algebraic-geometry
|
78/0 |
2 |
2 |
2024-09-10 15:40 (6 days ago) |
| #11977 |
101damnations |
feat: tensor products of bialgebras |
t-category-theory
|
217/0 |
3 |
2 |
2024-09-10 18:52 (5 days ago) |
| #16514 |
euprunin |
chore(Mathlib/Util): sort imports alphabetically |
maintainer-merge
|
29/29 |
21 |
5 |
2024-09-10 18:53 (5 days ago) |
| #16687 |
jouglasheen |
feat: a nonarchimedean group is totally disconnected |
new-contributor
t-number-theory
|
189/0 |
3 |
1 |
2024-09-10 21:21 (5 days ago) |
| #16663 |
YnirPaz |
feat (Mathlib/SetTheory/Ordinal/Arithmetic): add bounded recursion on ordinals |
new-contributor
t-logic
|
28/0 |
1 |
12 |
2024-09-10 22:16 (5 days ago) |
| #16586 |
vihdzp |
chore(SetTheory/Ordinal/Arithmetic): `WellFounded.rank` → `IsWellFounded.rank` |
t-order
|
96/34 |
4 |
2 |
2024-09-10 23:21 (5 days ago) |
| #16250 |
Parcly-Taxel |
chore: deprime `induction, cases` in `Combinatorics` |
tech debt
|
323/267 |
39 |
1 |
2024-09-10 23:53 (5 days ago) |
| #16584 |
AntoineChambert-Loir |
feat (Mathlib/RingTheory/MvPolynomial/Groebner) : monomial orders and division |
t-algebra
|
1068/1 |
7 |
8 |
2024-09-11 10:32 (5 days ago) |
| #14874 |
rwst |
feat(Nat/Prime): Primality of some numbers of form `a^n±1` |
t-number-theory
|
118/0 |
2 |
43 |
2024-09-11 16:30 (5 days ago) |
| #16675 |
xroblot |
feat(Analysis/BoxIntegral): Add `UnitPartition` |
t-analysis
|
294/0 |
3 |
1 |
2024-09-11 16:35 (5 days ago) |
| #15426 |
pechersky |
feat(Ideal/IsPrincipalPowQuotient): R/I equiv I^n/I^(n+1) |
t-algebra
|
131/0 |
3 |
10 |
2024-09-12 01:32 (4 days ago) |
| #16656 |
mo271 |
feat(Data/Fintype/List): generalize `fintypeNodupList` (no `DecidableEq`) |
t-data
|
64/24 |
2 |
3 |
2024-09-12 07:36 (4 days ago) |
| #16705 |
iehality |
feat(Computability): r.e. sets are closed under inter/union/projection/composition |
t-computability
|
130/0 |
1 |
1 |
2024-09-12 07:37 (4 days ago) |
| #16394 |
vihdzp |
feat(SetTheory/Cardinal/Basic): generalize universes |
t-logic
|
20/12 |
5 |
6 |
2024-09-12 07:49 (4 days ago) |
| #16216 |
jxjwan |
feat(RingTheory): isotypic components |
t-algebra
|
308/0 |
3 |
0 |
2024-09-12 07:53 (4 days ago) |
| #16723 |
vihdzp |
feat(Logic/Small/Set): `Small (Iic a) → Small (Ixx a)`, etc. |
t-order
|
28/18 |
4 |
1 |
2024-09-12 08:25 (4 days ago) |
| #16710 |
YnirPaz |
feat(SetTheory/Ordinal/Topology): define Ordinal.IsClosed and Ordinal.IsAcc |
t-set-theory
new-contributor
|
37/0 |
2 |
9 |
2024-09-12 08:32 (4 days ago) |
| #16666 |
eric-wieser |
fix: call checkSystem in `linarith` and `ring` |
t-meta
|
239/112 |
7 |
5 |
2024-09-12 08:33 (4 days ago) |
| #15744 |
urkud |
chore(Filter/Pi): add `dcomp_map_pi` |
t-order
t-topology
|
61/0 |
3 |
4 |
2024-09-12 14:26 (4 days ago) |
| #14269 |
Colin166 |
feat(NumberTheory/FactorisationProperties): abundant, pseudoperfect, deficient, and weird numbers |
new-contributor
t-number-theory
help-wanted
|
192/0 |
2 |
79 |
2024-09-12 17:23 (4 days ago) |
| #16737 |
urkud |
chore(UniformSpace): move `ofFun` to a new file |
t-topology
|
61/32 |
9 |
3 |
2024-09-12 18:25 (3 days ago) |
| #16718 |
Ruben-VandeVelde |
chore: tidy various files |
|
95/121 |
25 |
1 |
2024-09-12 19:57 (3 days ago) |
| #15419 |
callesonne |
feat(Bicategory/Grothendieck): Grothendieck construction |
t-category-theory
|
125/0 |
2 |
4 |
2024-09-12 20:01 (3 days ago) |
| #16041 |
vihdzp |
feat(SetTheory/Ordinal/Arithmetic): `Ordinal.toNat` |
t-logic
|
58/0 |
1 |
1 |
2024-09-12 20:41 (3 days ago) |
| #16741 |
Ruben-VandeVelde |
feat: generalize projective module results to semirings |
FLT
|
14/15 |
1 |
1 |
2024-09-12 20:49 (3 days ago) |
| #14033 |
pfaffelh |
feat(MeasureTheory): TendstoInMeasure gives ae unique limits; TendstoInMeasure equivalent to subsequences converging ae |
new-contributor
t-measure-probability
|
208/8 |
5 |
77 |
2024-09-12 20:51 (3 days ago) |
| #16707 |
yoh-tanimoto |
feat(Analysis/InnerProductSpace/Quotient): add the quotient `InnerProductSpace` by the null space |
t-analysis
RFC
|
240/24 |
4 |
9 |
2024-09-12 23:06 (3 days ago) |
| #10653 |
thorimur |
feat: `tfae_have ... :=` syntax |
t-meta
modifies-tactic-syntax
|
212/76 |
3 |
18 |
2024-09-13 02:19 (3 days ago) |
| #16154 |
Parcly-Taxel |
chore: remove all non-test uses of `autoImplicit` |
tech debt
|
78/38 |
3 |
15 |
2024-09-13 04:10 (3 days ago) |
| #16390 |
urkud |
feat(MeasureTheory): generalize `measure_iUnion_eq_iSup` |
t-measure-probability
|
117/127 |
10 |
2 |
2024-09-13 04:33 (3 days ago) |
| #16426 |
mans0954 |
feature(Analysis/Normed/Module/Dual): Add a few polar lemmas |
t-analysis
|
18/0 |
2 |
6 |
2024-09-13 06:02 (3 days ago) |
| #14988 |
mans0954 |
refactor(LinearAlgebra/BilinearForm/TensorProduct): Tensor products of bilinear maps |
t-algebra
|
113/32 |
4 |
5 |
2024-09-13 06:04 (3 days ago) |
| #15809 |
archiebrowne |
feat(RingTheory/MvPolynomial/Ideal): introduce new lemmas about MvPolynomial Ideals |
new-contributor
t-algebra
|
38/0 |
1 |
4 |
2024-09-13 06:45 (3 days ago) |
| #16711 |
JasonKYi |
feat(HolderNorm): Define the Hölder norm |
new-contributor
t-analysis
|
229/0 |
2 |
12 |
2024-09-13 07:28 (3 days ago) |
| #11968 |
JovanGerb |
feat: RefinedDiscrTree |
new-contributor
t-meta
|
2027/1366 |
16 |
24 |
2024-09-13 08:02 (3 days ago) |
| #15009 |
madeve-unipi |
feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem |
new-contributor
t-analysis
|
249/17 |
1 |
24 |
2024-09-13 08:33 (3 days ago) |
| #15883 |
YaelDillies |
feat: Expectation of a function over a finset |
t-algebra
|
425/0 |
3 |
20 |
2024-09-13 10:13 (3 days ago) |
| #16555 |
nomeata |
feat(KrullDimension): height_strictMono, mapping theorems |
t-order
|
35/0 |
1 |
17 |
2024-09-13 10:52 (3 days ago) |
| #15644 |
AntoineChambert-Loir |
feat(Combinatorics/Enumerative/Bell): number of ways of partitioning a set into subsets of given cardinalities |
t-data
t-combinatorics
|
225/0 |
3 |
8 |
2024-09-13 11:30 (3 days ago) |
| #16728 |
javra |
feat(CategoryTheory/Filtered): Finality of StructuredArrow.pre |
t-category-theory
|
91/0 |
2 |
6 |
2024-09-13 11:35 (3 days ago) |
| #14866 |
AntoineChambert-Loir |
feat(RingTheory.MvPowerSeries.Topology) : define the product topology on mv power series |
t-algebra
|
479/0 |
4 |
26 |
2024-09-13 11:36 (3 days ago) |
| #14442 |
amosturchet |
feat(NumberTheory/Ostrowski): First step of the proof of the Archimedean case of Ostrowski's Theorem |
new-contributor
t-number-theory
|
167/16 |
2 |
32 |
2024-09-13 12:14 (3 days ago) |
| #16685 |
euprunin |
chore(Mathlib/Combinatorics): sort imports |
|
14/14 |
14 |
3 |
2024-09-13 14:51 (3 days ago) |
| #16758 |
jjdishere |
feat(Topology/Algebra/Valued/NormedValued): add lemmas for `Valued.toNormedField` |
new-contributor
t-algebra
|
67/0 |
1 |
1 |
2024-09-13 15:08 (3 days ago) |
| #16190 |
AlexBrodbelt |
feat(Archive/Imo): formalize IMO 1982q3 |
IMO
new-contributor
|
366/0 |
2 |
7 |
2024-09-13 15:35 (3 days ago) |
| #16746 |
kbuzzard |
chore: make OreLocalization.smul not irreducible |
FLT
|
1/1 |
1 |
4 |
2024-09-13 15:41 (3 days ago) |
| #13152 |
hannahfechtner |
feat: presented monoids |
new-contributor
t-algebra
|
403/11 |
7 |
23 |
2024-09-13 16:30 (3 days ago) |
| #16667 |
joelriou |
refactor(Algebra/Category/ModuleCat): redefine presheaves of modules as families of objects in `ModuleCat` |
workshop-AIM-AG-2024
t-category-theory
|
482/636 |
14 |
1 |
2024-09-13 19:25 (2 days ago) |
| #16771 |
jjdishere |
feat(FieldTheory): define relative algebraic closure |
new-contributor
t-algebra
|
208/0 |
4 |
2 |
2024-09-13 20:37 (2 days ago) |
| #13710 |
mckoen |
feat(CategoryTheory): `MonoidalClosed` instance on functors to `Type` |
new-contributor
t-category-theory
|
76/0 |
2 |
18 |
2024-09-13 21:30 (2 days ago) |
| #16597 |
Command-Master |
feat: prove Cauchy's upper bound on polynomial roots |
t-analysis
|
89/0 |
2 |
7 |
2024-09-14 03:38 (2 days ago) |
| #15277 |
dupuisf |
feat(CStarAlgebra): matrices with entries in a C⋆-algebra |
t-analysis
|
789/31 |
7 |
34 |
2024-09-14 04:03 (2 days ago) |
| #16549 |
urkud |
feat(Topology): define `IsOpenQuotientMap` |
t-topology
|
87/0 |
4 |
1 |
2024-09-14 04:33 (2 days ago) |
| #16359 |
vihdzp |
chore(SetTheory/Cardinal/Basic): organize file |
t-logic
|
255/254 |
6 |
9 |
2024-09-14 04:36 (2 days ago) |
| #16792 |
Command-Master |
feat(RingTheory/Derivation/Basic): define lifting a derivation via an algebra homomorphism |
t-algebra
|
64/0 |
1 |
1 |
2024-09-14 05:27 (2 days ago) |
| #14967 |
Command-Master |
feat(RingTheory/Derivation/MapCoeffs): define `mapCoeffs` on a differential ring |
t-algebra
|
118/2 |
1 |
3 |
2024-09-14 05:36 (2 days ago) |
| #16786 |
urkud |
feat(List): add `exists_mem_iff_getElem` |
t-data
easy
|
9/0 |
1 |
1 |
2024-09-14 06:13 (2 days ago) |
| #15478 |
kkytola |
feat: in separable Borel spaces, convergence in distribution is metrizable (not just pseudometrizable) |
t-measure-probability
|
112/64 |
1 |
9 |
2024-09-14 08:07 (2 days ago) |
| #15645 |
haitian-yuki |
feat: Multiset lemmas |
t-data
maintainer-merge
new-contributor
|
18/0 |
1 |
21 |
2024-09-14 10:11 (2 days ago) |
| #16143 |
callesonne |
feat(MorphismProperty/Presheaf): add `relative` morphism property |
workshop-AIM-AG-2024
t-category-theory
|
93/8 |
1 |
3 |
2024-09-14 12:41 (2 days ago) |
| #15666 |
pimotte |
feat(Combinatorics/SimpleGraph): added matchings in cliques |
t-combinatorics
|
118/0 |
4 |
3 |
2024-09-14 16:13 (2 days ago) |
| #16799 |
awainverse |
chore(ModelTheory/Equivalence): Cleanup of `FirstOrder.Language.Theory.SemanticallyEquivalent` |
t-logic
|
173/130 |
4 |
1 |
2024-09-14 19:09 (1 days ago) |
| #16772 |
euprunin |
feat: add unsorted imports linter |
awaiting-zulip
t-linter
|
1843/1 |
2 |
4 |
2024-09-14 20:12 (1 days ago) |
| #16802 |
bjoernkjoshanssen |
feat: add First Derivative Test from calculus |
new-contributor
|
261/0 |
3 |
1 |
2024-09-14 20:13 (1 days ago) |
| #15535 |
adomani |
feat(Tactic/Linter): the pedantic linter |
t-linter
t-meta
|
216/3 |
8 |
13 |
2024-09-14 21:01 (1 days ago) |
| #16020 |
adomani |
feat: compare PR `olean`s size with `master` |
CI
|
136/0 |
5 |
39 |
2024-09-15 02:09 (1 days ago) |
| #15897 |
mattrobball |
chore: use `Batteries` test driver directly in the lake file |
CI
|
2/33 |
2 |
4 |
2024-09-15 02:12 (1 days ago) |
| #15936 |
zeramorphic |
feat: add Dockerfiles for lean and mathlib |
CI
|
114/4 |
5 |
5 |
2024-09-15 02:18 (1 days ago) |
| #16291 |
urkud |
feat(LocallyCompact): generalize `*Embedding.locallyCompactSpace` |
t-topology
easy
|
32/23 |
3 |
1 |
2024-09-15 03:21 (1 days ago) |
| #16788 |
urkud |
chore(Tactic/GCongr): new file for `@[gcongr] leanInitLemma` |
t-data
|
17/5 |
6 |
1 |
2024-09-15 05:12 (1 days ago) |
| #16488 |
adomani |
feat(CI): add summary of benchmarking output |
CI
|
244/0 |
2 |
22 |
2024-09-15 05:49 (1 days ago) |
| #15938 |
adomani |
feat: add autolabeling of PRs |
t-meta
|
416/0 |
6 |
22 |
2024-09-15 07:50 (1 days ago) |
| #16769 |
Command-Master |
feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` |
t-combinatorics
|
68/25 |
4 |
1 |
2024-09-15 09:33 (1 days ago) |
| #16817 |
Thmoas-Guan |
feat(Topology/Group): More on special subgroups |
new-contributor
t-algebra
t-topology
|
237/0 |
4 |
2 |
2024-09-15 10:44 (1 days ago) |
| #16822 |
xroblot |
feat(Module/ZLattice): define the coimage of a ZLattice |
t-algebra
|
102/8 |
2 |
1 |
2024-09-15 13:13 (1 days ago) |
| #16743 |
agjftucker |
feat(Analysis/Calculus/Implicit): define HasStrictDerivAt.implicitFunOfBivariate |
new-contributor
t-analysis
|
122/5 |
4 |
1 |
2024-09-15 17:55 (23 hours ago) |
| #16727 |
chrisflav |
feat(RingTheory): composition of presentations |
workshop-AIM-AG-2024
t-algebra
t-algebraic-geometry
|
157/2 |
4 |
1 |
2024-09-15 18:58 (22 hours ago) |
| #16713 |
arulandu |
feat(Probability/Distributions): formalize Pareto distribution |
new-contributor
t-measure-probability
|
150/0 |
2 |
29 |
2024-09-15 20:00 (21 hours ago) |
| #9602 |
AntoineChambert-Loir |
feat: lemmas on permutations, cycles, etc. |
t-algebra
|
373/6 |
6 |
84 |
2024-09-15 20:40 (20 hours ago) |
| #16829 |
urkud |
feat(MeasureTheory/Borel): add `nullMeasurable_Ixx` |
t-measure-probability
easy
|
49/26 |
12 |
1 |
2024-09-15 20:47 (20 hours ago) |
| #15088 |
acmepjz |
feat: add `[s|i]sup_toXXX` for intermediate fields and subalgebras |
t-algebra
|
83/0 |
2 |
13 |
2024-09-15 20:56 (20 hours ago) |
| #15874 |
vihdzp |
chore(Order/InitialSeg): Improve proofs and comments |
t-order
documentation
|
141/147 |
3 |
21 |
2024-09-15 23:10 (18 hours ago) |
| #16730 |
pechersky |
feat(Topology/UniformSpace): `Subtype.isComplete_iff` |
t-topology
easy
|
15/0 |
1 |
4 |
2024-09-15 23:14 (18 hours ago) |
| #16832 |
urkud |
chore(VectorMeasure): drop `T2Space` assumption here and there |
t-measure-probability
|
42/53 |
3 |
1 |
2024-09-16 01:38 (15 hours ago) |
| #16833 |
urkud |
chore(VectorMeasure): move `ComplexMeasure` to `Complex` |
t-measure-probability
easy
|
6/5 |
2 |
1 |
2024-09-16 01:41 (15 hours ago) |
| #16814 |
semorrison |
feat: Composition.blocksFun_le |
t-combinatorics
|
21/1 |
2 |
5 |
2024-09-16 01:52 (15 hours ago) |
| #16598 |
Parcly-Taxel |
feat: `Fintype (Finpartition s)` for `s : Finset α` |
t-combinatorics
|
9/0 |
1 |
12 |
2024-09-16 02:14 (15 hours ago) |
| #16835 |
Parcly-Taxel |
feat: `Finpartition.attachEquiv` |
t-combinatorics
|
89/0 |
2 |
1 |
2024-09-16 03:14 (14 hours ago) |
| #16520 |
euprunin |
chore(Mathlib/Logic): sort imports |
maintainer-merge
|
25/25 |
16 |
5 |
2024-09-16 04:44 (12 hours ago) |
| #16836 |
Parcly-Taxel |
chore: delete deprecated algebraic structure files |
tech debt
easy
|
0/1890 |
7 |
3 |
2024-09-16 04:48 (12 hours ago) |
| #16593 |
hrmacbeth |
feat: `match_scalars` and `module` tactics |
t-meta
|
952/1 |
5 |
18 |
2024-09-16 04:49 (12 hours ago) |
| #16838 |
euprunin |
chore(Mathlib/SetTheory): sort imports |
|
10/10 |
8 |
3 |
2024-09-16 05:13 (12 hours ago) |
| #16840 |
hrmacbeth |
feat: `ring`-based prover for certain inequalities in semirings |
t-meta
|
302/11 |
7 |
1 |
2024-09-16 05:14 (12 hours ago) |
| #14029 |
AntoineChambert-Loir |
feat(GroupTheory/GroupAction/Blocks): lemmas to handle blocks on finite sets |
t-algebra
|
148/10 |
2 |
37 |
2024-09-16 06:49 (10 hours ago) |
| #16722 |
ScottCarnahan |
feat (LinearAlgebra/RootSystem) : Construct root systems from bilinear forms on reflexive modules |
t-algebra
|
195/0 |
2 |
14 |
2024-09-16 08:27 (8 hours ago) |
| #16809 |
vihdzp |
doc(SetTheory/Game/PGame): expand docstrings for `≤` and `⧏` |
easy
documentation
|
4/2 |
1 |
5 |
2024-09-16 08:34 (8 hours ago) |
| #16054 |
vihdzp |
chore(SetTheory/Game/Impartial): remove `Impartial` typeclass |
t-combinatorics
RFC
|
152/149 |
2 |
2 |
2024-09-16 08:34 (8 hours ago) |
| #16845 |
madvorak |
chore(Archive/IMO/1962Q1): better hypothesis names |
IMO
|
56/62 |
1 |
1 |
2024-09-16 08:41 (8 hours ago) |
| #16846 |
madvorak |
chore(Archive/IMO/2024Q2): `apply (...).trans` instead of `suffices (...); exact` |
IMO
easy
|
6/10 |
1 |
1 |
2024-09-16 09:12 (8 hours ago) |
| #16398 |
FR-vdash-bot |
refactor(SetTheory/ZFC/Basic): redefine `Definable` |
|
168/74 |
1 |
6 |
2024-09-16 09:36 (7 hours ago) |
| #16078 |
vihdzp |
feat(Data/*/Sort): lemmas on sorted lists |
t-data
|
45/0 |
4 |
3 |
2024-09-16 09:49 (7 hours ago) |
| #16327 |
EtienneC30 |
feat: rewrite cylinders projective families of measures in terms of `Function.proj` |
t-measure-probability
|
245/32 |
6 |
2 |
2024-09-16 10:22 (7 hours ago) |
| #16848 |
vihdzp |
chore(NumberTheory/LucasPrimality): golf theorem |
t-number-theory
|
10/21 |
1 |
1 |
2024-09-16 10:28 (6 hours ago) |
| #16847 |
D-Thomine |
chore: remove unnecessary NeBot assumptions |
|
88/64 |
8 |
1 |
2024-09-16 11:00 (6 hours ago) |
| #16834 |
Aaron1011 |
feat(NumberTheory): add converse of Lucas test for primes |
new-contributor
t-number-theory
|
73/3 |
1 |
8 |
2024-09-16 11:00 (6 hours ago) |
| #16851 |
vihdzp |
chore(SetTheory/Cardinal/Basic): inline `mul_comm` into instance |
t-set-theory
|
18/22 |
1 |
1 |
2024-09-16 12:04 (5 hours ago) |
| #16631 |
mbkybky |
feat(RingTheory/DedekindDomain): `IsDedekindDomainDvr` implies `IsDedekindDomain` |
new-contributor
t-algebra
|
35/2 |
1 |
2 |
2024-09-16 12:08 (5 hours ago) |
| #16853 |
chrisflav |
feat(RingTheory/StandardSmooth): base change of standard smooth algebras |
workshop-AIM-AG-2024
t-algebra
t-algebraic-geometry
|
93/4 |
3 |
1 |
2024-09-16 12:38 (4 hours ago) |
| #15445 |
mariainesdff |
feat(Analysis.Normed.Ring.IsPowMulFaithful): prove eq_of_powMul_faithful |
t-analysis
t-number-theory
|
356/0 |
6 |
15 |
2024-09-16 12:46 (4 hours ago) |
| #9417 |
Multramate |
feat(AlgebraicGeometry/EllipticCurve/Projective): implement group operation polynomials for projective coordinates |
t-algebraic-geometry
t-number-theory
|
726/18 |
2 |
5 |
2024-09-16 13:12 (4 hours ago) |
| #16217 |
callesonne |
feat(Tactic/Algebraize): add algebraize tactic |
workshop-AIM-AG-2024
t-algebra
t-meta
|
396/58 |
11 |
64 |
2024-09-16 13:19 (4 hours ago) |
| #16557 |
Jun2M |
feat(Sym2): Add pmap |
t-data
|
27/0 |
1 |
7 |
2024-09-16 13:33 (3 hours ago) |
| #16650 |
kbuzzard |
feat: Ore localization of a commutative algebra is an algebra. |
FLT
t-algebra
|
245/13 |
5 |
7 |
2024-09-16 13:44 (3 hours ago) |
| #16821 |
b-mehta |
chore(Data/Finset/Image): simplify proof of filter_mem_image_eq_image |
t-data
|
4/11 |
2 |
4 |
2024-09-16 13:54 (3 hours ago) |
| #16826 |
mans0954 |
feat(Topology/Order): Sierpiński space classifies open sets of Scott topology |
t-order
|
41/0 |
3 |
3 |
2024-09-16 13:57 (3 hours ago) |
| #16849 |
mbkybky |
feat(NumberTheory/NumberField): Restricting maps to the ring of integers |
new-contributor
t-number-theory
|
60/0 |
2 |
1 |
2024-09-16 13:57 (3 hours ago) |
| #16852 |
yuma-mizuno |
feat(CategoryTheory): proof producing coherence tactic |
t-category-theory
t-meta
|
4939/1049 |
38 |
5 |
2024-09-16 14:22 (3 hours ago) |
| #16639 |
Julian |
feat(RingTheory/LaurentSeries): add notation |
t-algebra
|
47/38 |
1 |
4 |
2024-09-16 14:23 (3 hours ago) |
| #15878 |
Louddy |
feat(SkewMonoidAlgebra): add SkewMonoidAlgebra with irreducible def |
new-contributor
t-algebra
|
166/0 |
2 |
18 |
2024-09-16 15:06 (2 hours ago) |
| #16855 |
jcommelin |
chore: adaptations for nightly-2024-09-16 |
|
30/42 |
16 |
1 |
2024-09-16 15:10 (2 hours ago) |
| #14503 |
jjaassoonn |
feat: definition of a simple ring |
t-algebra
|
126/0 |
5 |
21 |
2024-09-16 15:44 (1 hours ago) |
| #16857 |
siddhartha-gadgil |
Explicit dependency and update for LeanSearchClient |
ready-to-merge
|
4/3 |
2 |
1 |
2024-09-16 16:20 (1 hours ago) |
| #16804 |
awainverse |
feat(ModelTheory/Order): The theory of dense linear orders is countably categorical, and thus complete |
t-logic
t-order
ready-to-merge
|
41/9 |
3 |
2 |
2024-09-16 16:39 (46 minutes ago) |
| #16844 |
sgouezel |
feat: a continuous linear map into continuous multilinear maps is analytic |
t-analysis
ready-to-merge
|
171/8 |
3 |
2 |
2024-09-16 16:48 (37 minutes ago) |
| #16843 |
sgouezel |
feat: more API for `AnalyticWithinAt` |
t-analysis
ready-to-merge
|
364/88 |
8 |
1 |
2024-09-16 16:48 (37 minutes ago) |
| #16719 |
vihdzp |
feat(Order/SuccPred/Limit): induction principles for `IsSuccLimit` and `IsPredLimit` |
maintainer-merge
t-order
ready-to-merge
|
233/64 |
2 |
7 |
2024-09-16 16:52 (32 minutes ago) |
| #15820 |
vihdzp |
refactor(SetTheory/Ordinal/Arithmetic): Ditch `Ordinal.sup` |
maintainer-merge
t-logic
ready-to-merge
|
380/124 |
7 |
65 |
2024-09-16 16:54 (31 minutes ago) |
| #16088 |
vihdzp |
feat(SetTheory/Ordinal/Nimber): Initial development of nimbers |
maintainer-merge
t-logic
ready-to-merge
|
361/0 |
2 |
21 |
2024-09-16 16:55 (30 minutes ago) |
| #15716 |
vihdzp |
feat(SetTheory/Game/Birthday): Define birthday of a game |
maintainer-merge
t-logic
ready-to-merge
|
146/30 |
5 |
42 |
2024-09-16 16:55 (29 minutes ago) |
| #13810 |
niklasmohrin |
feat(Combinatorics/SimpleGraph): add `Fintype` instance for `Path` |
new-contributor
t-combinatorics
|
53/0 |
1 |
29 |
2024-09-16 16:57 (28 minutes ago) |
| #15940 |
pechersky |
feat(Order/SuccPred/TypeTags): `SuccOrder (Multiplicative X)` and friends |
maintainer-merge
t-order
t-algebra
ready-to-merge
|
51/0 |
2 |
3 |
2024-09-16 16:59 (26 minutes ago) |
| #16668 |
chrisflav |
feat(CategorTheory/Galois): stabilizers form a neighborhood basis of the identity |
t-topology
t-category-theory
ready-to-merge
|
122/7 |
4 |
4 |
2024-09-16 17:03 (22 minutes ago) |
| #15777 |
pechersky |
feat(Normed/Field): `completeSpace_iff_isComplete_closedBall` |
t-topology
|
175/0 |
5 |
13 |
2024-09-16 17:04 (21 minutes ago) |
| #15846 |
pechersky |
feat(GroupTheory/Archimedean): `LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered` |
t-order
t-algebra
|
37/0 |
2 |
4 |
2024-09-16 17:06 (19 minutes ago) |
| #16025 |
jcommelin |
refactor(LinearAlgebra/Eigenspace): unified definition of (max(gen)?)?Eigenspace |
t-algebra
|
521/157 |
5 |
1 |
2024-09-16 17:08 (16 minutes ago) |