Zulip Chat Archive

Stream: PR reviews

Topics:

Results on maximal acyclic subgraphs (7 messages, latest: Dec 20 2025 at 08:38)
#33034 removing privateInPublic from lakefile (55 messages, latest: Dec 19 2025 at 19:52)
PRs towards IMO geometry 2024 P4 (8 messages, latest: Dec 19 2025 at 17:55)
Immersions and smooth embeddings (21 messages, latest: Dec 18 2025 at 17:04)
#26446 full subcategories refactor (5 messages, latest: Dec 18 2025 at 13:51)
(merged) #32776 grind and aesop annotations for ZMod (8 messages, latest: Dec 17 2025 at 23:18)
#30089 modular forms bounds (1 message, latest: Dec 16 2025 at 07:03)
Simplex reindexing PRs (4 messages, latest: Dec 15 2025 at 22:56)
More angle bisection lemmas #30474, #30476, #30477, … (11 messages, latest: Dec 15 2025 at 22:54)
#32892 arithmetic-geometric mean (5 messages, latest: Dec 15 2025 at 17:32)
PR #31821 Singular Value Decomposition (53 messages, latest: Dec 15 2025 at 16:51)
Tempered distributions (26 messages, latest: Dec 12 2025 at 22:37)
#30511 use fun_prop in measurability (18 messages, latest: Dec 12 2025 at 19:08)
(Classical) Distributions (42 messages, latest: Dec 12 2025 at 16:32)
Prokhorov theorem #32701 (11 messages, latest: Dec 12 2025 at 11:59)
Actually removing deprecated modules (5 messages, latest: Dec 12 2025 at 07:13)
#32116 - stuck in a pause (2 messages, latest: Dec 12 2025 at 01:19)
feat: register mathlib tactics with try? (4 messages, latest: Dec 10 2025 at 04:54)
#32599 – make Complex.exp an irreducible_def (14 messages, latest: Dec 08 2025 at 21:50)
#29422 [LinearOrder α] [DecidableEq α] (33 messages, latest: Dec 08 2025 at 04:06)
#32079 UniformContinuous version of uniform limit theorem (1 message, latest: Dec 06 2025 at 22:26)
#30669 doc(Algebra): fix typos (2 messages, latest: Dec 05 2025 at 22:01)
#30618 Glaisher's theorem & other Nat.Partition stuff (5 messages, latest: Dec 05 2025 at 12:35)
chore(Algebra): extract Submonoid.IsLocalizationMap #29596 (8 messages, latest: Dec 04 2025 at 23:20)
#32374 (3 messages, latest: Dec 04 2025 at 22:57)
#32379 prove smooth function is non-analytic (2 messages, latest: Dec 03 2025 at 18:52)
#30570 SimpleGraph reachabilitySet (1 message, latest: Dec 02 2025 at 00:54)
#30526 use Subrelation in Mathlib.Logic.Relation (10 messages, latest: Dec 02 2025 at 00:48)
#29602 Infinite conditional sums API (197 messages, latest: Nov 30 2025 at 11:34)
feat: #grind_lint check in module Mathlib #31866 (14 messages, latest: Nov 28 2025 at 16:06)
#29734 irreducibility of kernels (3 messages, latest: Nov 27 2025 at 13:41)
#30273 (already merged) (28 messages, latest: Nov 26 2025 at 19:35)
#8435: run hint tactics in parallel (10 messages, latest: Nov 26 2025 at 05:24)
#31294 feat(Analysis): Weierstrass ℘ functions (5 messages, latest: Nov 25 2025 at 11:54)
#27282 Real algebra (4 messages, latest: Nov 24 2025 at 22:25)
feat: fix_deprecations.py script #30994 (4 messages, latest: Nov 24 2025 at 18:11)
grind annotations (5 messages, latest: Nov 23 2025 at 03:33)
#28604 NonAssocComm(Semi)ring (3 messages, latest: Nov 21 2025 at 22:29)
#30678 Module and fast_instance% for Quaternion (1 message, latest: Nov 21 2025 at 16:15)
#30181 reducible strong recursion (2 messages, latest: Nov 21 2025 at 15:36)
#29856 add nonassociative normed rings (45 messages, latest: Nov 20 2025 at 12:23)
#23238 extended floor and ceil (13 messages, latest: Nov 20 2025 at 07:16)
#31789 More fast_instance% (20 messages, latest: Nov 19 2025 at 13:52)
#30855 deprecate IsTotal in favour of Std.Total (1 message, latest: Nov 18 2025 at 16:09)
feat: extract_goal preserves explicit foralls #31342 (1 message, latest: Nov 18 2025 at 01:33)
#30987 SpecialLinearGroup of a module (9 messages, latest: Nov 17 2025 at 12:55)
#31653 Følner filters (1 message, latest: Nov 16 2025 at 09:05)
#16981 Open normal subgroup in clopen nhds (45 messages, latest: Nov 15 2025 at 13:52)
Feedback requested on PR #30962: lattice path lemmas (3 messages, latest: Nov 15 2025 at 00:16)
#26110 sharp monoid (2 messages, latest: Nov 14 2025 at 17:39)
[#28325 LocallyCompactSpace Γ₀ ↔ Nonempty (LocallyFiniteOrder](topic/.2328325.20LocallyCompactSpace.20.CE.93.E2.82.80.20.E2.86.94.20Nonempty.20(LocallyFiniteOrder.html) (1 message, latest: Nov 14 2025 at 17:38)
#24730 feat(RingTheory): group-like elements (3 messages, latest: Nov 14 2025 at 11:12)
aristotle task for command palette (10 messages, latest: Nov 13 2025 at 08:10)
#26986 bijection between partitions of n and n - r (3 messages, latest: Nov 10 2025 at 05:40)
#30791 generalizing IsGaloisGroup (67 messages, latest: Nov 09 2025 at 19:06)
#30960 golf Combinatorics.SimpleGraph.Walk (1 message, latest: Nov 07 2025 at 04:05)
#29028 define unitary R →* StarAlgEquiv S R R (30 messages, latest: Nov 06 2025 at 10:09)
#30913 feat(Computability/Language):add subtraction notation (9 messages, latest: Nov 06 2025 at 10:03)
#22639 (cyclically) reduced words (40 messages, latest: Nov 06 2025 at 09:22)
#26510: feat(Matroid): exchange lemmas involving closure (4 messages, latest: Nov 05 2025 at 18:45)
PRs from Toric (52 messages, latest: Nov 04 2025 at 21:40)
#30285 document Spec(R) (1 message, latest: Nov 02 2025 at 16:22)
#11060 add min max list operations (1 message, latest: Nov 02 2025 at 11:13)
#30881 the generating function for large and small Schroder (1 message, latest: Nov 02 2025 at 04:15)
#30609 Define large and small Schröder numbers (1 message, latest: Nov 02 2025 at 04:04)
#27308 IsSymmetricAlgebra (8 messages, latest: Nov 02 2025 at 02:01)
#27824 exists_gt_of_deriv_pos (18 messages, latest: Oct 31 2025 at 18:28)
#25140 Hahn embedding theorem (124 messages, latest: Oct 31 2025 at 18:21)
#12190 have vs let linter (100 messages, latest: Oct 31 2025 at 18:21)
#28198 instances for EuclideanSpace rank (13 messages, latest: Oct 31 2025 at 17:02)
#26793 proves on difference sequences in combinatorial Math (14 messages, latest: Oct 31 2025 at 05:06)
#30759 remove declarations deprecated before 2025-04-21 (8 messages, latest: Oct 30 2025 at 15:46)
#30854 theorems on affine independence and automorphisms (9 messages, latest: Oct 28 2025 at 13:52)
#29735 order instances on quotients (2 messages, latest: Oct 27 2025 at 14:40)
#30553 splitting SchwartzSpace (1 message, latest: Oct 27 2025 at 04:19)
#30389 correctly apply hint priority (1 message, latest: Oct 26 2025 at 01:57)
Request for review: #27414 semilinear sets intersect/compl (1 message, latest: Oct 25 2025 at 15:15)
#26221 Towards geodesics and the Levi-Civita connection (87 messages, latest: Oct 23 2025 at 16:30)
#30782 chore(ModelTheory/PartialEquiv): use grind… (1 message, latest: Oct 23 2025 at 12:42)
#30814 Rank decomposition and bases adapted to a linear map (3 messages, latest: Oct 23 2025 at 10:35)
#29040 Erroneous "Unused import" linter (10 messages, latest: Oct 23 2025 at 10:05)
#30783 chore(MeasureTheory/Covering): simp adaptation notes (2 messages, latest: Oct 22 2025 at 18:00)
#26464 generators of pi tensor products (2 messages, latest: Oct 21 2025 at 14:44)
#30400 super simple universe change (1 message, latest: Oct 21 2025 at 09:51)
#30615 norm_num for rpow, renaming of norm_num lemmas (9 messages, latest: Oct 19 2025 at 14:39)
#28818, style issue for forall implications (7 messages, latest: Oct 19 2025 at 09:21)
#26330: Junk values (35 messages, latest: Oct 18 2025 at 04:42)
#28399 feat: ring-theoretic fractions in Rat (2 messages, latest: Oct 17 2025 at 13:57)
#30586 Inductive definition of IsAdmissible (10 messages, latest: Oct 16 2025 at 10:10)
#30313 feat(Data/List/Sigma): grind annotations, missing API (2 messages, latest: Oct 14 2025 at 00:48)
#30341 limits for ProfiniteAddGrp (1 message, latest: Oct 13 2025 at 20:58)
#29207 reorder Algebra.MonoidAlgebra.Defs (7 messages, latest: Oct 13 2025 at 08:45)
#9820 homogeneous submodule (8 messages, latest: Oct 11 2025 at 20:42)
#29413, #29418, #29656 incenter, simplex interior, bisector (4 messages, latest: Oct 07 2025 at 12:20)
#30244 misc. generalizations by LLM (13 messages, latest: Oct 06 2025 at 06:30)
#30183 move factorial theorem (11 messages, latest: Oct 05 2025 at 22:07)
#28871 Tournaments (1 message, latest: Oct 04 2025 at 13:13)
#29582 rename docs#prop to Prop.finite (43 messages, latest: Sep 30 2025 at 07:53)
#29914 Infinite conditional sums API (redux) (1 message, latest: Sep 27 2025 at 20:45)
#29437 Seq.subsequence (8 messages, latest: Sep 26 2025 at 21:22)
#28818 Setoid.ker_lift (29 messages, latest: Sep 25 2025 at 06:03)
#27082, #27639 preliminary of semilinear set PRs (3 messages, latest: Sep 24 2025 at 13:59)
#28669 chore: clean up some proofs about locally compact val (15 messages, latest: Sep 23 2025 at 16:48)
#29362 periods of lists and the Periodicity Lemma (4 messages, latest: Sep 23 2025 at 08:25)
#26031 the derived category is linear (3 messages, latest: Sep 22 2025 at 14:44)
#28803 refactor: unbundle algebra from ENormed* (114 messages, latest: Sep 22 2025 at 09:32)
Simprocs blog post 2 (1 message, latest: Sep 21 2025 at 20:39)
#29364 field_simp for inequalities (6 messages, latest: Sep 20 2025 at 14:24)
#29334 Should grind be preferred to linear_combination? (56 messages, latest: Sep 19 2025 at 11:11)
#29639 (15 messages, latest: Sep 19 2025 at 07:31)
#29788 add bundled ContinuousMaps: allegedly unused import (14 messages, latest: Sep 19 2025 at 02:21)
PR #29713: Euler-Poincaré formula (3 messages, latest: Sep 18 2025 at 11:39)
#28702: MulOne and MonoidHom (8 messages, latest: Sep 18 2025 at 00:06)
#26129 triangle inequality for angles (9 messages, latest: Sep 17 2025 at 19:05)
#28484 More golfs in Data (1 message, latest: Sep 17 2025 at 17:24)
#29058 Colex type alias (4 messages, latest: Sep 17 2025 at 15:21)
# 29464 corrections to docs by way of LLM (24 messages, latest: Sep 16 2025 at 07:49)
cutsat and grobner macro frontends to grind #29468 (2 messages, latest: Sep 16 2025 at 01:15)
#29588 basic residue definitions (14 messages, latest: Sep 14 2025 at 20:29)
#29115: develop some more limUnder API (16 messages, latest: Sep 12 2025 at 17:51)
representation of reals in [0, 1] in positional system (39 messages, latest: Sep 11 2025 at 21:01)
HasPrimitives on disc #9598 (4 messages, latest: Sep 11 2025 at 12:48)
#6718 Lindemann-Weierstrass Theorem (20 messages, latest: Sep 11 2025 at 11:52)
Jeremy Tan's open PRs (91 messages, latest: Sep 11 2025 at 08:10)
#29092 absolutely continuous functions (12 messages, latest: Sep 10 2025 at 19:48)
#25201 Upper bound of dimension of polynomial ring (14 messages, latest: Sep 10 2025 at 09:02)
#29057 AddCircle.liftIoc_continuous (3 messages, latest: Sep 09 2025 at 14:56)
could someone please take a look at mathlib4 PR #28175 (2 messages, latest: Sep 09 2025 at 11:55)
#28589 More lemmas on char 2 rings (1 message, latest: Sep 06 2025 at 06:54)
#26453 PNat and Order instances (3 messages, latest: Sep 05 2025 at 15:33)
3 basic definitions (39 messages, latest: Sep 04 2025 at 13:30)
#27288 semilinearizing some of TensorProduct/Basic (1 message, latest: Sep 03 2025 at 17:01)
#29162 generalize Schroeder-Bernstein theorem (2 messages, latest: Sep 03 2025 at 06:39)
#28469 WithLp equivalences (16 messages, latest: Sep 02 2025 at 20:14)
#24532 fill out the `FreeProduct.asPowers namespace (2 messages, latest: Sep 02 2025 at 06:25)
#28533 linarith? (1 message, latest: Sep 02 2025 at 03:06)
#29114 Mean value theorem for integrals (1 message, latest: Sep 01 2025 at 09:03)
Basic lemmas for ContMDiff (3 messages, latest: Sep 01 2025 at 08:57)
#28284 finite product of probability measures (1 message, latest: Aug 31 2025 at 20:41)
#26790 define standard Bell number (2 messages, latest: Aug 31 2025 at 12:53)
#28191 tag Injective, Surjective, and Bijective with fun_pro (21 messages, latest: Aug 29 2025 at 06:13)
#26530, #26529, #26527 location of touchpoints of a simplex (6 messages, latest: Aug 28 2025 at 21:33)
#29065: make Coverage and Pretopology extend Precoverage (2 messages, latest: Aug 28 2025 at 17:31)
#29060 refactored: move argument s to last in LSeries_congr (2 messages, latest: Aug 28 2025 at 15:54)
#28658 New field_simp (23 messages, latest: Aug 28 2025 at 09:30)
#23594 chore: rename dmaSMul_apply to domSMul_apply (6 messages, latest: Aug 27 2025 at 14:59)
#28818 Setoid.ker_lift (13 messages, latest: Aug 26 2025 at 07:44)
#24050 generalise pointwise scalar multiplication of finsupp (1 message, latest: Aug 23 2025 at 15:44)
#26838 lemmas about List.scanr (1 message, latest: Aug 23 2025 at 15:38)
#28451 & #28477 Using Oka predicates (2 messages, latest: Aug 22 2025 at 20:55)
#28710 MulEquivClass := MulHomClass (10 messages, latest: Aug 22 2025 at 00:32)
#26766 some additions related to IsBounded (2 messages, latest: Aug 21 2025 at 15:31)
#28661 doc(MeasureTheory): Miscellaneous typo fixes (1 message, latest: Aug 21 2025 at 07:56)
#28322 chore: remove a now-unneeded maxHeartbeats (2 messages, latest: Aug 21 2025 at 02:26)
#26804 ZFSet is a model of ZFC (9 messages, latest: Aug 20 2025 at 02:20)
#27321 Colimit can be computed fiberwise (2 messages, latest: Aug 19 2025 at 13:35)
#28180 clean up PiFin.mkLiteralQ (1 message, latest: Aug 19 2025 at 11:30)
#28317 more lemmas about units in ordered monoid (1 message, latest: Aug 19 2025 at 11:20)
#27562 Deduplicate some meta code (1 message, latest: Aug 18 2025 at 12:15)
#28148 Simproc for Matrix Transpose (250 messages, latest: Aug 18 2025 at 04:20)
card_Union_le_sum_card lemmas (7 messages, latest: Aug 16 2025 at 23:20)
#28498 Use the delta deriving handler (2 messages, latest: Aug 16 2025 at 07:02)
#28169 Monoid of ideals of a Dedekind domain is torsion-free (20 messages, latest: Aug 14 2025 at 19:52)
#19872 rename relindex to relIndex (15 messages, latest: Aug 13 2025 at 13:52)
#9915 norm_num for division in NNRat and NNReal (5 messages, latest: Aug 13 2025 at 07:59)
#28072 tactic for equivalent valuations (79 messages, latest: Aug 12 2025 at 21:01)
#27552 TypeVec.Arrow over varying universes (1 message, latest: Aug 11 2025 at 19:45)
#27200 oka condition (1 message, latest: Aug 08 2025 at 13:27)
Three small PR's to add Finsupp lemmas (2 messages, latest: Aug 05 2025 at 10:51)
#27852 add Teichmuller-Tukey lemma (2 messages, latest: Aug 02 2025 at 08:51)
#27076 don't require DecidablePred to state PrimrecPred (2 messages, latest: Aug 02 2025 at 00:10)
#25730 feat(ZLattice/Covolume): add covolume_div_covolume_eq (1 message, latest: Aug 01 2025 at 01:17)
#26928 lower set in well-order is open (1 message, latest: Jul 30 2025 at 21:53)
PRs from FLT (2 messages, latest: Jul 29 2025 at 15:57)
Filtered Algebra (11 messages, latest: Jul 28 2025 at 19:38)
Catching typos: a continuous thread (6 messages, latest: Jul 27 2025 at 14:49)
#27270 Turn WithLp into a one field structure (1 message, latest: Jul 26 2025 at 19:19)
#24311 replace Monoid.IsTorsionFree with IsMulTorsionFree (1 message, latest: Jul 26 2025 at 06:05)
Using enorm more in mathlib (9 messages, latest: Jul 25 2025 at 08:18)
Refactoring to use ValuativeRel instead of Valued (134 messages, latest: Jul 24 2025 at 20:46)
#27254 2025 IMO Problem 3 (1 message, latest: Jul 24 2025 at 16:09)
#27292 Asymptotic cone of a set (5 messages, latest: Jul 20 2025 at 20:02)
#27215 site on CommRingCatᵒᵖ (1 message, latest: Jul 19 2025 at 11:48)
#26290 Define Stirling Numbers (10 messages, latest: Jul 19 2025 at 08:24)
Riemannian manifolds (58 messages, latest: Jul 18 2025 at 20:31)
#25833 topologist's sine curve (3 messages, latest: Jul 18 2025 at 17:54)
#26659 algebraize tactic fix & feats (4 messages, latest: Jul 18 2025 at 10:41)
#24351 Derivatives of powers (3 messages, latest: Jul 18 2025 at 08:37)
#26070 instances on Dedekind domains (1 message, latest: Jul 15 2025 at 10:36)
✔ #26976 Concept lattice renames (95 messages, latest: Jul 11 2025 at 20:37)
#26923 The pointwise ergodic theorem (Birkhoff's) (11 messages, latest: Jul 11 2025 at 17:46)
#25961 Improve SetLike ruleset (1 message, latest: Jul 08 2025 at 19:04)
#22782 Etale space (2 messages, latest: Jul 08 2025 at 16:11)
multicoequalizers in Type (6 messages, latest: Jul 07 2025 at 12:43)
#24131 - Primitive subgroups of the permutation group (16 messages, latest: Jul 07 2025 at 07:42)
Fix broken links in docs #8785 (1 message, latest: Jul 05 2025 at 20:06)
#26770 Multigraph Subgraph relation (1 message, latest: Jul 04 2025 at 21:57)
#26718 commandStart linter and : (3 messages, latest: Jul 04 2025 at 11:05)
#26170 Add an equivalence for Equiv.symm. (1 message, latest: Jul 03 2025 at 12:51)
#26220 Remove Equiv explict FunLike instance. (2 messages, latest: Jul 03 2025 at 12:49)
#25304 Joint differentiability from partial derivatives (12 messages, latest: Jul 01 2025 at 17:20)
✔ #26400 pigeonhole-like results for Fin (2 messages, latest: Jul 01 2025 at 12:26)
von Neumann hierarchy: #26543 , #26518 (59 messages, latest: Jun 30 2025 at 21:36)
#17027 , #26518 von Neumann hierarchy (1 message, latest: Jun 30 2025 at 14:48)
#23986 (2 messages, latest: Jun 30 2025 at 06:56)
#26392 maintainer-merge (12 messages, latest: Jun 30 2025 at 02:27)
#26427 any cyclotomic extension is abelian (2 messages, latest: Jun 29 2025 at 06:10)
#7300 synthetic geometry (61 messages, latest: Jun 28 2025 at 09:24)
#26436 - Fuel Nat.minFac (12 messages, latest: Jun 28 2025 at 05:24)
#22018 (2 messages, latest: Jun 26 2025 at 20:20)
#25935 incenter, touchpoints and tangency (1 message, latest: Jun 25 2025 at 22:59)
#26408 Equivalence between Nat and Nat + its first n element (1 message, latest: Jun 25 2025 at 15:58)
#26285 Resultant of two polynomials (72 messages, latest: Jun 25 2025 at 13:31)
#26277 - Basic isomorphism theorems for ring congruences (3 messages, latest: Jun 25 2025 at 08:31)
#25491 Freer Monad (4 messages, latest: Jun 24 2025 at 17:14)
#26297 (2 messages, latest: Jun 24 2025 at 16:36)
#26060 Grassmannians (6 messages, latest: Jun 24 2025 at 12:31)
#18629 runtime complexity of sorting a list (35 messages, latest: Jun 23 2025 at 14:32)
#21560 Definition of sublocales (11 messages, latest: Jun 23 2025 at 12:46)
#26203 IsPrime.one_notMem (1 message, latest: Jun 22 2025 at 23:54)
#26061 define Projective Space (4 messages, latest: Jun 21 2025 at 19:39)
#25728 PIR => Krull dim LE one without domain condition (1 message, latest: Jun 21 2025 at 07:26)
Hausdorff–Alexandroff theorem (11 messages, latest: Jun 20 2025 at 07:37)
Test for emoji reactions #25950 (2 messages, latest: Jun 18 2025 at 23:27)
#24578 cardinality of product set (+54/-16) (1 message, latest: Jun 18 2025 at 18:51)
#23678 recursor for nonempty lists (1 message, latest: Jun 17 2025 at 19:37)
#23926 & #24336 finsum_mem lemmas (5 messages, latest: Jun 16 2025 at 15:48)
#25168 LinearOrder on HahnSeries (4 messages, latest: Jun 13 2025 at 18:18)
#24931 (n + 1).sqrt is not greater than n (19 messages, latest: Jun 12 2025 at 16:32)
#23752 incenters and excenters (3 messages, latest: Jun 12 2025 at 11:48)
#20676 unbundling ordered algebra (111 messages, latest: Jun 12 2025 at 04:40)
Mysterious CI error in "verify that everything was availa… (3 messages, latest: Jun 10 2025 at 19:34)
#22834 lifting properties and parametrized adjunctions (1 message, latest: Jun 10 2025 at 05:56)
#25253 add AlgHom.natCard_of_splits (2 messages, latest: Jun 09 2025 at 21:38)
#25558 split Mathlib/Topology/Algebra/RestrictedProduct (11 messages, latest: Jun 07 2025 at 22:20)
#24982 refactor definition of mates (1 message, latest: Jun 07 2025 at 09:58)
#24540 various quiver shapes (5 messages, latest: Jun 06 2025 at 22:58)
#23969 feat: add LinearEquiv.ofInjectiveOfFinrankEq (1 message, latest: Jun 06 2025 at 07:48)
#25449 maintainer merge emoji reaction (1 message, latest: Jun 04 2025 at 19:07)
#25050 - Adding Vector and List.Vector equivalence (17 messages, latest: Jun 04 2025 at 13:55)
#25264 Fairly elementary monoid lifts. (5 messages, latest: Jun 04 2025 at 12:41)
#24735: define tensorLeft/Right as abbrev for curriedTensor (3 messages, latest: Jun 03 2025 at 16:25)
#24669 Defining LinearIsometryEquiv for commuting products (1 message, latest: Jun 02 2025 at 06:29)
#24792 Matrix.vec (2 messages, latest: Jun 02 2025 at 00:36)
#25218 Tate normal form of elliptic curves (1 message, latest: Jun 01 2025 at 13:04)
#14752 - Repair the topology of valued fields (8 messages, latest: Jun 01 2025 at 11:24)
#25087 algebra isomorphisms induced by Weierstrass division (1 message, latest: Jun 01 2025 at 07:40)
#24303 Reassoc for isomorphisms (2 messages, latest: May 27 2025 at 17:31)
Boring linear algebra results: #25166, #25169, #25142 (1 message, latest: May 25 2025 at 12:16)
#24690 Reverse lexicographic order (4 messages, latest: May 24 2025 at 14:44)
#22653 Bors failure (2 messages, latest: May 24 2025 at 08:09)
lean-pr-testing-7352 (3 messages, latest: May 21 2025 at 23:26)
#24295 AffineSubspace.subtypeA (2 messages, latest: May 21 2025 at 19:16)
#24991 Day convolution of functors (9 messages, latest: May 19 2025 at 04:43)
#24960 PermOf implements more-efficient finite permutations. (2 messages, latest: May 16 2025 at 14:58)
#23974 Change file name to CamelCase (28 messages, latest: May 16 2025 at 12:57)
#22884 Turing Degrees (1 message, latest: May 15 2025 at 15:03)
#24122 Multigraphs (45 messages, latest: May 14 2025 at 18:54)
#24149 reorder, streamline convex cones (17 messages, latest: May 14 2025 at 11:47)
#24897 replicate the Algebra subfolders design in Order (1 message, latest: May 14 2025 at 10:41)
#23507 SummableUniformlyOn (4 messages, latest: May 13 2025 at 13:53)
#24660 Use Classical or Decidable in definition (74 messages, latest: May 12 2025 at 15:14)
#22957 row and column functions of matrices (12 messages, latest: May 10 2025 at 15:27)
#24321 + #24667: adjoint triples & quadruples (9 messages, latest: May 09 2025 at 23:54)
#24719 cannot find home (4 messages, latest: May 09 2025 at 15:54)
#24556 Testing the new emojibot label (26 messages, latest: May 08 2025 at 13:27)
Add "closed-pr" emoji in Zulip? (42 messages, latest: May 07 2025 at 09:21)
Local diffeomorphism PRs (3 messages, latest: May 06 2025 at 15:14)
#24452 + #24454 + #24506: rotate_isos tactic (13 messages, latest: May 06 2025 at 13:55)
#23951 matroid rank API (2 messages, latest: May 05 2025 at 07:03)
#24178 Which order to sort eigenvalues? (9 messages, latest: May 03 2025 at 17:26)
#24127 PR not on the review queue (11 messages, latest: May 02 2025 at 21:39)
#24465 maintainer merged PRs (7 messages, latest: May 02 2025 at 14:35)
#24538 homOfEq lemmas (3 messages, latest: May 02 2025 at 11:55)
#22337 type class generalization (104 messages, latest: Apr 30 2025 at 12:37)
#22196 lie_ring tactic (12 messages, latest: Apr 30 2025 at 06:52)
#24441 theorem on list commutativity (1 message, latest: Apr 28 2025 at 18:58)
#22361 NFA closure properties (5 messages, latest: Apr 27 2025 at 13:22)
#24369 modify the class IsQuadraticExtension (1 message, latest: Apr 25 2025 at 15:37)
#23715 make orthogonalProjection a continuous affine map (4 messages, latest: Apr 23 2025 at 17:59)
#20230 categories of homological complexes are Grothendieck (2 messages, latest: Apr 23 2025 at 15:24)
#22574 redefine full subcategories using ObjectProperty (3 messages, latest: Apr 23 2025 at 10:32)
#22355 Some lemmas about RingQuot.mkRingHom (22 messages, latest: Apr 23 2025 at 06:19)
#19668 define ≤/< on WithBot/WithTop by induction (12 messages, latest: Apr 18 2025 at 23:13)
#24182 Remove IntermediateField.instCoeOutSubtypeMem (1 message, latest: Apr 18 2025 at 20:01)
#19920 More differential geometry documentation (7 messages, latest: Apr 18 2025 at 19:12)
#24139 Fin.cycleIcc (4 messages, latest: Apr 17 2025 at 14:07)
#24125 clean up WithVal (1 message, latest: Apr 16 2025 at 19:27)
#22929 characterise covering in Pi types (1 message, latest: Apr 16 2025 at 19:16)
equivalence of stabilizers (2 messages, latest: Apr 16 2025 at 07:44)
✔ #17980 Functoriality of the Grothendieck construction (11 messages, latest: Apr 15 2025 at 18:39)
#23637 Circuit contains a cycle (1 message, latest: Apr 15 2025 at 13:29)
#23503 ENat and tsum (105 messages, latest: Apr 13 2025 at 16:22)
Categorical structure of Quiv (5 messages, latest: Apr 13 2025 at 08:58)
SubMulAction (3 messages, latest: Apr 12 2025 at 11:20)
#23948 - Eisenstein Criterion (1 message, latest: Apr 11 2025 at 15:08)
#23946 edge sets of walks (1 message, latest: Apr 11 2025 at 11:31)
Thread for failed staging PRs (43 messages, latest: Apr 11 2025 at 02:35)
#23866 and #23867, removing most \[Nat.AtLeastTwo n\] (71 messages, latest: Apr 11 2025 at 02:16)
#23065 eval_of_algHom (1 message, latest: Apr 10 2025 at 14:08)
#23124 nets (1 message, latest: Apr 10 2025 at 13:21)
#18396 the Lie algebra of a real or complex Lie group (53 messages, latest: Apr 10 2025 at 08:32)
#23892 Drop ZeroLeOneClass assumption in some lemmas (4 messages, latest: Apr 10 2025 at 08:16)
#23884 Loopless matroids (1 message, latest: Apr 09 2025 at 17:47)
#23873 Minors of matroids (1 message, latest: Apr 09 2025 at 16:14)
#21903 FreeSemigroup and List with relative theorems (4 messages, latest: Apr 08 2025 at 07:55)
#23798 strict inclusion of unbounded intervals (1 message, latest: Apr 08 2025 at 04:44)
#22314 leftmost derivations for context-free grammars (3 messages, latest: Apr 07 2025 at 07:17)
#21603 Basic ChosenFiniteCoproducts class (3 messages, latest: Apr 07 2025 at 05:54)
#20681 define deleteIncidenceSet (Combinatorics/SimpleGraph) (3 messages, latest: Apr 07 2025 at 01:55)
#20495 Combinatorial Nullstellensatz (3 messages, latest: Apr 07 2025 at 01:53)
#23710 - A generalized Eisenstein criterion (2 messages, latest: Apr 07 2025 at 01:52)
#21488 Premonoidal categories (4 messages, latest: Apr 07 2025 at 01:51)
#20680 weak factorisation systems (2 messages, latest: Apr 05 2025 at 22:04)
#23645 (1 message, latest: Apr 05 2025 at 01:36)
#22127 Module length is additive in short exact sequences (5 messages, latest: Apr 04 2025 at 14:38)
#23557 matroid contraction (3 messages, latest: Apr 04 2025 at 11:19)
✔ #11521 speeding up lots of instances (108 messages, latest: Apr 03 2025 at 16:40)
#21238 lake exe cache (12 messages, latest: Apr 02 2025 at 10:04)
#21080 continuous functions on profinites (4 messages, latest: Apr 02 2025 at 09:54)
#22503 Rewriting Multiplicity in Factorization (3 messages, latest: Apr 02 2025 at 06:56)
#18397 rename RestrictGenTopology to IsRestrictGen (15 messages, latest: Mar 31 2025 at 13:56)
#23086 lemmas about periodicPts on Fintype (2 messages, latest: Mar 31 2025 at 08:49)
#23454 ENat lemmas about mul/iInf/iSup (1 message, latest: Mar 30 2025 at 17:01)
Frobenius map now in Mathlib.Algebra.CharP.Frobenius (1 message, latest: Mar 29 2025 at 18:44)
Rings with multiplicative norm (8 messages, latest: Mar 29 2025 at 01:23)
#23377 Matroid ENat-valued rank (5 messages, latest: Mar 27 2025 at 18:27)
#23373 Matroid coloops (1 message, latest: Mar 27 2025 at 15:18)
#23209 add improper integral of complex exp (2 messages, latest: Mar 27 2025 at 15:10)
#21944 Weierstrass preparation for complete local ring (32 messages, latest: Mar 27 2025 at 07:03)
#22964 Sum.elim lemmas in Data/Set/Image (3 messages, latest: Mar 26 2025 at 17:49)
Rewriting Python style linters in Lean (46 messages, latest: Mar 25 2025 at 21:31)
Ackermann function is computable #22457 (5 messages, latest: Mar 25 2025 at 05:21)
#23276 Matroid minors (1 message, latest: Mar 24 2025 at 19:28)
#23196 docstrings for Nat.factorial and Nat.choose (1 message, latest: Mar 21 2025 at 15:53)
#23150 Matrix row/column rename (1 message, latest: Mar 20 2025 at 23:51)
#23157 matroid nonloops (1 message, latest: Mar 20 2025 at 17:30)
#22253 set difference lemmas (1 message, latest: Mar 20 2025 at 15:36)
#22533 deprime induction' in root files (8 messages, latest: Mar 19 2025 at 02:52)
#22365 hint tactics (27 messages, latest: Mar 18 2025 at 16:35)
#23053, merging admit linter into deprecated syntax linter (1 message, latest: Mar 18 2025 at 16:32)
Eliminating cases' (for real) (17 messages, latest: Mar 17 2025 at 23:45)
#22226 Infinite matrix rank (29 messages, latest: Mar 17 2025 at 16:25)
#22366 check_equalities tactic for defeq problems (5 messages, latest: Mar 17 2025 at 03:06)
#22976 Refactoring CategoryTheory.Sums (3 messages, latest: Mar 17 2025 at 02:58)
#22631 define associated graded structure for abelian group (2 messages, latest: Mar 16 2025 at 02:44)
#22948 Definition about morphism of directsum decomposition (9 messages, latest: Mar 16 2025 at 01:39)
#22614 CanonAtomM (23 messages, latest: Mar 15 2025 at 14:45)
#22587 chore(Algebra/Group/Basic): rename mul_right_eq_self (3 messages, latest: Mar 14 2025 at 07:06)
#22892 hint looks for error messages (3 messages, latest: Mar 14 2025 at 00:14)
#21090 refactor(AlgebraicTopology): use the Subpresheaf API (5 messages, latest: Mar 13 2025 at 10:11)
PR #22018 localization of a finite direct product (1 message, latest: Mar 12 2025 at 13:52)
#22851 More LinearIndepOn (4 messages, latest: Mar 12 2025 at 13:26)
#20488 various lemmas about lists (8 messages, latest: Mar 11 2025 at 09:14)
#22312 Intrinsic Interior, Closure, and Related Properties (33 messages, latest: Mar 11 2025 at 07:53)
#21078 WeakBilin eval map (4 messages, latest: Mar 10 2025 at 23:20)
#21585 lemmas about nonterminals (3 messages, latest: Mar 10 2025 at 23:20)
#22780 scoping a few instances with weak keys (14 messages, latest: Mar 10 2025 at 20:42)
lean4#7356 monadic theorems about mapM, foldM, etc (1 message, latest: Mar 10 2025 at 08:42)
"Add closed-pr emoji in Zulip" failed (32 messages, latest: Mar 09 2025 at 19:30)
#22678 - bilinearCombination (1 message, latest: Mar 07 2025 at 10:56)
#22527 ofSetSetoid (1 message, latest: Mar 07 2025 at 09:41)
#22377 Vandermonde matrices with exceptional rows (16 messages, latest: Mar 05 2025 at 18:45)
#22230 chore(Algebra/Group):add coercion for subgroup class (1 message, latest: Mar 03 2025 at 07:36)
#11968 improvements to RefinedDiscrTree (11 messages, latest: Mar 01 2025 at 00:39)
#21571 normalized trace (1 message, latest: Feb 28 2025 at 23:25)
#11563 ∑ i ∈ s with hi : p i, f i hi syntax (3 messages, latest: Feb 28 2025 at 13:28)
#21442 define open covers (6 messages, latest: Feb 28 2025 at 12:57)
#21341 quotients of multiplicative normed groups (1 message, latest: Feb 28 2025 at 11:46)
#22368 more linearIndepOn api (2 messages, latest: Feb 27 2025 at 16:26)
#20744 the minimum cardinality of generating set (17 messages, latest: Feb 26 2025 at 10:14)
#20688 truncated simplicial notations (3 messages, latest: Feb 24 2025 at 18:42)
#22208 feat(Algebra):filtered ring hom (1 message, latest: Feb 24 2025 at 10:15)
#16733 Nonarchimedean locally compact iff complete and DVR (1 message, latest: Feb 24 2025 at 03:12)
#22105 Discrete spaces are 0-dimensional manifolds (4 messages, latest: Feb 23 2025 at 21:08)
#22225 move Polynomial.coeffs (1 message, latest: Feb 23 2025 at 20:33)
#21886 LinearIndepOn refactor (14 messages, latest: Feb 23 2025 at 17:30)
#22186 some encard lemmas (1 message, latest: Feb 22 2025 at 18:24)
#22097 dot notation for disjointness (1 message, latest: Feb 19 2025 at 19:02)
#12259 more apply (26 messages, latest: Feb 19 2025 at 02:58)
#22045 Matroid loops (1 message, latest: Feb 18 2025 at 16:32)
#22031 maybe adds emoji to first message (4 messages, latest: Feb 18 2025 at 09:10)
#21995 deprecate Complex.abs (7 messages, latest: Feb 18 2025 at 07:20)
#19580 incomparable relation (1 message, latest: Feb 18 2025 at 05:38)
#20502 generalize IsLUB.mem_of_not_isSuccPrelimit (15 messages, latest: Feb 17 2025 at 09:16)
#18547 ordinals are uncountable (1 message, latest: Feb 17 2025 at 06:22)
simplify lakefile post_update hook #21650 (1 message, latest: Feb 16 2025 at 22:14)
#21768 deprime induction'/cases' in Topology (7 messages, latest: Feb 15 2025 at 12:53)
#20686 CompletableTopField instance for NormedField (21 messages, latest: Feb 15 2025 at 10:46)
#21021 Chevalley’s theorem (1 message, latest: Feb 14 2025 at 21:45)
#21879 Add 'Is' to matroid predicate names (1 message, latest: Feb 14 2025 at 17:07)
#21799 LinearIndependentOn (1 message, latest: Feb 13 2025 at 11:50)
#21772 clearing (some of) docBlame (2 messages, latest: Feb 12 2025 at 07:08)
#21741 -> #21748: presentation of SimplexCategory (1 message, latest: Feb 11 2025 at 21:53)
feat: erw?, a tool to explain why erw is necessary #21643 (14 messages, latest: Feb 11 2025 at 16:28)
#21694 Finite-rank sets in matroids (1 message, latest: Feb 10 2025 at 23:36)
#21692 Matroid cocircuits (1 message, latest: Feb 10 2025 at 23:33)
#20642 extend API for WithAbs (1 message, latest: Feb 10 2025 at 20:08)
#17129 add unicode linter for unicode variant-selectors (5 messages, latest: Feb 10 2025 at 10:22)
#20988 multiequalizer refactor (category theory) (1 message, latest: Feb 10 2025 at 09:19)
#21582 More APIs for IsAdicComplete (5 messages, latest: Feb 10 2025 at 03:39)
#21563 the untilt map (1 message, latest: Feb 09 2025 at 17:40)
#21180 IndepMatroid docstring (1 message, latest: Feb 09 2025 at 17:06)
#21605 Rk -> Rank in instance names (3 messages, latest: Feb 09 2025 at 16:45)
#17908 Hopkins–Levitzki theorem (18 messages, latest: Feb 08 2025 at 17:53)
#21525 Locally Cartesian Closed Categories (7 messages, latest: Feb 07 2025 at 14:28)
#21372 Exponent for (purely inseparable) field extensions (6 messages, latest: Feb 07 2025 at 08:54)
#21527 add reassoc tag to terminal.comp_from (1 message, latest: Feb 07 2025 at 02:17)
#21520 Linear independence and sets of indices (1 message, latest: Feb 06 2025 at 19:25)
#21296 don't import Ring in GroupTheory.Commutator.Basic (37 messages, latest: Feb 06 2025 at 16:55)
#21454 Protect some results about Complex.abs (11 messages, latest: Feb 06 2025 at 16:52)
#21511 Trivial linear independence lemmas (1 message, latest: Feb 06 2025 at 16:48)
#21097 SetLike instance for equivalence classes (35 messages, latest: Feb 06 2025 at 15:39)
#21428 Set partitions (6 messages, latest: Feb 05 2025 at 21:22)
#21172 Circuit elimination and finitary matroids (2 messages, latest: Feb 05 2025 at 14:08)
#21322 insertion and iUnion (2 messages, latest: Feb 04 2025 at 14:35)
#17930 introduce Ideal.IsTwoSided class (11 messages, latest: Feb 04 2025 at 08:32)
#17580 lint declarations which contain a double underscore (17 messages, latest: Feb 04 2025 at 00:38)
#21383 iff versions of scaling and linear independence (1 message, latest: Feb 03 2025 at 22:28)
#21357 check_compositions (8 messages, latest: Feb 03 2025 at 10:26)
#20225 - tidy various files (4 messages, latest: Feb 02 2025 at 20:44)
#21168 IsLocalRing for sub(semi)rings (3 messages, latest: Jan 31 2025 at 20:45)
✔ #21199 IsUnit x ↔ x ∈ A⁰ in algebras over artinian rings (3 messages, latest: Jan 31 2025 at 19:11)
#20748 don't import MonoidWithZero in submonoids (10 messages, latest: Jan 31 2025 at 12:16)
#19946 ZFC order instances (4 messages, latest: Jan 31 2025 at 01:36)
Open PR on group theory (14 messages, latest: Jan 30 2025 at 13:22)
#21240 Fixed junk values for fundamental circuits. (6 messages, latest: Jan 30 2025 at 13:12)
#20658 define SubgraphIso (8 messages, latest: Jan 29 2025 at 19:56)
✔ #21191 IsIntegral and (cartesian) product (3 messages, latest: Jan 29 2025 at 12:50)
#21005 style PR on Games (5 messages, latest: Jan 29 2025 at 07:45)
✔ #21062 Polynomial.aeval for product algebras (5 messages, latest: Jan 28 2025 at 12:06)
lean4#6269 warnings for declaration/export conflicts (20 messages, latest: Jan 28 2025 at 10:38)
#21099 use unification hints for generators (36 messages, latest: Jan 28 2025 at 00:59)
#21145 (1 message, latest: Jan 27 2025 at 21:31)
#19571 AntisymmRel lemmas (3 messages, latest: Jan 27 2025 at 01:06)
#16936 equidecomposition (7 messages, latest: Jan 26 2025 at 23:45)
✔ #21019 artinian local reduced ring is a field (6 messages, latest: Jan 25 2025 at 21:01)
#20182 Distributive Categories (6 messages, latest: Jan 25 2025 at 09:56)
#20885 Matroid closure lemmas (2 messages, latest: Jan 25 2025 at 06:15)
#16991 ContinuousMulEquiv (11 messages, latest: Jan 24 2025 at 21:55)
#20745 don't import MonoidWithZero for results about MonoidH (7 messages, latest: Jan 24 2025 at 16:20)
#20538 still maintainer-merge (1 message, latest: Jan 23 2025 at 23:09)
#20721 Equivs involving center and Module.End (1 message, latest: Jan 23 2025 at 18:08)
#20886 Instances for basic matroids (1 message, latest: Jan 23 2025 at 17:53)
Truncation of (multivariate) power series (7 messages, latest: Jan 23 2025 at 16:54)
#20995 Matroid circuits (1 message, latest: Jan 23 2025 at 16:49)
#20977: more on additive contents (4 messages, latest: Jan 23 2025 at 11:53)
#7162 refactor: separate out PGame.relabelling (26 messages, latest: Jan 23 2025 at 09:58)
#16993 Galois Group is Profinite (14 messages, latest: Jan 23 2025 at 05:40)
#19393 Up and down games (6 messages, latest: Jan 23 2025 at 04:37)
Azumaya algebras #20489 (6 messages, latest: Jan 22 2025 at 07:03)
#20828 MaximalSpectrum R instead of {I \| I.IsMaximal} (45 messages, latest: Jan 21 2025 at 18:05)
#20921 Cardinality-valued matroid rank (1 message, latest: Jan 21 2025 at 17:34)
#17325 feat(Data/Nat): faster computation of Nat.log (2 messages, latest: Jan 21 2025 at 15:17)
#20888 Finitary matroid bases are equicardinal (1 message, latest: Jan 21 2025 at 01:10)
#10186 Defining Greedoid (5 messages, latest: Jan 21 2025 at 01:07)
#19838 #20876 #20877 Matroid housekeeping (5 messages, latest: Jan 20 2025 at 16:50)
✔ #5901 feat: more PGame.identical PGame.memₗ PGame.memᵣ … (2 messages, latest: Jan 20 2025 at 04:59)
#14990 Linear topologies (3 messages, latest: Jan 17 2025 at 10:17)
#16992 Profinite Group is limit of finite groups (12 messages, latest: Jan 17 2025 at 09:32)
#20794 RingEquiv.piUnique (3 messages, latest: Jan 17 2025 at 08:59)
#20772 split off definition of ring spectra (3 messages, latest: Jan 16 2025 at 10:18)
#20488 setOf_mem_list_eq_singleton_of_nodup (7 messages, latest: Jan 16 2025 at 00:20)
#20491 generalize SuccOrder theorems (1 message, latest: Jan 16 2025 at 00:19)
#19973 ¬a < b ↔ ¬a ≤ b ∨ b ≤ a (1 message, latest: Jan 15 2025 at 23:46)
#19115 Generalize flatness to semirings (6 messages, latest: Jan 15 2025 at 14:49)
#19802 deprecate Ordinal.IsLimit (1 message, latest: Jan 14 2025 at 15:13)
#17538 automatically add dependency-bump (2 messages, latest: Jan 13 2025 at 14:13)
#15891 Boundary points of a real interval (6 messages, latest: Jan 12 2025 at 22:45)
#17522 feat: study the centralizer of a permutation (3 messages, latest: Jan 12 2025 at 16:17)
Maximal subgroups #20499 (12 messages, latest: Jan 10 2025 at 15:01)
#19514 Congruence between subtypes and sets/finsets (13 messages, latest: Jan 08 2025 at 05:16)
#18818 Traversable Tree instance (1 message, latest: Jan 07 2025 at 09:55)
#16797 Liouville / differential field theory (7 messages, latest: Jan 06 2025 at 11:20)
#19970 ⨆ a < x, succ a = x (1 message, latest: Jan 04 2025 at 20:59)
#20282 feat(Topology/Group): Lemmas about profinite group (1 message, latest: Jan 04 2025 at 15:50)
#20364 fix NatTrans.CommShift (1 message, latest: Jan 03 2025 at 09:52)
#18461 left and right common multiples mixins (9 messages, latest: Jan 03 2025 at 06:33)
#20371 sort_antisymmetry and sort_embedding (11 messages, latest: Jan 03 2025 at 05:14)
L-series (81 messages, latest: Dec 31 2024 at 21:49)
#20330 (3 messages, latest: Dec 30 2024 at 21:50)
#20331: rename Nat.lt_div_iff_mul_lt (1 message, latest: Dec 29 2024 at 20:44)
#20136 rename iteratedDeriv_const_{smul,mul} (1 message, latest: Dec 28 2024 at 10:07)
✔ metaprobook needs update!! (2 messages, latest: Dec 25 2024 at 10:46)
#19163 bounding the coefficients of modByMonic/divByMonic (2 messages, latest: Dec 19 2024 at 10:57)
#17554 -> #17779 + #17781: sifted categories (RFC!) (10 messages, latest: Dec 19 2024 at 10:55)
#17758 Ordinal.toENat (57 messages, latest: Dec 16 2024 at 01:12)
#16688 Fix two PATH resolution issues (3 messages, latest: Dec 15 2024 at 22:11)
#19977 ChosenFiniteProducts for affine schemes (2 messages, latest: Dec 15 2024 at 17:20)
#16769 add Walk.penultimate and Walk.snd (1 message, latest: Dec 13 2024 at 13:31)
#19237: address porting notes (1 message, latest: Dec 12 2024 at 14:41)
#18778: omega ordinals are principal (1 message, latest: Dec 12 2024 at 14:37)
#16865: Laurent series are complete (31 messages, latest: Dec 12 2024 at 05:58)
#16344 induction principle for FreeProduct (22 messages, latest: Dec 12 2024 at 04:07)
#19757 Algebra/Category/Ring: make morphisms a structure (3 messages, latest: Dec 11 2024 at 22:18)
#19755 test an executable with import Mathlib (2 messages, latest: Dec 11 2024 at 14:04)
#14987 Relative rank of intermediate fields (32 messages, latest: Dec 08 2024 at 07:23)
✔ #12405 (8 messages, latest: Dec 04 2024 at 20:57)
Integrate analytic functions in the smooth hierarchy (75 messages, latest: Dec 04 2024 at 06:28)
#19042 localization of a direct product injects (2 messages, latest: Dec 03 2024 at 22:39)
#18689 feat(Topology): Introduce HomeomorphClass (2 messages, latest: Dec 03 2024 at 08:55)
#18611 Veblen hierarchy (3 messages, latest: Dec 03 2024 at 07:14)
#19068 Dini's theorem (1 message, latest: Dec 02 2024 at 10:37)
#19435 an equality condition for AM-GM inequality (9 messages, latest: Nov 30 2024 at 13:31)
#19522: emoji reactions to all public channels (128 messages, latest: Nov 30 2024 at 08:41)
#18239 cleanup of ZFC rank (3 messages, latest: Nov 27 2024 at 22:25)
#18990 sup-closed sets are closed under finite suprema (5 messages, latest: Nov 27 2024 at 22:20)
#19060 IsSuccLimit theorems for SuccAddOrder (2 messages, latest: Nov 27 2024 at 19:30)
#19236 natural addition without blsub (2 messages, latest: Nov 27 2024 at 19:28)
#19425: gcongr forward-reasoning (1 message, latest: Nov 27 2024 at 17:34)
Prerequisites for PNT and Dirichlet's Thm (71 messages, latest: Nov 27 2024 at 10:24)
#17087 Add results about EReal (4 messages, latest: Nov 27 2024 at 08:03)
Testing new emoji system using #18679 as a guinea PR (3 messages, latest: Nov 26 2024 at 00:40)
#19447 change the definition of List.finRange (4 messages, latest: Nov 25 2024 at 06:09)
#18235 typeLT notation (20 messages, latest: Nov 23 2024 at 19:58)
#19181 cleanup of many set_option deprecated.linter false (2 messages, latest: Nov 23 2024 at 07:32)
#19367 (5 messages, latest: Nov 22 2024 at 11:48)
HolomorphicOn and HolomorphicAt (30 messages, latest: Nov 21 2024 at 14:49)
#19119 atom representatives for ring and abel (18 messages, latest: Nov 18 2024 at 20:59)
#19082 linear_combination error message (1 message, latest: Nov 18 2024 at 15:00)
#18967 has incomplete deprecations (18 messages, latest: Nov 18 2024 at 09:36)
#18463 type of fundamental sequences (1 message, latest: Nov 17 2024 at 07:38)
#19080 Theorems about LocalizedModule (5 messages, latest: Nov 16 2024 at 09:40)
✔ #16877 Nimber multiplication (8 messages, latest: Nov 15 2024 at 01:48)
#19042 Ring Theory (3 messages, latest: Nov 14 2024 at 20:11)
#16311 regular languages are context-free (3 messages, latest: Nov 14 2024 at 10:06)
#16792 lifting a derivation via an algebra homomorphism (7 messages, latest: Nov 13 2024 at 15:38)
#18947 bump Mathlib for batteries#1029 (1 message, latest: Nov 13 2024 at 03:19)
#16105 add Stacks Project tags in Chapter 09FA Fields (5 messages, latest: Nov 12 2024 at 05:53)
#18043 deprecate StrictOrder.cof (1 message, latest: Nov 12 2024 at 01:58)
#18667, #18823 Goursat's lemma (4 messages, latest: Nov 10 2024 at 20:21)
#18032 quasi-compact + specializing <=> closed map (1 message, latest: Nov 10 2024 at 03:28)
Orthogonality of Dirichlet characters (17 messages, latest: Nov 08 2024 at 21:23)
#18065 periodic holomorphic functions (1 message, latest: Nov 08 2024 at 16:11)
#18689 feat(Topology): Introduce HomeomorphClass (8 messages, latest: Nov 08 2024 at 13:15)
Transcendental and algebraically independent (13 messages, latest: Nov 07 2024 at 08:32)
#18709 select correct lean4checker version (1 message, latest: Nov 06 2024 at 23:43)
#16991 feat(Topology/Group): Continuous isomorphism (3 messages, latest: Nov 06 2024 at 11:29)
#14598 typeclasses for top/bot being additively absorbing… (7 messages, latest: Nov 05 2024 at 17:16)
✔ #18495 TU matrices (2 messages, latest: Nov 04 2024 at 16:00)
#18255 Underlying space of pullback (3 messages, latest: Nov 04 2024 at 15:15)
#18516: refactor roots of unity (6 messages, latest: Nov 04 2024 at 08:24)
#18491 removes @[simp] from Sum.forall and Sum.exists (18 messages, latest: Nov 04 2024 at 07:25)
#17549: Ring Theory (10 messages, latest: Oct 31 2024 at 19:12)
#18335 Mahler basis functions (1 message, latest: Oct 31 2024 at 14:30)
#16982 Fundamental Theorem of Infinite Galois Theory (13 messages, latest: Oct 31 2024 at 00:45)
#17942 avoid Coe.coe in Data.Multiset.Functor (1 message, latest: Oct 30 2024 at 22:15)
#17674 simpler definition of Cardinal.aleph (2 messages, latest: Oct 30 2024 at 07:46)
#17751 generalize nfpFamily universes (3 messages, latest: Oct 30 2024 at 02:40)
#18346 Final iso between K⸨X⸩ and X-adic completion of K(X) (2 messages, latest: Oct 29 2024 at 16:07)
#18034 finiteness tactic (3 messages, latest: Oct 28 2024 at 07:35)
#17544 p-adic valuation of casts (1 message, latest: Oct 27 2024 at 14:35)
#17037 trivialities about Nat.primeCounting and Finsets (2 messages, latest: Oct 27 2024 at 13:15)
#17097 Measurability of add and mul on EReal (1 message, latest: Oct 27 2024 at 01:55)
#17881 MultilinearMap operations for Pi and DFinsupp (1 message, latest: Oct 25 2024 at 17:56)
#15793 Initial development of ordinals in ZFSet (3 messages, latest: Oct 25 2024 at 05:27)
18188 T2Space is Antitone: to golf or not to golf (3 messages, latest: Oct 24 2024 at 17:53)
#17602 fix InitialSeg simp lemmas (2 messages, latest: Oct 24 2024 at 17:29)
✔ #17483 more lemmas on characteristic two (3 messages, latest: Oct 24 2024 at 17:28)
✔ #16586 WellFounded.rank → IsWellFounded.rank (2 messages, latest: Oct 23 2024 at 20:25)
#18129 Spanning sets in matroids (1 message, latest: Oct 23 2024 at 15:30)
!3#16586 push_neg option (1 message, latest: Oct 22 2024 at 11:06)
✔ #17679 deprecate blsub₂ (2 messages, latest: Oct 22 2024 at 10:09)
#17960 API for separated morphisms (1 message, latest: Oct 22 2024 at 08:13)
#15897 chore: use Batteries test driver (4 messages, latest: Oct 21 2024 at 22:22)
#12339 the multi-goal linter (6 messages, latest: Oct 21 2024 at 01:30)
#17444 make CanonicallyOrdered* mixin (1 message, latest: Oct 19 2024 at 21:35)
#17945 Move infinite Galois (1 message, latest: Oct 19 2024 at 15:26)
#17599 Ordinal.typein tweaks (1 message, latest: Oct 19 2024 at 05:11)
#17901 reorganize ContinuousOn file (1 message, latest: Oct 18 2024 at 09:50)
#17859 feat: consistent family of kernels (7 messages, latest: Oct 17 2024 at 15:22)
#17276 feat(Algebra/Homology): study of the target of the… (1 message, latest: Oct 17 2024 at 13:55)
#17867 some results on Transcendental (1 message, latest: Oct 17 2024 at 13:06)
#16755 towards sheaf of differentials (1 message, latest: Oct 17 2024 at 09:42)
Discrete condensed objects #14027 #15321 #15566 #15569 (18 messages, latest: Oct 17 2024 at 08:10)
#15238 some results of extendScalars (6 messages, latest: Oct 17 2024 at 07:02)
#16409 doc: fix some issues under RepresentationTheory (1 message, latest: Oct 17 2024 at 06:57)
#14798 relations between trace maps and quotients (31 messages, latest: Oct 17 2024 at 06:39)
#15240 morphisms from Spec R for R local (3 messages, latest: Oct 16 2024 at 16:04)
#15093 Scheme.Hom refactor (1 message, latest: Oct 16 2024 at 07:53)
#16881 Multiplicity refactor (8 messages, latest: Oct 16 2024 at 06:55)
#8885 – fast powering in code generation (2 messages, latest: Oct 15 2024 at 20:39)
PRs from APAP (17 messages, latest: Oct 15 2024 at 16:25)
#17431 further properties of j-invariants (2 messages, latest: Oct 15 2024 at 15:40)
#17766 CartesianClosed refactor (1 message, latest: Oct 15 2024 at 11:00)
#16041 Ordinal.toNat (8 messages, latest: Oct 15 2024 at 04:50)
✔ #16283 rewrap and improve docs (2 messages, latest: Oct 15 2024 at 04:38)
#16818 Basic API for List.GroupBy (3 messages, latest: Oct 15 2024 at 03:00)
#17176 integrals/integrability with .re (7 messages, latest: Oct 14 2024 at 17:25)
#17718 bump batteries (3 messages, latest: Oct 14 2024 at 07:28)
#17348 unused arguments (1 message, latest: Oct 14 2024 at 05:07)
#17223 use foldr in List.prod (1 message, latest: Oct 14 2024 at 04:56)
#16159 error in PR (3 messages, latest: Oct 13 2024 at 20:07)
#11156 basis and dual of PiTensorProduct (19 messages, latest: Oct 13 2024 at 19:40)
#16392 chore: rename IsAlgClosure fields (2 messages, latest: Oct 12 2024 at 11:33)
#15779 improve insertLeft / insertRight API (5 messages, latest: Oct 12 2024 at 07:01)
#6045 refactor IsLocalRingHom (23 messages, latest: Oct 09 2024 at 13:29)
#15947 prod and piSetoid lemmas and equivs (2 messages, latest: Oct 09 2024 at 04:58)
#13740 More robust ae notation (2 messages, latest: Oct 06 2024 at 09:04)
#17262 nonarchimedean property of Qp (3 messages, latest: Oct 04 2024 at 10:58)
#17273 Lemmas on Multiset (2 messages, latest: Oct 03 2024 at 17:18)
#16020: store olean sizes (6 messages, latest: Oct 03 2024 at 13:56)
#16840 "ring" tactic variant handling inequalities (5 messages, latest: Oct 02 2024 at 16:04)
#16735 Clean up sSup/sInf API for Real (1 message, latest: Oct 02 2024 at 13:07)
#15743 Jacobi sums (14 messages, latest: Oct 01 2024 at 18:30)
#15815 Generalise the rearrangement inequality (2 messages, latest: Oct 01 2024 at 13:11)
#8013 Walking Reflexive Pair (4 messages, latest: Oct 01 2024 at 09:10)
#15914 feat(Data/List/Sort): List.Sorted.cons (1 message, latest: Oct 01 2024 at 09:01)
#14999 Convex functions are continuous (5 messages, latest: Oct 01 2024 at 07:01)
#16651 fin_omega (6 messages, latest: Sep 29 2024 at 23:14)
#15624 computable ZFSet.sUnion (5 messages, latest: Sep 29 2024 at 09:30)
#17220 and #17222 (2 messages, latest: Sep 29 2024 at 07:22)
#16976 limits in the category of profinite groups (2 messages, latest: Sep 28 2024 at 15:04)
#17197 move galois file (1 message, latest: Sep 28 2024 at 08:50)
#17199 split WeierstrassCurve.VariableChange to a new file (2 messages, latest: Sep 28 2024 at 05:39)
#16864 normal forms of elliptic curves (3 messages, latest: Sep 27 2024 at 18:19)
#17140 (7 messages, latest: Sep 26 2024 at 07:54)
#16666 abandon ring and linarith more quickly (2 messages, latest: Sep 26 2024 at 00:16)
#17139 morphism properties respects left and respects right (1 message, latest: Sep 25 2024 at 20:41)
#16916-19 Galois-group-is-profinite and Fundamental Theorem (7 messages, latest: Sep 24 2024 at 06:12)
#16816 Limit of finite group is profinite group (17 messages, latest: Sep 24 2024 at 06:11)
#17042 use Std.HashMap in linarith (3 messages, latest: Sep 23 2024 at 08:57)
#15915 Cantor Normal Form (8 messages, latest: Sep 23 2024 at 03:11)
#14269 feat(NumberTheory/FactorisationProperties): abundant, (2 messages, latest: Sep 23 2024 at 03:09)
#15764 pre-game product cannot be lifted to games (2 messages, latest: Sep 21 2024 at 09:42)
#15527 partition of a space into fibres (14 messages, latest: Sep 19 2024 at 11:54)
#16897 weaken assumptions on local ring hom properties (5 messages, latest: Sep 18 2024 at 11:46)
#13810 – branch has unmerged commits. (2 messages, latest: Sep 18 2024 at 11:18)
#16489 chore: split Topology.Algebra.Module.WeakDual (7 messages, latest: Sep 17 2024 at 10:30)
Work on MvPowerSeries (3 messages, latest: Sep 17 2024 at 09:57)
#16828 ext lemma for EllipticCurve (3 messages, latest: Sep 16 2024 at 17:14)
#16648 feat(Topology/Group/Profinite)Define Profinite Groups (28 messages, latest: Sep 16 2024 at 16:43)
#16531 split Algebra.MonoidAlgebra.Basic (1 message, latest: Sep 16 2024 at 04:30)
#16405 remove duplicate ToExpr Fin instance (3 messages, latest: Sep 16 2024 at 03:08)
#16234 use List.eraseDups in simps (1 message, latest: Sep 16 2024 at 02:36)
Further cleanup of Init.Logic (39 messages, latest: Sep 15 2024 at 11:53)
#16349 golf proof of Sprague-Grundy (4 messages, latest: Sep 15 2024 at 04:28)
#15535 Pedantic Linter (1 message, latest: Sep 13 2024 at 09:30)
#16446 even and odd functions (2 messages, latest: Sep 12 2024 at 09:18)
#16119 to_app attribute (2 messages, latest: Sep 12 2024 at 09:11)
#14702 feat(Algebra/Polynomial/Derivation): coefficient-wise (1 message, latest: Sep 11 2024 at 11:42)
#16088 Initial development of nimbers (9 messages, latest: Sep 11 2024 at 02:19)
#16585 purely insep. ext. non-commutative case (1 message, latest: Sep 10 2024 at 18:40)
#16584 Monomial orders and Groebner bases (7 messages, latest: Sep 10 2024 at 07:41)
[#16630 feat: Pi.{zero,one}{mono,anti}](topic/.2316630.20feat.3A.20Pi.2E.7Bzero.2Cone.7D.7Bmono.2Canti.7D.html) (2 messages, latest: Sep 09 2024 at 18:15)
#13416: define prefibered categories (2 messages, latest: Sep 09 2024 at 11:16)
#16250 removing primed tactics from Combinatorics (6 messages, latest: Sep 09 2024 at 01:04)
#15335 meta code for monoidal categories (41 messages, latest: Sep 09 2024 at 01:03)
#16401 prove Ordinal linear order instance earlier (3 messages, latest: Sep 07 2024 at 22:57)
✔ #15722 tweak ordinal simp lemmas (4 messages, latest: Sep 06 2024 at 05:58)
#15383 needs a nudge (1 message, latest: Sep 05 2024 at 08:24)
chore: deprecate unused MLList material (1 message, latest: Sep 05 2024 at 03:52)
Approved PRs (2 messages, latest: Sep 03 2024 at 08:52)
#16096 (2 messages, latest: Sep 02 2024 at 23:31)
#15977 Add PSet.rank and ZFSet.rank (1 message, latest: Sep 01 2024 at 23:10)
#15990 more lemmas on Ordinal.log (1 message, latest: Sep 01 2024 at 17:04)
#9857 update nolints periodically (52 messages, latest: Sep 01 2024 at 01:06)
#15522 feat: monotonicity lemmas for OrdinalApprox (9 messages, latest: Aug 31 2024 at 12:22)
#15716 combinatorial game birthday (1 message, latest: Aug 31 2024 at 04:16)
#16189 / #16198 removing induction' and cases' (5 messages, latest: Aug 30 2024 at 15:51)
#15610 the longFile linter (8 messages, latest: Aug 30 2024 at 11:56)
#15097 the long line linter as a syntax linter (39 messages, latest: Aug 29 2024 at 22:55)
#16253 Basics of Discrete Fair Division (17 messages, latest: Aug 29 2024 at 21:43)
#14739 Measure: add gcongr lemmas (5 messages, latest: Aug 29 2024 at 04:47)
#16140 and relative representability (3 messages, latest: Aug 27 2024 at 11:26)
#13997 analytic continuation of Dirichlet L-series (2 messages, latest: Aug 27 2024 at 07:33)
#15686 FreeAlgebra asPowers, simp opts (3 messages, latest: Aug 26 2024 at 04:33)
#15813 Actions on and by an order synonym (2 messages, latest: Aug 25 2024 at 20:26)
#13950 Dualisable notion of ExistsAddOfLE (45 messages, latest: Aug 25 2024 at 15:23)
#16120 Ring homomorphisms as a StrongHomClass (7 messages, latest: Aug 25 2024 at 01:52)
#14660 Put a simplex between a point and a neighborhood (3 messages, latest: Aug 22 2024 at 22:12)
#16018 SimpleGraph extending Digraph (24 messages, latest: Aug 22 2024 at 06:21)
#15555: feat(RelSeries): LTSeries.iota (1 message, latest: Aug 21 2024 at 16:45)
#15521 enable the setOption, longLine, missingEnd linters (3 messages, latest: Aug 20 2024 at 07:47)
#15758 Nat.descFactorial_le (1 message, latest: Aug 19 2024 at 19:32)
#15759 chore: backports from byAsSorry (1 message, latest: Aug 19 2024 at 11:10)
#15960 Fintype (LTSeries α) if Fintype α (3 messages, latest: Aug 19 2024 at 04:33)
#15371 Remove some uses of open Classical (25 messages, latest: Aug 17 2024 at 21:23)
#15920 functor product : (A ⥤ B) × (C ⥤ D) ⥤ A × C ⥤ B × D (1 message, latest: Aug 17 2024 at 13:42)
#14091 on digraphs (13 messages, latest: Aug 17 2024 at 04:28)
#14162 (3 messages, latest: Aug 16 2024 at 06:23)
#15854 Make rel_iso_iff universe polymorphic (1 message, latest: Aug 15 2024 at 19:10)
#13973 lake exe refactor (3 messages, latest: Aug 14 2024 at 08:04)
#15794 DocModule syntax linter (6 messages, latest: Aug 14 2024 at 08:01)
#15635 ensure Batteries is fully built in lake test (1 message, latest: Aug 14 2024 at 02:04)
#15258 Cat is monoidal with the cartesian product of categor (3 messages, latest: Aug 14 2024 at 01:33)
#15380 topology on ENat (8 messages, latest: Aug 13 2024 at 22:24)
#15614 typeToCat is right adjoint to connectedComponents (2 messages, latest: Aug 13 2024 at 20:15)
#15756 backports from nightly-testing-2024-08-12 (2 messages, latest: Aug 13 2024 at 09:16)
#15762 (2 messages, latest: Aug 13 2024 at 09:14)
#15116 Make circle a type (8 messages, latest: Aug 13 2024 at 09:09)
#15726 move to v4.11.0-rc2 (new variable) (59 messages, latest: Aug 13 2024 at 00:13)
#15318 flexible linter fixes (2 messages, latest: Aug 12 2024 at 14:25)
#15717 (8 messages, latest: Aug 12 2024 at 14:03)
Style linter for ← (5 messages, latest: Aug 09 2024 at 19:58)
Too many lines linter (28 messages, latest: Aug 09 2024 at 18:05)
#15606 backports for leanprover/lean4#4814 (part 35) (1 message, latest: Aug 08 2024 at 20:15)
#15221 remove outdated comment about Bundled.map (3 messages, latest: Aug 08 2024 at 18:33)
#15424 Residue field is finite iff totally bounded DVR (19 messages, latest: Aug 07 2024 at 16:57)
#15180 fix minImports for server (1 message, latest: Aug 07 2024 at 06:22)
#14991 scalar tower instances for Module.End (1 message, latest: Aug 05 2024 at 21:04)
#14721 change minimality to a predicate (20 messages, latest: Aug 05 2024 at 16:45)
The category of pointed objects of a concrete category (20 messages, latest: Aug 05 2024 at 08:54)
Speeding up Geometry/ (24 messages, latest: Aug 04 2024 at 13:53)
#15447 union of an infinite collection of sets is infinite (1 message, latest: Aug 02 2024 at 15:20)
[#15188 cleanup in Mathlib/Init/](topic/.2315188.20cleanup.20in.20Mathlib.2FInit.2F.html) (4 messages, latest: Aug 02 2024 at 11:20)
squashing commits + keeping up with master in PR (2 messages, latest: Aug 02 2024 at 05:02)
#15145 report commits in nightly testing bot (1 message, latest: Jul 31 2024 at 23:53)
#13486 API for essentially small sites (2 messages, latest: Jul 31 2024 at 14:57)
#15061 direct sums of matroids (6 messages, latest: Jul 31 2024 at 11:46)
Algebraic geometry PRs (9 messages, latest: Jul 31 2024 at 06:53)
#12273 Konig's infinity lemma (1 message, latest: Jul 30 2024 at 17:31)
#15177 Renaming snorm to eLpNorm (4 messages, latest: Jul 30 2024 at 17:02)
#9781 Dyck words (7 messages, latest: Jul 30 2024 at 07:37)
#15171 move 'Walk' from Connectivity into its own file (16 messages, latest: Jul 30 2024 at 07:37)
#14699: Differential rings and notation (9 messages, latest: Jul 29 2024 at 12:27)
#8304 Extended Hales-Jewett (25 messages, latest: Jul 29 2024 at 06:43)
#13424 NormedSpace.Core (5 messages, latest: Jul 29 2024 at 01:34)
#14927 clopen inside another set (1 message, latest: Jul 28 2024 at 16:39)
#10541: SkewMonoidAlgebra (6 messages, latest: Jul 24 2024 at 10:41)
#13514 CF languages union (2 messages, latest: Jul 23 2024 at 20:00)
#14992: algebraic geometry: HasRingHomProperty (3 messages, latest: Jul 23 2024 at 19:33)
#15001: algebraic geometry: opens of a scheme (1 message, latest: Jul 23 2024 at 19:21)
#15028 More matroid closure + insertion (1 message, latest: Jul 22 2024 at 19:10)
#15025 matroid closure and independence (1 message, latest: Jul 22 2024 at 17:16)
#13483 update_deprecations (22 messages, latest: Jul 22 2024 at 17:06)
#14975 define closed n-manifolds (5 messages, latest: Jul 21 2024 at 17:53)
#14887 remove #align and #align_import statements (172 messages, latest: Jul 20 2024 at 16:34)
quote4#47 documentation for ~q() (2 messages, latest: Jul 19 2024 at 21:27)
#14882: Being an isomorphism is local at the target (2 messages, latest: Jul 19 2024 at 10:49)
#14858: AlgebraCat.FilteredColimits begins (29 messages, latest: Jul 19 2024 at 00:20)
#14479 Antidiagonals for SMul and VAdd (2 messages, latest: Jul 18 2024 at 18:32)
#14874 Euler's proof and counterexample of prime Fermat … (1 message, latest: Jul 18 2024 at 17:52)
#14418 : the Laurent series valuation saga continues (8 messages, latest: Jul 18 2024 at 13:06)
#14430 algebraic geometry morphisms refactor (4 messages, latest: Jul 18 2024 at 11:40)
#14826 Split RingTheory.IntegralClosure (42 messages, latest: Jul 18 2024 at 11:04)
#12016: unfold? tactic (1 message, latest: Jul 18 2024 at 10:01)
#9249 suffix ₚ for positivity assumptions (35 messages, latest: Jul 18 2024 at 01:00)
#14466 chore: split Algebra/Module/Equiv (1 message, latest: Jul 16 2024 at 16:58)
#14437 – the #min_imports command (59 messages, latest: Jul 16 2024 at 15:12)
✔ #13939 Multiplicative characters (9 messages, latest: Jul 15 2024 at 20:38)
✔ #14458 Polar set of a submodule (14 messages, latest: Jul 15 2024 at 20:38)
#12221 Subbasis closed under intersection (4 messages, latest: Jul 15 2024 at 17:52)
✔ #14540 chore: remove scripts/mk_all.sh (6 messages, latest: Jul 15 2024 at 04:37)
#14452 Coefficients of products of univ. power series (5 messages, latest: Jul 13 2024 at 17:19)
#14704 typeclass for simple field extensions (1 message, latest: Jul 13 2024 at 09:50)
#13317 Hopf monoids in braided categories (14 messages, latest: Jul 12 2024 at 20:44)
#13972 Noetherian Schemes (1 message, latest: Jul 12 2024 at 17:56)
#12572 Complete homogeneous, monomial symmetric polynomials (2 messages, latest: Jul 12 2024 at 11:21)
#14647, splitting Combinatorics/SimpleGraph/Connectivity (9 messages, latest: Jul 11 2024 at 12:25)
#14542 Making Equiv.Perm.support a Set (6 messages, latest: Jul 10 2024 at 22:24)
#14616 Slightly strength Fin.completeLinearOrder (1 message, latest: Jul 10 2024 at 15:52)
#14004 Strong atomicity (4 messages, latest: Jul 10 2024 at 15:41)
Dualizing category theory API (6 messages, latest: Jul 10 2024 at 09:58)
#13724 SubtractionMonoid instance for LinearOrderedAddCommGr (3 messages, latest: Jul 09 2024 at 17:35)
#14571 Order and LexOrder of multivariate power series (1 message, latest: Jul 09 2024 at 16:43)
#14163 (2 messages, latest: Jul 09 2024 at 16:29)
#14557 extensible unused tactics (3 messages, latest: Jul 09 2024 at 08:39)
#14454 Invertibility of power series (2 messages, latest: Jul 06 2024 at 16:33)
#14431 Induction principles for ≤ on Nat (1 message, latest: Jul 06 2024 at 09:12)
#13012 functors preserving 1-hypercovers are continuous (2 messages, latest: Jul 04 2024 at 12:51)
#14197 Matroid closure (3 messages, latest: Jul 04 2024 at 07:31)
#13210 shorten names of continued fraction declarations (19 messages, latest: Jul 03 2024 at 08:17)
leanprover-community.github.io#480, #482,#483 Lean 4 update (4 messages, latest: Jul 03 2024 at 07:24)
#13162 algebras essentially of finite type (1 message, latest: Jul 03 2024 at 07:10)
#13637 (1 message, latest: Jul 02 2024 at 16:19)
#14034 Well-founded of strictly monotone (1 message, latest: Jul 02 2024 at 14:21)
#14195 Injections from disjoint sets (1 message, latest: Jul 02 2024 at 13:54)
#14335 avoid order in Module.LinearMap.End (4 messages, latest: Jul 01 2024 at 18:44)
#14233 scope simps in Algebra.AddConstMap (14 messages, latest: Jul 01 2024 at 15:50)
#13585 BinomialRing instance for NNRat algebras (2 messages, latest: Jul 01 2024 at 08:26)
#13178 Krull dimension of a topological space (2 messages, latest: Jul 01 2024 at 01:03)
#14060 bounded recursion on ordinals and clubs (1 message, latest: Jun 30 2024 at 12:13)
#12346 Colexicographic order on Finset Nat (15 messages, latest: Jun 29 2024 at 19:16)
#14219 delay imports of Star (1 message, latest: Jun 28 2024 at 11:47)
✔ #14095 Build fails in the checks (12 messages, latest: Jun 28 2024 at 08:30)
#14188 blind abel to ordered algebra (2 messages, latest: Jun 28 2024 at 01:39)
#14069 if the RHS constrains universes, make it explicit (7 messages, latest: Jun 27 2024 at 07:42)
PRs for Turán's theorem (28 messages, latest: Jun 26 2024 at 14:44)
#13145 : Removing finiteness requirement for cycleOf (27 messages, latest: Jun 26 2024 at 12:47)
#13960 Matroid maps (2 messages, latest: Jun 26 2024 at 12:27)
#9814 Tweak of BoundedOrder and Lattice for Fin (16 messages, latest: Jun 26 2024 at 10:33)
#13694 chore: reverse gdelta/separation dependency (3 messages, latest: Jun 26 2024 at 02:14)
#14047 removing CI surrounding move-decls (1 message, latest: Jun 23 2024 at 07:45)
#14002 making TensorProduct.mul irreducible (1 message, latest: Jun 21 2024 at 16:56)
channel events (1 message, latest: Jun 21 2024 at 01:34)
Porting notes (1 message, latest: Jun 20 2024 at 07:58)
#13638 - set insertion / maximality (4 messages, latest: Jun 20 2024 at 03:23)
#13929, doc-strings in Analysis/Convex/Slope (3 messages, latest: Jun 18 2024 at 17:48)
#13692 Bijectivity on supersets (2 messages, latest: Jun 18 2024 at 16:06)
subsingleton tactic #12525 (5 messages, latest: Jun 17 2024 at 22:24)
#13887 Statement of Poincaré conjecture (7 messages, latest: Jun 17 2024 at 05:40)
#13746: deprecate unused HashMap API additions (1 message, latest: Jun 16 2024 at 00:25)
#12058 Diameter of simple graphs (2 messages, latest: Jun 15 2024 at 19:18)
#13353 discrete Fourier transform on ZMod N (50 messages, latest: Jun 14 2024 at 17:01)
#9398 itauto tactic (2 messages, latest: Jun 12 2024 at 17:47)
#13013 bounded, a.e. cont. function is integrable on a box (4 messages, latest: Jun 12 2024 at 11:31)
#11143 Bergelson Intersectivity Lemma (1 message, latest: Jun 11 2024 at 17:23)
#13719: trans for implications (10 messages, latest: Jun 11 2024 at 11:00)
#13716 add commit hash to PR summary (1 message, latest: Jun 11 2024 at 08:40)
#13589 deprecate duplicate definitions about Bool (1 message, latest: Jun 11 2024 at 03:39)
#12875 pairs (10 messages, latest: Jun 10 2024 at 13:37)
✔ #13605 cleanup redundant type arguments (4 messages, latest: Jun 10 2024 at 08:53)
#13176 Feat: weaken 2ndCnt to Lindelof in Reg+Lind=>Normal (10 messages, latest: Jun 10 2024 at 08:43)
#13540 move GaussSums from under LegendreSymbol (6 messages, latest: Jun 10 2024 at 04:34)
#12555 inj/bij/surjectivity (4 messages, latest: Jun 08 2024 at 18:05)
#9334 Sesquilinear Maps and Matrices (1 message, latest: Jun 08 2024 at 10:12)
#12415 matroid constructions (9 messages, latest: Jun 07 2024 at 11:29)
#13500 bors failed because of merge conflict (1 message, latest: Jun 07 2024 at 09:57)
#12076 Orzech's theorem (66 messages, latest: Jun 06 2024 at 10:46)
#12731 Make CompleteLinearOrder extend BiheytingAlgebra (4 messages, latest: Jun 06 2024 at 08:44)
#3730 Remove Cat suffix (6 messages, latest: Jun 06 2024 at 08:39)
#12544 Add regular sequence (1 message, latest: Jun 05 2024 at 20:03)
#1388 Redefine pow in terms of iterate (31 messages, latest: Jun 05 2024 at 07:10)
#13525 fix names for String lemmas (1 message, latest: Jun 05 2024 at 04:33)
#13489 regularly update dependencies (1 message, latest: Jun 05 2024 at 01:53)
#13521 chore(Data/UInt): deprecate UInt8.isUpper etc (1 message, latest: Jun 04 2024 at 23:31)
#13489 chore: regularly update dependencies (2 messages, latest: Jun 04 2024 at 02:13)
#13472 removing refine' (3 messages, latest: Jun 03 2024 at 09:12)
#13170 remove accidental global instance (15 messages, latest: Jun 02 2024 at 20:59)
#13392 Multiplicative characters (5 messages, latest: Jun 01 2024 at 20:11)
#13413 fix to @[elementwise] (1 message, latest: Jun 01 2024 at 15:47)
#13395 Add success message to the cache (3 messages, latest: Jun 01 2024 at 12:27)
leanprover-community.github.io#391 calc mode for Lean 4 (3 messages, latest: Jun 01 2024 at 11:50)
#13164 chore: remove bad simps, and add test (16 messages, latest: May 31 2024 at 21:35)
#7386 Linear Programming (167 messages, latest: May 31 2024 at 19:29)
✔ #13065 normalized factors (5 messages, latest: May 31 2024 at 08:28)
#13319 refactor of light profinite sets (3 messages, latest: May 30 2024 at 13:37)
#13287 more refine' replacements (10 messages, latest: May 30 2024 at 11:19)
#13357 refine' to refine final(?) batch (2 messages, latest: May 29 2024 at 23:12)
#13037 New simp lemmas for HomogeneousLocalization (1 message, latest: May 28 2024 at 18:25)
#12986 second countable profinite spaces (1 message, latest: May 28 2024 at 12:21)
#12498 some linear maps induced by mul. for submodules (1 message, latest: May 27 2024 at 22:36)
#13115 smooth numbers (9 messages, latest: May 27 2024 at 12:00)
#12551 No wrap-around principle for 3APs (1 message, latest: May 27 2024 at 07:02)
#12992 (3 messages, latest: May 27 2024 at 06:16)
#12653 More ways of bijecting finsets (1 message, latest: May 26 2024 at 10:12)
#13142 Removing the hash-command linter script (6 messages, latest: May 25 2024 at 21:41)
✔ #11945 distance between vertices is 1 iff they are adja… (5 messages, latest: May 24 2024 at 19:48)
✔ feat: add competely normal (non-Hausdorff) property #12458 (2 messages, latest: May 24 2024 at 18:28)
#13166 refine' to refine (43 messages, latest: May 24 2024 at 16:10)
#12769: Fourier transform of iterated derivatives (1 message, latest: May 24 2024 at 07:24)
#13110 aesop_cat uses sorry if there is a sorry (7 messages, latest: May 23 2024 at 07:10)
bimonoid objects (1 message, latest: May 23 2024 at 05:17)
#13109 simp lemmas for unbundled comp and categorical ids (1 message, latest: May 23 2024 at 01:47)
✔ Docstrings for Computability: #12480 and #13087 (3 messages, latest: May 22 2024 at 06:50)
concrete categories (4 messages, latest: May 22 2024 at 05:40)
#13080 minor cleanup in aisle AG (5 messages, latest: May 22 2024 at 05:06)
#12849 relax condition of Subalgebra.eq_bot_of_finrank_one (14 messages, latest: May 21 2024 at 19:44)
#13045 (5 messages, latest: May 21 2024 at 04:08)
#13054 simp normal form for Abelianization.map (1 message, latest: May 21 2024 at 01:50)
#11920 towards proj construction (18 messages, latest: May 20 2024 at 15:44)
#13046 backporting some additional implicit arguments (1 message, latest: May 20 2024 at 00:49)
#12947, use since := "YYYY-MM-DD" in @[deprecated] (5 messages, latest: May 17 2024 at 09:14)
#12567 chore: remove an unused congr lemma (5 messages, latest: May 17 2024 at 07:39)
feat(Topology): stoneCechUnit injective for T35Space #12536 (4 messages, latest: May 16 2024 at 02:40)
#12886 new CI check for noisy files (1 message, latest: May 15 2024 at 23:06)
#12425 split RatFunc (2 messages, latest: May 15 2024 at 15:46)
#12648 regular expression nfa equivalence (1 message, latest: May 14 2024 at 18:54)
#12781 rename a few lemmas exp –> rexp (16 messages, latest: May 14 2024 at 11:28)
#9733 (2 messages, latest: May 13 2024 at 01:04)
#12705 Prime ideal separator in bounded dist lattices (10 messages, latest: May 11 2024 at 18:49)
#12515: reduced diff in CI (24 messages, latest: May 11 2024 at 05:57)
#12004 switch lean4checker to a cron job (2 messages, latest: May 10 2024 at 10:24)
#11853 lake exe mkAll (6 messages, latest: May 10 2024 at 10:22)
removing things labeled helper (1 message, latest: May 09 2024 at 20:25)
#12777 split RingTheory.Ideal.Operations (6 messages, latest: May 09 2024 at 15:43)
#12636 make Opposite.op the constructor for Opposite (2 messages, latest: May 08 2024 at 14:57)
#12755 remove another refine' {..} pattern (1 message, latest: May 08 2024 at 12:17)
#10681 positivity extension for posPart (1 message, latest: May 08 2024 at 06:24)
#12741 even more universe annotations (1 message, latest: May 07 2024 at 21:15)
#12729 clean up copying orders (1 message, latest: May 07 2024 at 16:51)
feat: Positivity extension for Finset.prod #9365 (3 messages, latest: May 07 2024 at 15:14)
#12546 Turn Freiman homs into predicates (6 messages, latest: May 07 2024 at 12:32)
#12570 Construct a tripartite graph from its triangles (2 messages, latest: May 07 2024 at 06:23)
#12144 Fourier transform on Schwartz space (10 messages, latest: May 06 2024 at 19:10)
#12569 More additive energy lemmas (1 message, latest: May 06 2024 at 07:34)
#12394 defines tight measures, is it too long? (18 messages, latest: May 05 2024 at 11:07)
#12526 Locally linear graphs (1 message, latest: May 04 2024 at 18:22)
#10824 Tensor products of finsupp types (26 messages, latest: May 04 2024 at 17:58)
#12397 - some List.nthLe -> get migration (3 messages, latest: May 02 2024 at 15:53)
#12563 slightly less defeq abuse in AG (7 messages, latest: May 01 2024 at 13:02)
#12523 Triangle removal (1 message, latest: May 01 2024 at 07:49)
#12422 multi-goal linter (5 messages, latest: Apr 30 2024 at 14:07)
#12470 split MeasureTheory.Constructions.BorelSpace.Basic (7 messages, latest: Apr 29 2024 at 22:56)
#10551 More big operators lemmas (7 messages, latest: Apr 29 2024 at 22:10)
#8896 Triangle counting (2 messages, latest: Apr 29 2024 at 09:34)
#12364 Move NormalizedGCDMonoid Int to reduce imports (9 messages, latest: Apr 27 2024 at 10:59)
#3976 instance LawfulFunctor Array (4 messages, latest: Apr 27 2024 at 04:42)
metapro book, #136, "run on Lean4 playground" (2 messages, latest: Apr 26 2024 at 16:18)
#12380 direct sum of matroids (39 messages, latest: Apr 26 2024 at 12:27)
std4#314 (8 messages, latest: Apr 26 2024 at 07:32)
(deleted) (1 message, latest: Apr 25 2024 at 21:55)
#9513 co/limits in LightProfinite (2 messages, latest: Apr 23 2024 at 13:28)
Adding dates to remaining deprecations (2 messages, latest: Apr 22 2024 at 22:51)
✔ metaprogramming in lean, #131 (2 messages, latest: Apr 21 2024 at 08:49)
#12279 Hölder's inequality (8 messages, latest: Apr 20 2024 at 19:11)
#11774 Cocardinal, cocountable filters (1 message, latest: Apr 20 2024 at 11:27)
std4#748 unbundle array size constraint from hash map bucket (12 messages, latest: Apr 19 2024 at 16:14)
#10603 ae_toKernel_eq_one disappearing (3 messages, latest: Apr 17 2024 at 06:59)
review request: #12120 (new theorems about Real.rpow) (12 messages, latest: Apr 16 2024 at 03:02)
✔ metapro book/#137 (6 messages, latest: Apr 15 2024 at 18:46)
#12104 shorten long pole (2 messages, latest: Apr 15 2024 at 06:38)
#7898 (3 messages, latest: Apr 14 2024 at 07:21)
#11798 remove autoImplicit from more files (12 messages, latest: Apr 13 2024 at 22:19)
#11620 add a few new theorems (2 messages, latest: Apr 13 2024 at 19:23)
#12048 - The Iwasawa criterion for simplicity (5 messages, latest: Apr 13 2024 at 12:47)
#12037 remove an instance (1 message, latest: Apr 09 2024 at 19:14)
#11800 K-Lindelöf spaces (5 messages, latest: Apr 09 2024 at 18:08)
PRs from sphere eversion (11 messages, latest: Apr 09 2024 at 12:50)
#12023 Generalize preimage_smul_set etc to equivariant maps (1 message, latest: Apr 09 2024 at 06:38)
#11822 flexible tactics linter (17 messages, latest: Apr 08 2024 at 11:27)
metaprogramming in lean, #115 (1 message, latest: Apr 06 2024 at 13:38)
#11867 eq_on versions of deriv lemmas (2 messages, latest: Apr 06 2024 at 06:22)
#10515 and #10531 : cocardinal and CardinalInterFilter (13 messages, latest: Apr 04 2024 at 06:23)
#10856 Measurability Modulo a filter (2 messages, latest: Apr 02 2024 at 17:11)
PR #11851 Multigraphs, Paths, Homotopy (7 messages, latest: Apr 02 2024 at 13:48)
> PR #11604: Serre graphs, fundamental groups, covering spac (9 messages, latest: Apr 02 2024 at 12:34)
#11832 (4 messages, latest: Apr 01 2024 at 23:58)
#11019: a syntax linter for #-commands (23 messages, latest: Mar 31 2024 at 07:55)
#11776 higher derivative of Fourier transform (2 messages, latest: Mar 29 2024 at 20:34)
bors crashed on #11322 and closed the PR (7 messages, latest: Mar 28 2024 at 16:44)
#9163 Vitali's convergence theorem (2 messages, latest: Mar 27 2024 at 19:21)
#11591 (3 messages, latest: Mar 27 2024 at 17:57)
#11689 VCSP expressive power (12 messages, latest: Mar 27 2024 at 11:06)
#11470 Uniform convergence topology type-synonym (1 message, latest: Mar 27 2024 at 05:11)
PRs from new contributors (5 messages, latest: Mar 26 2024 at 22:12)
#16040 Spin Group (40 messages, latest: Mar 26 2024 at 06:49)
renaming symmetric MvPolynomials #11251 (7 messages, latest: Mar 24 2024 at 22:02)
CI fails with unused variable error (19 messages, latest: Mar 24 2024 at 07:25)
#11451 : change order of expansion for powers (5 messages, latest: Mar 23 2024 at 21:43)
#11231 fix a crash in slim_check (2 messages, latest: Mar 22 2024 at 22:53)
#10661 Positivity extension for integrals (2 messages, latest: Mar 22 2024 at 22:43)
#11534: norm on a PiTensorProduct (3 messages, latest: Mar 21 2024 at 20:23)
#11542 Splitting Data.List.Basic (3 messages, latest: Mar 21 2024 at 03:21)
#11530 Rename mul-div cancellation lemmas (2 messages, latest: Mar 20 2024 at 21:29)
characterize roots of unity in cyclotomic extensions #10710 (4 messages, latest: Mar 20 2024 at 16:34)
#11247 non-terminal simp linter (10 messages, latest: Mar 20 2024 at 15:54)
#10924: remove unnecessary assumptions (36 messages, latest: Mar 18 2024 at 08:37)
#9736 single-edge graph (3 messages, latest: Mar 18 2024 at 04:02)
#10565 Topological properties of order-connected sets in ℝⁿ (2 messages, latest: Mar 17 2024 at 18:02)
#11372 DFA.acceptsFrom, DFA.map, DFA.equiv (2 messages, latest: Mar 17 2024 at 14:00)
#11257 Basic lemmas about List recursion principles (1 message, latest: Mar 17 2024 at 12:54)
[#11418 chore(): remove empty lines between variable](topic/.2311418.20chore().3A.20remove.20empty.20lines.20between.20variable.html) (4 messages, latest: Mar 16 2024 at 17:18)
#11069 (sums over Int) (2 messages, latest: Mar 14 2024 at 13:01)
#11303 (generalize and add 2 thms) (1 message, latest: Mar 12 2024 at 14:44)
#11312 (move AddChar definitions) (1 message, latest: Mar 12 2024 at 09:59)
#11305 — shrink CategoryTheory.Subterminal by 95% (2 messages, latest: Mar 11 2024 at 22:12)
#11235 (1 message, latest: Mar 11 2024 at 09:31)
#11214 L-series: naming (4 messages, latest: Mar 10 2024 at 16:53)
#6307 refactor of monoidal categories (18 messages, latest: Mar 07 2024 at 23:11)
#10562 feat(Tactic.Bound): Add a bound tactic for ineq… (2 messages, latest: Mar 06 2024 at 08:32)
fix(fun_prop): few bug fixes for fun_prop #11092 (1 message, latest: Mar 05 2024 at 14:22)
#10725 and #10728: L-series (112 messages, latest: Mar 05 2024 at 12:36)
#6057 MulActionHom in the semilinear style (30 messages, latest: Mar 05 2024 at 10:42)
#11002 (operator norm) (2 messages, latest: Mar 04 2024 at 20:27)
#7496 add nonterminal simp checker (10 messages, latest: Mar 03 2024 at 10:48)
#11049 (1 message, latest: Feb 29 2024 at 19:47)
#10000 Abel's limit theorem (3 messages, latest: Feb 29 2024 at 12:50)
✔ #11050: split InfiniteSum.Basic (4 messages, latest: Feb 29 2024 at 10:29)
Positivity extensions (5 messages, latest: Feb 29 2024 at 09:14)
#10566 - bounded sets of PGames (2 messages, latest: Feb 28 2024 at 15:58)
#11027 - First isomorphism theorem for algebras (1 message, latest: Feb 28 2024 at 06:45)
#10833 cleanup Fourier (1 message, latest: Feb 28 2024 at 06:07)
#10909 porting notes in RingTheory.Polynomial.Basic (3 messages, latest: Feb 28 2024 at 04:47)
#11022 remove an erw (1 message, latest: Feb 27 2024 at 20:06)
#9815 split Topology/MetricSpace/Pseudometric.lean (6 messages, latest: Feb 26 2024 at 16:30)
#7894 fractional polymorphisms for VCSP (6 messages, latest: Feb 26 2024 at 08:42)
#10910 appropriate transparency level for diamond checks (7 messages, latest: Feb 25 2024 at 17:17)
#10907 split Mathlib.GroupTheory.Perm.Cycle.Basic (16 messages, latest: Feb 24 2024 at 17:06)
#10900 split off ordered instances for subalgebraic things (3 messages, latest: Feb 23 2024 at 22:57)
#10581 string diagrams (1 message, latest: Feb 23 2024 at 04:10)
#10828 - generalizing CommRing to CommSemiring etc. (11 messages, latest: Feb 21 2024 at 22:54)
#10724 fun_prop refactor and bug fixes (1 message, latest: Feb 19 2024 at 18:26)
#10715 - correct a docstring (1 message, latest: Feb 19 2024 at 10:49)
#10637 - correct bug in Mathlib.Data.Finset.Sym (12 messages, latest: Feb 18 2024 at 07:03)
#10640 - remove old style uses of have (7 messages, latest: Feb 17 2024 at 12:02)
#8187 & #8788 (4 messages, latest: Feb 16 2024 at 14:40)
#9933 actually check cache works (12 messages, latest: Feb 16 2024 at 10:47)
#10415 Add yang baxter equation and the opposite braided mon (5 messages, latest: Feb 15 2024 at 23:22)
feat: define PGame.identical PGame.memₗ PGame.memᵣ #5901 (14 messages, latest: Feb 15 2024 at 21:31)
#10009 Dilation equiv in normed spaces (1 message, latest: Feb 14 2024 at 18:52)
PR #6042 Singular Value Decomposition (41 messages, latest: Feb 13 2024 at 19:00)
chore: add setting to prevent accidental editing of depende (3 messages, latest: Feb 13 2024 at 18:58)
#10496 address porting notes in Order.Grade (5 messages, latest: Feb 13 2024 at 17:32)
#9372, convolution of measures (1 message, latest: Feb 12 2024 at 19:07)
#10139 everywhere positive sets (7 messages, latest: Feb 12 2024 at 13:17)
#10403 notation scopes for arith funs (1 message, latest: Feb 12 2024 at 11:05)
#8979 making Finsupp.filter computable (10 messages, latest: Feb 12 2024 at 08:33)
#9920 reorganisation of coherent files (3 messages, latest: Feb 11 2024 at 10:50)
✔ #9910 generalizing mkPiField (2 messages, latest: Feb 09 2024 at 19:26)
#10344 removing norm_num support for Nat.sub, Sub.sub, etc (17 messages, latest: Feb 09 2024 at 05:38)
#10316 remove duplicate instances (1 message, latest: Feb 07 2024 at 00:00)
#10099 Integration by parts (5 messages, latest: Feb 05 2024 at 08:46)
"Staging failed at cache" bell (6 messages, latest: Feb 04 2024 at 21:54)
#8773 Extensionality principle for bitvectors (1 message, latest: Feb 03 2024 at 20:47)
#10191 heartbeat bumped files down into the single digits (12 messages, latest: Feb 02 2024 at 22:23)
#10185 renaming with deprecation (4 messages, latest: Feb 02 2024 at 22:19)
#10187 ensure that the linter fails when it should (9 messages, latest: Feb 02 2024 at 14:15)
Preliminary PRs for L-series (5 messages, latest: Feb 01 2024 at 20:05)
#10077 rename _0 -> _zero, _1 -> _one (3 messages, latest: Jan 31 2024 at 21:34)
#10129 Make infsep consistent with diam and infdist (1 message, latest: Jan 30 2024 at 17:31)
#9961 positivity extension for algebraMap (1 message, latest: Jan 30 2024 at 13:36)
#9145 Refactor of succAbove etc. (96 messages, latest: Jan 30 2024 at 13:02)
#10042 New lemmas for succAbove (3 messages, latest: Jan 26 2024 at 22:30)
✔ #9869 splitting Data.ENNReal.Basic (2 messages, latest: Jan 26 2024 at 01:29)
#9658 ~~avoid~~ fix tc search (1 message, latest: Jan 25 2024 at 22:32)
#9564 Weaken commutativity assumptions for AdjoinRoot.lift a (23 messages, latest: Jan 25 2024 at 15:37)
#9847, #9889 arctangent API (1 message, latest: Jan 23 2024 at 01:59)
Rename and small lemma (1 message, latest: Jan 21 2024 at 20:46)
#8735 finpartitions from setoids (9 messages, latest: Jan 21 2024 at 02:55)
✔ #9783 and #9666 Modular forms (12 messages, latest: Jan 20 2024 at 12:19)
#9728 tidying (5 messages, latest: Jan 17 2024 at 22:58)
#9791 + #9793: Redefine predAbove and succAbove (4 messages, latest: Jan 17 2024 at 00:41)
#9588, #9565 Splitting MFDeriv (5 messages, latest: Jan 16 2024 at 23:00)
✔ #9780 Redefinition of castPred (11 messages, latest: Jan 16 2024 at 20:58)
✔ #9652 Matrix.dotProduct inequalities (16 messages, latest: Jan 15 2024 at 14:55)
#9658 avoid tc search (4 messages, latest: Jan 15 2024 at 14:07)
Move set definitions to a new file #9737 (24 messages, latest: Jan 15 2024 at 13:54)
#9251 caratheodory theorem for convex cones (10 messages, latest: Jan 15 2024 at 10:13)
#9006 Unit subgroup (56 messages, latest: Jan 15 2024 at 01:02)
#9695 Performance issues refactoring Submodule lattice def (1 message, latest: Jan 12 2024 at 17:40)
(Frechet) derivative of the Fourier transform (1 message, latest: Jan 11 2024 at 22:04)
#9655 de-prioritize Subalgebra.module' (4 messages, latest: Jan 11 2024 at 18:39)
#9267 local graph operations (13 messages, latest: Jan 11 2024 at 16:06)
#9636 and #9637 speed up CategoryTheory files (7 messages, latest: Jan 11 2024 at 09:38)
HasPrimitives on disc (1 message, latest: Jan 09 2024 at 22:48)
chore(Covby): rename Covby to CovBy #9578 (7 messages, latest: Jan 09 2024 at 09:06)
#9555 speed up ProjectiveResolution (7 messages, latest: Jan 08 2024 at 20:22)
#9556 Removing yet another commutativity assumption (5 messages, latest: Jan 08 2024 at 19:49)
#9495 Remove yet another commutativity instance (1 message, latest: Jan 06 2024 at 23:30)
#9493 Weaken an instance (3 messages, latest: Jan 06 2024 at 23:21)
#9404 EReal (2 messages, latest: Jan 05 2024 at 21:21)
✔ #9408 and #9200 (2 messages, latest: Jan 05 2024 at 13:39)
Integral curves on manifolds (9 messages, latest: Jan 05 2024 at 09:11)
#9399 and #9400 (2 messages, latest: Jan 04 2024 at 07:13)
#9359 Centralizer of a permutation (1 message, latest: Dec 31 2023 at 13:20)
#9270 estimates for the complex logarithm (3 messages, latest: Dec 29 2023 at 21:26)
#13483 move_add (69 messages, latest: Dec 27 2023 at 19:28)
#7904 Antidiagonal for finsupp-orted functions (3 messages, latest: Dec 26 2023 at 15:57)
#6057 refactor MulActionHom to allow “semilinear”-style maps (2 messages, latest: Dec 26 2023 at 15:18)
#9159 dimension of dual space (Erdős-Kaplansky) (8 messages, latest: Dec 25 2023 at 19:43)
#8878 refactor(ProperCone) (2 messages, latest: Dec 24 2023 at 05:31)
✔ Linear maps and DistribMulAction hom (#6057) (8 messages, latest: Dec 23 2023 at 16:19)
#9116 Introducing Complex.slitPlane (57 messages, latest: Dec 23 2023 at 06:53)
#7506 : compatible measures on quotient spaces and groups (3 messages, latest: Dec 19 2023 at 04:09)
#9114 API for ltByCases (101 messages, latest: Dec 17 2023 at 09:12)
#9079 Golfing simps (10 messages, latest: Dec 17 2023 at 00:28)
#7795 Nonterminal simps (14 messages, latest: Dec 16 2023 at 00:06)
#8809 positive semidef matrices (29 messages, latest: Dec 15 2023 at 18:00)
#15763: Lie group of ring units (19 messages, latest: Dec 14 2023 at 13:39)
#8732 (Matroid Duality) (1 message, latest: Dec 12 2023 at 15:07)
#8727 refactoring sheafification (10 messages, latest: Dec 11 2023 at 21:29)
#7506 aesop timeout (6 messages, latest: Dec 08 2023 at 20:11)
#6582 (7 messages, latest: Dec 08 2023 at 17:46)
#8559 Character module (5 messages, latest: Dec 08 2023 at 15:42)
#8614 and #8615 (derivatives, fundamental thm of calculus) (11 messages, latest: Dec 07 2023 at 19:56)
#8480 (1 message, latest: Dec 07 2023 at 17:19)
#8178 space after ← (47 messages, latest: Dec 04 2023 at 16:55)
#7815 some matrix results (2 messages, latest: Dec 04 2023 at 14:41)
#8751 Euler products (1 message, latest: Dec 04 2023 at 11:17)
Quick style PRs (2 messages, latest: Dec 03 2023 at 07:50)
#8721 Binary products of finite measures (3 messages, latest: Dec 02 2023 at 23:18)
#8774 special unitary group (3 messages, latest: Dec 01 2023 at 19:34)
#8725 review normed group structure on ContinuousLinearMap (2 messages, latest: Dec 01 2023 at 17:40)
#7810 LibrarySearch test failures (5 messages, latest: Nov 30 2023 at 13:51)
#8642 Lemmas about List.map (1 message, latest: Nov 30 2023 at 11:46)
#7843 Homomorphism from centre into centroid (1 message, latest: Nov 28 2023 at 19:17)
#8071 Matroid axioms (4 messages, latest: Nov 28 2023 at 17:41)
#8397 Lie group structure on units of a complete normed ring (1 message, latest: Nov 28 2023 at 08:28)
#8449 Bounds for Dirichlet character values (23 messages, latest: Nov 27 2023 at 20:37)
#8584 TensorProduct.liftAddHom (8 messages, latest: Nov 27 2023 at 16:55)
#7394 Tensor products of graded algebras (1 message, latest: Nov 27 2023 at 12:34)
#6856 match_xYz (25 messages, latest: Nov 25 2023 at 22:17)
#8440 Dirichlet characters (1 message, latest: Nov 23 2023 at 09:49)
#7060 Separate commutative and associative multiplication (1 message, latest: Nov 21 2023 at 20:39)
#8498 uniqueness of weak limits of finite Borel measures (4 messages, latest: Nov 20 2023 at 09:17)
✔ #8524 easy liminf / limsup lemmas (3 messages, latest: Nov 20 2023 at 08:10)
hint tactic (10 messages, latest: Nov 19 2023 at 02:43)
#8410 Euler products (1 message, latest: Nov 18 2023 at 11:06)
Dirichlet characters (10 messages, latest: Nov 17 2023 at 20:27)
✔ #8406 IsIntegral dot notation, noncomm generalization &… (2 messages, latest: Nov 17 2023 at 17:46)
#8086 Removing Add.add from theorem statements (6 messages, latest: Nov 16 2023 at 14:27)
#8189 add Trans instance for List.Perm and a lemma on Lists (1 message, latest: Nov 16 2023 at 08:44)
#8409 (1 message, latest: Nov 15 2023 at 20:03)
#8107 (3 messages, latest: Nov 15 2023 at 18:55)
#7801 split LinearAlgebra.Basic (2 messages, latest: Nov 15 2023 at 09:47)
#7905 instance for non-dependent FunLike (34 messages, latest: Nov 15 2023 at 09:38)
#8389 split MeasureSpace.lean into 3 files (20 messages, latest: Nov 13 2023 at 21:52)
#8325 (3 messages, latest: Nov 13 2023 at 18:44)
#7903 define UnboundedSpace (11 messages, latest: Nov 11 2023 at 18:20)
#8252 smooth numbers (1 message, latest: Nov 11 2023 at 10:44)
#6363 feat: More to #find! (18 messages, latest: Nov 11 2023 at 00:25)
#8068 (1 message, latest: Nov 06 2023 at 16:23)
#7341 updateFinset (19 messages, latest: Nov 06 2023 at 12:47)
#7790 polyrith radicals (7 messages, latest: Nov 03 2023 at 15:56)
#7894 VCSP theory RFC (3 messages, latest: Nov 03 2023 at 13:45)
#6996 Define the centre … for non-associative algebras (26 messages, latest: Nov 03 2023 at 10:59)
#7885 add namespace UpperHalfPlane.ModularGroup (10 messages, latest: Nov 01 2023 at 09:03)
#8029: replace ContinuousMap.Homotopy with Function.Homotopy (14 messages, latest: Oct 31 2023 at 18:04)
#7860 ClosableCompactSubsetOpenSpace (1 message, latest: Oct 31 2023 at 15:39)
#7685 peel tactic (13 messages, latest: Oct 30 2023 at 16:41)
#5376 reduce_mod_char tactic (6 messages, latest: Oct 30 2023 at 15:10)
#8006 ofNat lemmas (11 messages, latest: Oct 29 2023 at 18:34)
#7883 rings vs orders (22 messages, latest: Oct 26 2023 at 00:26)
#7404 VCSP (21 messages, latest: Oct 24 2023 at 13:32)
#7854 split CategoryTheory/Sites/SheafOfTypes (2 messages, latest: Oct 23 2023 at 22:06)
#5901 PGame.Identical (1 message, latest: Oct 22 2023 at 07:00)
#7506 inferInstance issues (17 messages, latest: Oct 20 2023 at 21:02)
#7606, adaptations for lean4#2644 (34 messages, latest: Oct 20 2023 at 13:12)
!4#4593 (23 messages, latest: Oct 20 2023 at 10:17)
#7205 pp.beta (33 messages, latest: Oct 19 2023 at 14:00)
✔ #7664 and #7723: boring lemmas about quadratic forms (2 messages, latest: Oct 19 2023 at 13:01)
#7552 analytic functions (6 messages, latest: Oct 18 2023 at 11:10)
#7040 Uniformly and strongly convex functions (4 messages, latest: Oct 18 2023 at 04:55)
#7586 / !3#17142: polyrith crash (7 messages, latest: Oct 18 2023 at 01:44)
#7486 antidiagonal (21 messages, latest: Oct 11 2023 at 15:36)
#6578 compact subsets in products as limits in Profinite (3 messages, latest: Oct 10 2023 at 15:45)
#6223 the Unfolding Trick (56 messages, latest: Oct 07 2023 at 09:52)
#7326 suppress_compilation tactic (17 messages, latest: Oct 04 2023 at 08:36)
#7368 lean4checker (2 messages, latest: Oct 03 2023 at 02:05)
std4#243 (7 messages, latest: Oct 02 2023 at 08:58)
#7433 cycleTypes of perm (2 messages, latest: Sep 29 2023 at 15:03)
✔ #7367 CONTRIBUTING.md (3 messages, latest: Sep 29 2023 at 14:19)
#6589 LocallyConstant.piecewise' (3 messages, latest: Sep 29 2023 at 13:10)
#7319 harmonic number not an integer (15 messages, latest: Sep 28 2023 at 22:46)
super factorial and vandermonde determinant (5 messages, latest: Sep 26 2023 at 19:35)
#6310 OrderedAddCommMonoidWithOne (17 messages, latest: Sep 24 2023 at 01:09)
#7203 R\[A\] for AddMonoidAlgebra R A (1 message, latest: Sep 16 2023 at 06:00)
#7148 bump to nightly-2023-09-14 (2 messages, latest: Sep 15 2023 at 00:27)
#6755 UniqueProds: subsingleton and MulOpposite lemmas (6 messages, latest: Sep 14 2023 at 12:43)
!3#18732 Bergelson intersectivity (10 messages, latest: Sep 14 2023 at 06:33)
#6998 (8 messages, latest: Sep 11 2023 at 19:16)
#6385 context-free grammars (25 messages, latest: Sep 11 2023 at 10:20)
#6880 Zeckendorf's Theorem (2 messages, latest: Sep 07 2023 at 20:32)
#3464 nondeterminism monad (8 messages, latest: Sep 07 2023 at 09:19)
#6437 pointed cones (12 messages, latest: Sep 05 2023 at 15:31)
#6870 change junk value for supremum of unbounded sets (5 messages, latest: Sep 05 2023 at 13:40)
#6896 regular and extensive coverages (1 message, latest: Sep 05 2023 at 09:48)
#6151 adn #6153 lake exe graph (4 messages, latest: Sep 05 2023 at 09:20)
#232 (4 messages, latest: Sep 05 2023 at 06:02)
#6568 and #6569 (3 messages, latest: Sep 04 2023 at 16:38)
#6342 (14 messages, latest: Sep 04 2023 at 14:19)
#6864 (4 messages, latest: Sep 03 2023 at 07:23)
fix ODE theorem (1 message, latest: Sep 03 2023 at 05:01)
#6588 nilpotent matrices have nilpotent trace (3 messages, latest: Sep 02 2023 at 19:34)
#6447 Right exactness of tensor product (55 messages, latest: Sep 02 2023 at 10:10)
✔ #6920 Correct a name (2 messages, latest: Sep 02 2023 at 09:32)
#6808 vertex replacement (4 messages, latest: Sep 01 2023 at 03:25)
#6866 (12 messages, latest: Sep 01 2023 at 02:01)
#6728 sorting lemmas (1 message, latest: Aug 31 2023 at 21:31)
#6729 Add lemmas to working with LiftRel (11 messages, latest: Aug 31 2023 at 11:47)
✔ #6756 mem_doubleton (20 messages, latest: Aug 29 2023 at 20:52)
docker (1 message, latest: Aug 29 2023 at 18:41)
#6842, deleting an empty file (1 message, latest: Aug 29 2023 at 09:10)
#6736 Bool consistency. (18 messages, latest: Aug 28 2023 at 22:18)
#6663 Create direct versions of getLeft? and getRight? (1 message, latest: Aug 28 2023 at 09:49)
#6714 Generalisation of nodal polynomial. (1 message, latest: Aug 28 2023 at 09:46)
#6372 maps from the unitization of non-unital subobjects (5 messages, latest: Aug 25 2023 at 18:00)
#6696 clique folder (6 messages, latest: Aug 24 2023 at 07:24)
#5930 Ring.divide (4 messages, latest: Aug 22 2023 at 17:15)
#5858 Profinite is precoherent (1 message, latest: Aug 22 2023 at 10:53)
#5808 projectivity of Stonean spaces in CompHaus (1 message, latest: Aug 22 2023 at 10:34)
#6365 Game to SetTheory.Game (2 messages, latest: Aug 21 2023 at 15:31)
#6404 defining initial ordinals (9 messages, latest: Aug 21 2023 at 13:39)
#6683, #6684, #6702 pp_with_univ (3 messages, latest: Aug 21 2023 at 12:08)
#6507 matrix equality of strongly regular graphs (1 message, latest: Aug 20 2023 at 02:00)
#6344 product of distinct factors of a squarefree Nat (4 messages, latest: Aug 18 2023 at 13:39)
#6637 delete instFunLikeDual (5 messages, latest: Aug 18 2023 at 13:37)
#3757 fail_if_no_progress (1 message, latest: Aug 18 2023 at 09:45)
std4#120 ext? and ext!? (2 messages, latest: Aug 17 2023 at 10:51)
#4773 base change (28 messages, latest: Aug 17 2023 at 10:14)
#5803 Legendre's theorem (32 messages, latest: Aug 16 2023 at 22:58)
#6136 WithLp for products (4 messages, latest: Aug 15 2023 at 16:32)
#6487 Matrix multiplication (2 messages, latest: Aug 15 2023 at 08:52)
#6456 protect Function.Commute (30 messages, latest: Aug 14 2023 at 13:50)
[#6370 Type](topic/.236370.20Type.html) (63 messages, latest: Aug 11 2023 at 16:25)
#6409 WithLp (7 messages, latest: Aug 11 2023 at 10:24)
#5960 Dirichlet's unit theorem (1 message, latest: Aug 10 2023 at 01:06)
#6386 Analytic structure groupoid (1 message, latest: Aug 09 2023 at 11:05)
#5969 discrete subsets and subgroups (3 messages, latest: Aug 08 2023 at 17:01)
#6286 Nöbeling's theorem (3 messages, latest: Aug 08 2023 at 13:00)
#5634 Gleason's theorem (2 messages, latest: Aug 08 2023 at 04:40)
#6405 and #6360 (12 messages, latest: Aug 07 2023 at 21:06)
#6035 Generalize rings in TensorProduct/Tower (4 messages, latest: Aug 07 2023 at 10:26)
#5942 Add a DecidableEq instance for Polynomial (61 messages, latest: Aug 06 2023 at 23:14)
#5959 instance priority changes (2 messages, latest: Aug 06 2023 at 14:13)
#6333 fixing #eval on multiset (1 message, latest: Aug 03 2023 at 13:05)
#5859 (4 messages, latest: Aug 02 2023 at 13:12)
#4989 reflexive modules and perfect pairings (10 messages, latest: Aug 02 2023 at 08:16)
#6145 lower cancel priorities (1 message, latest: Aug 01 2023 at 20:58)
#6051 rank of a matrix unaffected by multiplication with inv (5 messages, latest: Aug 01 2023 at 11:41)
#6057 - Add equivariant morphisms and adjust linear maps (9 messages, latest: Jul 31 2023 at 17:40)
!3#18887 feat(analysis/specific_limits/complex) (11 messages, latest: Jul 31 2023 at 17:22)
#6163 Normal Closure (5 messages, latest: Jul 31 2023 at 16:34)
#5805 Use FunLike for OrderHom (5 messages, latest: Jul 31 2023 at 13:41)
#6260 ← !3#15296 (13 messages, latest: Jul 31 2023 at 09:55)
!3#18863 Unfolding Trick (15 messages, latest: Jul 30 2023 at 15:16)
std4#160 case : t => tac tactic to search for goals by type (1 message, latest: Jul 30 2023 at 09:28)
!3#17923 (4 messages, latest: Jul 30 2023 at 07:27)
#5748 NumberField Units (5 messages, latest: Jul 30 2023 at 01:38)
#6221 compute_degree (2 messages, latest: Jul 29 2023 at 17:25)
#5762 and #5763 explicit limits in CompHaus and Profinite (3 messages, latest: Jul 29 2023 at 09:17)
!3#15260 small sets of pre-games / games / surreals are bdd (1 message, latest: Jul 28 2023 at 07:38)
!3#17828 feat(combinatorics/quiver/covering) (3 messages, latest: Jul 28 2023 at 07:28)
#4871 StarOrderedRing.positive (51 messages, latest: Jul 28 2023 at 03:06)
!3#18230 Positivity of linear maps (35 messages, latest: Jul 27 2023 at 22:08)
#6187 split RingTheory.TensorProduct (1 message, latest: Jul 27 2023 at 21:58)
!3#18789 (8 messages, latest: Jul 27 2023 at 07:33)
#5980 says combinator (3 messages, latest: Jul 27 2023 at 05:48)
!3#18779 (1 message, latest: Jul 26 2023 at 23:45)
#5766 add IsLocalizedModule.isBaseChange (5 messages, latest: Jul 25 2023 at 21:08)
!3#18289 invariant submodules (3 messages, latest: Jul 25 2023 at 20:48)
#5267 remove conjInvariantSubalgebra (1 message, latest: Jul 25 2023 at 02:41)
mathlib4 PR titles (37 messages, latest: Jul 23 2023 at 23:37)
#6060 – paramerer equality of SRGs (4 messages, latest: Jul 23 2023 at 02:07)
#5671 (2 messages, latest: Jul 21 2023 at 23:12)
#5911 minimals/maximals API (4 messages, latest: Jul 21 2023 at 11:06)
#6026 undergrad.yaml in mathlib4 (5 messages, latest: Jul 20 2023 at 16:14)
#5882 and #6007 compute_degree_le (10 messages, latest: Jul 19 2023 at 15:49)
!4#6002 add integrable_fun_mul_exp_neg_mul_sq (2 messages, latest: Jul 19 2023 at 14:48)
slim_check (17 messages, latest: Jul 19 2023 at 12:33)
#5997 add RingHom.inverse (1 message, latest: Jul 19 2023 at 10:39)
#5862 Kummer's lemma in terms of p-adic valuations (8 messages, latest: Jul 19 2023 at 06:01)
#18300 feat(group_theory/sylow): add inverse to card_eq_mul (24 messages, latest: Jul 12 2023 at 12:22)
#5805 FunLike for OrderHom (1 message, latest: Jul 11 2023 at 14:59)
Lemmas to handle part_enat.card, #19198 (8 messages, latest: Jul 10 2023 at 18:34)
multipliable !3#19219 (37 messages, latest: Jul 10 2023 at 15:22)
✔ #5678 Continuous alternating maps (21 messages, latest: Jul 06 2023 at 20:16)
#5695 Facts about the coherent topology (4 messages, latest: Jul 06 2023 at 08:59)
!4#5647 : colimits and yoneda (4 messages, latest: Jul 03 2023 at 09:59)
#5629 complex differentiable functions are continuously diff (7 messages, latest: Jul 02 2023 at 20:52)
!3#19008 – should be ready (7 messages, latest: Jul 01 2023 at 03:14)
!4#5584 for !4#5409 (1 message, latest: Jul 01 2023 at 03:12)
!4#5032 Analysis.Analytic.Inverse (2 messages, latest: Jun 29 2023 at 04:03)
!4#5468 RepresentationTheory.GroupCohomology.Basic (1 message, latest: Jun 25 2023 at 12:09)
!4#5391 RepresentationTheory.GroupCohomology.Resolution (2 messages, latest: Jun 24 2023 at 17:50)
congrm (3 messages, latest: Jun 21 2023 at 14:08)
#19146 sheaves on manifolds (13 messages, latest: Jun 20 2023 at 15:16)
!4#5083 (1 message, latest: Jun 18 2023 at 12:51)
!4#5205, !4#5213, !4#5215 (2 messages, latest: Jun 18 2023 at 11:58)
!4#5041 RepresentationTheory.Rep (7 messages, latest: Jun 16 2023 at 18:30)
!4#3162 variable! (11 messages, latest: Jun 15 2023 at 07:19)
port AlgebraicGeometry.Scheme !4#5040 (1 message, latest: Jun 14 2023 at 11:48)
#19183 golf (1 message, latest: Jun 14 2023 at 09:26)
!4#4020 CategoryTheory.DifferentialObject (3 messages, latest: Jun 14 2023 at 04:17)
!4#4602 Analysis.InnerProductSpace.TwoDim (2 messages, latest: Jun 12 2023 at 07:57)
!4#4898 MeasureTheory.Function.ConditionalExpectation.Basic (1 message, latest: Jun 09 2023 at 14:16)
!4#4872 Data.Real.Pi.Bounds (5 messages, latest: Jun 09 2023 at 11:19)
#18266 (6 messages, latest: Jun 09 2023 at 08:26)
#18849 inverse of 2×2 block triangular matrices (3 messages, latest: Jun 08 2023 at 18:51)
!4#4723 FieldTheory.Adjoin (15 messages, latest: Jun 08 2023 at 09:39)
!4#3961 (5 messages, latest: Jun 08 2023 at 00:10)
!4#4761 RepresentationTheory.Rep (1 message, latest: Jun 07 2023 at 01:25)
!4#4746 (1 message, latest: Jun 06 2023 at 17:22)
!4#4707 Algebra.Module.PID (7 messages, latest: Jun 06 2023 at 10:35)
port CategoryTheory.WithTerminal !4#2630 (3 messages, latest: Jun 05 2023 at 12:16)
!4#4653 Trigonometric.Deriv (13 messages, latest: Jun 05 2023 at 08:47)
#19149 split open immersion (1 message, latest: Jun 04 2023 at 16:23)
!4#3361 (9 messages, latest: Jun 03 2023 at 16:44)
!4#4560 (2 messages, latest: Jun 01 2023 at 21:08)
chore(ring_theory/derivation): split file #19138 (1 message, latest: Jun 01 2023 at 19:05)
!4#4530 (1 message, latest: Jun 01 2023 at 05:48)
#19054 (sums of two squares) (1 message, latest: May 31 2023 at 19:14)
newer ports (61 messages, latest: May 31 2023 at 16:20)
#18820 Adjoint for unbounded operators (5 messages, latest: May 30 2023 at 21:44)
StrictSeries !4#3858, !4#3852 (21 messages, latest: May 29 2023 at 19:36)
#18979 (9 messages, latest: May 28 2023 at 18:02)
!4#3987 Topology.Gluing (3 messages, latest: May 28 2023 at 10:28)
!4#4200 SProd (1 message, latest: May 28 2023 at 02:49)
!4#4357 coherence tactic (1 message, latest: May 27 2023 at 16:25)
!4#2508 Introduce the Scott topology on a preorder (1 message, latest: May 26 2023 at 06:56)
#17298 continuous seminorms (1 message, latest: May 25 2023 at 13:17)
#2770 Kruskal-Katona theorem and some related results (7 messages, latest: May 24 2023 at 08:26)
!#4231 RingTheory.Localization.Integral (1 message, latest: May 23 2023 at 10:16)
#18857 resolve the splitting field diamond (8 messages, latest: May 22 2023 at 12:49)
!4#4169 LinearAlgebra.Matrix.Charpoly.Coeff (5 messages, latest: May 22 2023 at 01:33)
#18913 feat(analysis/convex/cone/proper): define proper cone (1 message, latest: May 20 2023 at 23:03)
!4#4075 Topology.ContinuousFunction.Bounded (22 messages, latest: May 20 2023 at 16:36)
!4#4106 port RingTheory.PolynomialAlgebra (4 messages, latest: May 20 2023 at 14:42)
✔ !4#4094 Algebra.Category.Mon.FilteredColimits (9 messages, latest: May 20 2023 at 00:46)
#18417 and port-status#data/fintype/quotient (15 messages, latest: May 19 2023 at 18:19)
add Mathlib.Tactic.Common, and import !4#4056 (7 messages, latest: May 19 2023 at 11:56)
#19043 split convex.cone (1 message, latest: May 19 2023 at 05:14)
!4#3333 Data.ZMod.Quotient (78 messages, latest: May 18 2023 at 21:32)
✔ !4#3828 (2 messages, latest: May 18 2023 at 17:12)
!4#2808 CategoryTheory.Monoidal.Free.Basic (6 messages, latest: May 18 2023 at 12:44)
!4#2994 NumberTheory.LegendreSymbol.MulCharacter (20 messages, latest: May 17 2023 at 23:38)
!4#4010 Combinatorics.SimpleGraph.Finsubgraph (1 message, latest: May 17 2023 at 11:46)
#18865 and !4#3634 (2 messages, latest: May 16 2023 at 16:09)
feat: port NumberTheory.Padics.PadicNumbers !4#3095 (7 messages, latest: May 16 2023 at 09:31)
!4#3988 Analysis.SpecialFunctions.Exp (3 messages, latest: May 15 2023 at 23:39)
Analysis.Complex.Basic !4#3930 (1 message, latest: May 15 2023 at 13:14)
older ports (23 messages, latest: May 15 2023 at 08:25)
Incomplete work (14 messages, latest: May 12 2023 at 11:12)
✔ #18945 deriv of polynomial aeval (6 messages, latest: May 11 2023 at 19:31)
!4#2323 – mono (3 messages, latest: May 11 2023 at 02:15)
rewrites tactic, !4#3119 (3 messages, latest: May 10 2023 at 10:54)
✔ #18821 (improper integrals) (4 messages, latest: May 05 2023 at 05:18)
#18940 (1 message, latest: May 05 2023 at 00:20)
!4#3737 Data.Complex.Module (1 message, latest: May 02 2023 at 07:39)
old mathlib3 PRs (22 messages, latest: Apr 28 2023 at 13:16)
!4#3651 Analysis.NormedSpace.AffineIsometry (5 messages, latest: Apr 25 2023 at 17:05)
!4#3640 fixing #aligns (5 messages, latest: Apr 25 2023 at 14:52)
!4#1204 Data.Vector3 (3 messages, latest: Apr 22 2023 at 23:28)
#18643 bound for the n-th derivative of a composition (1 message, latest: Apr 22 2023 at 15:22)
!4#3550 (1 message, latest: Apr 20 2023 at 15:56)
!4#3119 (2 messages, latest: Apr 20 2023 at 06:34)
!4#2920 backtracking code in solve_by_elim (5 messages, latest: Apr 18 2023 at 03:33)
!4#2898 propose (3 messages, latest: Apr 18 2023 at 03:29)
#3452 Timeout (4 messages, latest: Apr 17 2023 at 15:17)
#18802 boring star lemmas (2 messages, latest: Apr 16 2023 at 20:59)
!4#1238 (12 messages, latest: Apr 15 2023 at 20:35)
!4#3063 – linter fails in 165 places (5 messages, latest: Apr 15 2023 at 06:56)
Data.Dlist !4#1498 (2 messages, latest: Apr 14 2023 at 10:38)
!4#1707 norm_num for scientific notation (3 messages, latest: Apr 12 2023 at 06:52)
#13149 UV-compressing reduces the size of the shadow (9 messages, latest: Apr 11 2023 at 23:45)
!4#3378 (2 messages, latest: Apr 11 2023 at 14:08)
✔ #18710 compactly supported functions are dense in L^p (2 messages, latest: Apr 10 2023 at 17:49)
Control.Fold !4#2341 (1 message, latest: Apr 10 2023 at 12:28)
!4#3303 dot notation aliases (9 messages, latest: Apr 10 2023 at 10:00)
!4#3354 (LinearAlgebra.Dimension) (7 messages, latest: Apr 10 2023 at 07:29)
#18766 (linear algebra) and related PRs (6 messages, latest: Apr 10 2023 at 00:54)
!4#3247 (72 messages, latest: Apr 09 2023 at 21:00)
!4#3280 (2 messages, latest: Apr 08 2023 at 13:33)
!4#3320 (15 messages, latest: Apr 07 2023 at 05:00)
#18626 Pell's equation (2 messages, latest: Apr 06 2023 at 21:06)
!4#3242 (1 message, latest: Apr 06 2023 at 11:56)
!4#3287 (1 message, latest: Apr 05 2023 at 11:55)
!4#2969 simps bug? (Monad.Basic) (7 messages, latest: Apr 05 2023 at 10:46)
!4#3204 simps bug (Grothendieck construction) (4 messages, latest: Apr 05 2023 at 01:09)
#18651 (1 message, latest: Apr 05 2023 at 00:02)
#15041 constrain universes (11 messages, latest: Apr 04 2023 at 14:55)
!4#3225 MvPolynomial.Funext (2 messages, latest: Apr 03 2023 at 01:40)
#2819 (27 messages, latest: Mar 31 2023 at 16:51)
!4#3114 (1 message, latest: Mar 30 2023 at 21:48)
#17719 Riemann-Lebesgue lemma (13 messages, latest: Mar 30 2023 at 12:22)
#10140 (11 messages, latest: Mar 30 2023 at 09:06)
#18686 (1 message, latest: Mar 30 2023 at 04:11)
#18688 (1 message, latest: Mar 30 2023 at 04:09)
!4#3130 (4 messages, latest: Mar 29 2023 at 22:20)
#14324 define natural multiplication (8 messages, latest: Mar 29 2023 at 16:12)
#15326 Renaming is_self_adjoint (124 messages, latest: Mar 29 2023 at 13:08)
!4#2945 (3 messages, latest: Mar 29 2023 at 09:19)
!4#3155 (9 messages, latest: Mar 29 2023 at 08:56)
#18442 (1 message, latest: Mar 28 2023 at 21:43)
!4#2424 (6 messages, latest: Mar 28 2023 at 11:31)
#18583 ¬(inner_product_space extends normed_add_comm_group) (2 messages, latest: Mar 23 2023 at 18:20)
!4#2692 (2 messages, latest: Mar 23 2023 at 05:41)
mathlib4#2204 port success_if_fail_with_msg (5 messages, latest: Mar 22 2023 at 00:56)
#15905 mv_polynomial division (2 messages, latest: Mar 21 2023 at 11:47)
#18568 (5 messages, latest: Mar 19 2023 at 19:23)
#17972 Borel hierarchy (6 messages, latest: Mar 18 2023 at 14:34)
#15738 lemmas for arbitrary concrete matrices (1 message, latest: Mar 16 2023 at 16:23)
#18517 Insert for directed sets (3 messages, latest: Mar 12 2023 at 12:11)
#18460 Legendre's theorem on rational approximation (1 message, latest: Mar 09 2023 at 03:27)
!4#2103 Rat functionality for positivity (2 messages, latest: Mar 08 2023 at 11:19)
#16794 (3 messages, latest: Mar 08 2023 at 01:25)
!4#1897 (1 message, latest: Mar 07 2023 at 21:50)
✔ !4#2564 and !4#2594 (3 messages, latest: Mar 07 2023 at 16:45)
#18379 action of SL(2, ℝ) on upper half plane is isometric (4 messages, latest: Mar 01 2023 at 19:24)
#18448 Introduce the Scott topology on a preorder (7 messages, latest: Feb 28 2023 at 11:27)
!4#2464 Filter.EventuallyLe (1 message, latest: Feb 28 2023 at 10:25)
#18433 Sections of cofiltered systems (3 messages, latest: Feb 27 2023 at 19:40)
#18440 removed obviously tactic for data fields (2 messages, latest: Feb 23 2023 at 10:01)
✔ More precise porting SHAs, leanprover-community/mathpor… (36 messages, latest: Feb 22 2023 at 04:57)
✔ #18414 split topology.algebra.infinite_sum (6 messages, latest: Feb 16 2023 at 01:09)
#18410 An infinite graph has ≥one end (1 message, latest: Feb 14 2023 at 14:54)
✔ #18382 and #18347 easy results on quaternions (3 messages, latest: Feb 14 2023 at 13:28)
✔ !4#2178 data.fin.basic forwardport (2 messages, latest: Feb 11 2023 at 11:31)
!4#2145 continuity tactic (1 message, latest: Feb 10 2023 at 09:40)
#10255 Direct sums of tensor powers (1 message, latest: Feb 08 2023 at 12:02)
Szemerédi Regularity Lemma (5 messages, latest: Feb 05 2023 at 09:40)
#18312 review topology/order (45 messages, latest: Jan 30 2023 at 23:45)
Ends of a simple graph #17857 (5 messages, latest: Jan 30 2023 at 13:44)
#16870 the return of the Dedekind-Kummer theorem (7 messages, latest: Jan 25 2023 at 16:10)
#13187 Chebyshev's sum inequality (17 messages, latest: Jan 22 2023 at 11:50)
group_theory/subgroup/basic reduction #17862 (12 messages, latest: Jan 19 2023 at 16:15)
geometry PRs ping (14 messages, latest: Jan 17 2023 at 23:33)
#17961 s ∩ t * s ∪ t ⊆ s * t (6 messages, latest: Jan 17 2023 at 09:56)
#18093 adding back bilin_form_of_real_inner (1 message, latest: Jan 17 2023 at 00:09)
#18173 Getting rid of enat (2 messages, latest: Jan 16 2023 at 21:14)
#18021 generalizing theory of minpoly (43 messages, latest: Jan 14 2023 at 12:30)
✔ mathlib4#1419 gitpod config (1 message, latest: Jan 11 2023 at 21:10)
mathlib4#1419 gitpod config (14 messages, latest: Jan 11 2023 at 20:14)
#18121: lift f (x ⊗ₜ y) = f x y by rfl (1 message, latest: Jan 10 2023 at 16:18)
#17948 Improve finset/multiset lemma names (4 messages, latest: Jan 09 2023 at 13:30)
mathlib4#856 refactor of solve_by_elim (11 messages, latest: Jan 09 2023 at 07:10)
#18079 PR issue? (1 message, latest: Jan 07 2023 at 18:11)
✔ #18013 filtered categories (2 messages, latest: Dec 31 2022 at 15:34)
non-normalizable gcd_monoid (14 messages, latest: Dec 31 2022 at 05:41)
#18011 well-approximable numbers and Gallagher's zero-one la (2 messages, latest: Dec 30 2022 at 10:03)
#15111 (1 message, latest: Dec 29 2022 at 19:54)
#18013 filtered categories (1 message, latest: Dec 29 2022 at 07:31)
✔ #17988 timeout? (8 messages, latest: Dec 26 2022 at 08:15)
#17988 timeout? (6 messages, latest: Dec 21 2022 at 20:26)
#17985 various results split out from proof of Gallagher's t (6 messages, latest: Dec 21 2022 at 13:35)
✔ Lean 3 (2 messages, latest: Dec 21 2022 at 09:34)
Lean 3 (5 messages, latest: Dec 21 2022 at 08:49)
#17426 Introduce the lower topology on a preorder (1 message, latest: Dec 20 2022 at 05:50)
✔ Quivers: #17618 #17617 and #17665 (6 messages, latest: Dec 18 2022 at 20:59)
Quivers: #17618 #17617 and #17665 (48 messages, latest: Dec 16 2022 at 16:26)
#17916 assert_not_exists problems (1 message, latest: Dec 14 2022 at 11:21)
#17548 Dold-Kan correspondence (4 messages, latest: Dec 13 2022 at 16:21)
#17832 (10 messages, latest: Dec 12 2022 at 08:42)
#17767 uniform continuity of functions in C₀(X, Y) (6 messages, latest: Dec 12 2022 at 08:35)
#17749 submodules are convex cones (1 message, latest: Dec 11 2022 at 22:05)
#16975 Topology and upper/lower sets (2 messages, latest: Dec 11 2022 at 12:40)
#16715 ping (1 message, latest: Dec 08 2022 at 08:39)
mathlib4#896 (1 message, latest: Dec 07 2022 at 22:58)
#17831 refactor is_domain - deterministic timeout (17 messages, latest: Dec 07 2022 at 21:56)
#17212 (2 messages, latest: Dec 07 2022 at 09:15)
mathlib4#804 Order.Hom.Basic (3 messages, latest: Dec 06 2022 at 02:49)
#17779 injectivity of fin.cons (1 message, latest: Dec 06 2022 at 00:47)
This month in mathlib (10 messages, latest: Dec 05 2022 at 15:12)
#17747 set.prod lemmas (1 message, latest: Dec 05 2022 at 01:44)
#17544 ergodicity of zsmul on the additive circle (1 message, latest: Dec 01 2022 at 19:44)
#17750 - split up algebra.ring.equiv (1 message, latest: Dec 01 2022 at 14:07)
[chore(group_theory/sub): avoid fintype dependencies #17762](topic/chore(group_theory.2Fsub).3A.20avoid.20fintype.20dependencies.20.2317762.html) (1 message, latest: Nov 30 2022 at 15:26)
#16930 and #16931 refactor prime and projective spectra (2 messages, latest: Nov 30 2022 at 14:53)
#17716 is_cancel_mul_zero (2 messages, latest: Nov 30 2022 at 09:38)
mathlib4#792 (1 message, latest: Nov 30 2022 at 02:47)
#17498 boring list lemmas (1 message, latest: Nov 30 2022 at 00:24)
#17462 fundamental domain for rational rotations in circle (1 message, latest: Nov 28 2022 at 09:22)
#17717 (need help) finsupp.map_range_sub (19 messages, latest: Nov 27 2022 at 19:19)
#13250 Modular form definition (11 messages, latest: Nov 27 2022 at 15:13)
#17453 Bump functions (1 message, latest: Nov 27 2022 at 11:29)
mathlib4#659 (2 messages, latest: Nov 26 2022 at 08:11)
#15996: Qcqs lemma (4 messages, latest: Nov 24 2022 at 12:06)
#17438 add fundamental domain constructor (3 messages, latest: Nov 23 2022 at 14:04)
#17674 mathlib4 sync bot (4 messages, latest: Nov 22 2022 at 08:12)
#17499 feat(data/list/big_operators) (11 messages, latest: Nov 21 2022 at 20:41)
compact limits of holomorphic functions (6 messages, latest: Nov 21 2022 at 15:43)
#17321 finite-order points on the circle (2 messages, latest: Nov 21 2022 at 10:51)
#17545 category theory refactor (1 message, latest: Nov 18 2022 at 09:13)
#17562 (1 message, latest: Nov 18 2022 at 07:47)
#17271 (1 message, latest: Nov 17 2022 at 17:31)
#17249 continuity of seminorms (3 messages, latest: Nov 16 2022 at 10:33)
#17403 (1 message, latest: Nov 16 2022 at 09:03)
#17200 (1 message, latest: Nov 15 2022 at 23:44)
#17079 (1 message, latest: Nov 15 2022 at 23:42)
#13250 Modular form defiinition (38 messages, latest: Nov 15 2022 at 11:00)
lean#770 (11 messages, latest: Nov 15 2022 at 10:45)
#17519 (5 messages, latest: Nov 15 2022 at 10:19)
#17507 (2 messages, latest: Nov 14 2022 at 22:02)
✔ #17190 feat(data/list/{basic,join}) (1 message, latest: Nov 14 2022 at 12:11)
refactoring PRs in algebra/ (4 messages, latest: Nov 14 2022 at 09:25)
mathlib4#550 (4 messages, latest: Nov 14 2022 at 01:37)
doc-gen#172 instance lists for pi and Type (7 messages, latest: Nov 14 2022 at 00:10)
mathlib4#572 (1 message, latest: Nov 13 2022 at 23:50)
#17508 (4 messages, latest: Nov 13 2022 at 21:27)
#17190 feat(data/list/{basic,join}) (15 messages, latest: Nov 13 2022 at 10:34)
#17470 (1 message, latest: Nov 12 2022 at 21:57)
#17030 volume_preimage_coe (2 messages, latest: Nov 11 2022 at 22:12)
#16434 Redefining disjoint and codisjoint (6 messages, latest: Nov 11 2022 at 16:17)
Simple PRs (2 messages, latest: Nov 09 2022 at 01:31)
#17064 Add is_localized_module.mk' (1 message, latest: Nov 08 2022 at 11:53)
#16523 #16525 ring lemmas (2 messages, latest: Nov 08 2022 at 07:42)
doc-gen#163 - reverse instance lookup (20 messages, latest: Nov 04 2022 at 18:41)
#16491 Japanese bracket and integrability (4 messages, latest: Nov 04 2022 at 00:21)
#17048 classes for coercions that are homomorphisms (8 messages, latest: Nov 02 2022 at 20:01)
Lie group and ODEs (5 messages, latest: Nov 01 2022 at 09:07)
#17027 Riesz-Markov-Kakutani (20 messages, latest: Oct 30 2022 at 11:15)
#17023 Multiplicativise file (1 message, latest: Oct 30 2022 at 11:14)
#16756 Schwartz derivative (9 messages, latest: Oct 28 2022 at 10:28)
#15880 Cauchy induction (1 message, latest: Oct 27 2022 at 05:53)
#17046 define ergodic maps / measures (3 messages, latest: Oct 27 2022 at 05:42)
✔ #17133 removing/adding ∅ from/to a topological basis (1 message, latest: Oct 27 2022 at 05:41)
#17133 removing/adding ∅ from/to a topological basis (1 message, latest: Oct 26 2022 at 21:34)
#17031 the volume measure on the additive circle is doubling (1 message, latest: Oct 26 2022 at 14:43)
reducing imports to algebra.invertible (1 message, latest: Oct 26 2022 at 03:41)
#16757 lemmas about cyclotomic extensions (1 message, latest: Oct 25 2022 at 22:02)
[✔ #16317 Multinomial theorem (was #16744 Multinomial for…](topic/.E2.9C.94.20.2316317.20.20Multinomial.20theorem.20(was.20.2316744.20Multinomial.20for.2E.2E.2E.html) (17 messages, latest: Oct 24 2022 at 21:07)
#16658 (1 message, latest: Oct 24 2022 at 21:04)
[#16317 Multinomial theorem (was #16744 Multinomial for…](topic/.2316317.20.20Multinomial.20theorem.20(was.20.2316744.20Multinomial.20for.2E.2E.2E.html) (7 messages, latest: Oct 24 2022 at 17:42)
#16617 @⟨p1, p2⟩ patterns in rcases (5 messages, latest: Oct 23 2022 at 12:30)
#16958 Distance between constant functions (1 message, latest: Oct 23 2022 at 12:17)
#16763 Binary map of option (1 message, latest: Oct 23 2022 at 09:45)
#17109 Quotients of groupoids (1 message, latest: Oct 22 2022 at 06:28)
#16487 volume form, its prerequisites and consequences (10 messages, latest: Oct 21 2022 at 09:57)
#16087 Covering Spaces (2 messages, latest: Oct 21 2022 at 08:59)
mathlib4 porting PRs (3 messages, latest: Oct 20 2022 at 00:35)
#16134 (3 messages, latest: Oct 19 2022 at 09:43)
#16944 Function.extend_apply_of_unique (5 messages, latest: Oct 19 2022 at 07:33)
#16833 define conductor ideal and some basic theory (19 messages, latest: Oct 18 2022 at 22:01)
#17049 (2 messages, latest: Oct 18 2022 at 16:06)
#17009 (1 message, latest: Oct 18 2022 at 06:10)
#16088 Notation for restriction of sections (6 messages, latest: Oct 16 2022 at 15:25)
#15689 Adding "infimum separation" (53 messages, latest: Oct 14 2022 at 12:57)
mathlib-tools#126 (7 messages, latest: Oct 14 2022 at 11:57)
✔ #15331 (3 messages, latest: Oct 13 2022 at 11:13)
mathlib4#461 (7 messages, latest: Oct 13 2022 at 11:02)
#16819 define filter.blimsup, filter.bliminf (25 messages, latest: Oct 13 2022 at 09:18)
#16945 Dependent induction for submodules (1 message, latest: Oct 13 2022 at 08:02)
✔ #16641 (1 message, latest: Oct 11 2022 at 16:50)
✔ #16903 fix timeout (1 message, latest: Oct 11 2022 at 16:29)
#16641 (1 message, latest: Oct 11 2022 at 16:21)
#16607 ennreal lemmas (1 message, latest: Oct 11 2022 at 13:52)
#16903 fix timeout (1 message, latest: Oct 11 2022 at 05:45)
#16599 is_closed.interior_union (4 messages, latest: Oct 10 2022 at 22:44)
cleaning up algebra.order.ring and dependencies (21 messages, latest: Oct 09 2022 at 04:12)
16721 coatoms in a t1_space (10 messages, latest: Oct 09 2022 at 00:45)
#16536 (5 messages, latest: Oct 08 2022 at 18:42)
#16851 speedup (2 messages, latest: Oct 07 2022 at 16:10)
✔ #16844 fix timeout (5 messages, latest: Oct 07 2022 at 14:35)
#16844 fix timeout (4 messages, latest: Oct 07 2022 at 12:17)
mathlib4/433 (1 message, latest: Oct 07 2022 at 04:37)
✔ #15405 Selmer groups of Dedekind domains (1 message, latest: Oct 07 2022 at 04:15)
#16792 (27 messages, latest: Oct 06 2022 at 23:49)
#16150 Inverse of triangular matrix (2 messages, latest: Oct 06 2022 at 17:30)
#16329: unique products (2 messages, latest: Oct 06 2022 at 05:54)
#16744 Multinomial formula (12 messages, latest: Oct 05 2022 at 18:03)
#15968 (3 messages, latest: Oct 05 2022 at 02:22)
✔ PRs forgotten for 2+ weeks (1 message, latest: Oct 04 2022 at 20:28)
#16742 Basics for subgroupoids (1 message, latest: Oct 04 2022 at 14:35)
#16314 stuck in philosophical issue (2 messages, latest: Oct 04 2022 at 14:33)
#16772 well-foundedness of lex/prod order on (d)finsupp/pi (1 message, latest: Oct 03 2022 at 07:03)
#16666 free groupoid on a quiver (9 messages, latest: Oct 03 2022 at 06:57)
#15405 Selmer groups of Dedekind domains (5 messages, latest: Oct 03 2022 at 05:52)
#16123: distrib_smul (6 messages, latest: Oct 01 2022 at 08:30)
#15916 (2 messages, latest: Sep 30 2022 at 01:36)
#16680: ae differentiability of bounded variation functions (1 message, latest: Sep 28 2022 at 16:51)
#16201 define additive circle (3 messages, latest: Sep 27 2022 at 08:09)
#16611 free groupoid on a quiver (10 messages, latest: Sep 27 2022 at 06:24)
[✔ #16655 chore(analysis/normed_space/continuous_affine_ma…](topic/.E2.9C.94.20.2316655.20chore(analysis.2Fnormed_space.2Fcontinuous_affine_ma.2E.2E.2E.html) (3 messages, latest: Sep 26 2022 at 13:24)
#16586 push_neg option (1 message, latest: Sep 26 2022 at 03:21)
#16515 rpow lemmas (9 messages, latest: Sep 24 2022 at 11:44)
#16436 reordering some finset lemmas (1 message, latest: Sep 22 2022 at 07:52)
#16567: make algebra_map a has_lift_t (10 messages, latest: Sep 21 2022 at 05:26)
PRs forgotten for 2+ weeks (4 messages, latest: Sep 20 2022 at 17:39)
#16531: refactor alg_equiv (15 messages, latest: Sep 19 2022 at 15:58)
#15000: the Kummer-Dedekind theorem (29 messages, latest: Sep 16 2022 at 16:28)
#16352 algebra/order/floor.lean refactor (30 messages, latest: Sep 16 2022 at 16:10)
#16347 bundle complex.abs into an absolute_value (1 message, latest: Sep 16 2022 at 12:25)
#15513 Symplectic Group (4 messages, latest: Sep 16 2022 at 12:14)
#16071 Dold-Kan correspondence (2 messages, latest: Sep 13 2022 at 14:41)
#16453 (5 messages, latest: Sep 13 2022 at 07:08)
#16484 Redefine equiv.perm.of_subtype (1 message, latest: Sep 12 2022 at 17:27)
#12746 : Introduce the centroid of a semiring (1 message, latest: Sep 07 2022 at 19:49)
#15769 Continuous partially defined linear maps (1 message, latest: Sep 05 2022 at 16:27)
#15850 The Schwartz space (1 message, latest: Sep 04 2022 at 18:50)
#16313 qify tactic (1 message, latest: Sep 04 2022 at 04:38)
#16195 ssyts (5 messages, latest: Sep 02 2022 at 20:31)
#16120 young_diagram transposes, rows, columns (1 message, latest: Sep 02 2022 at 18:30)
✔ #16127 finsupp.lex (3 messages, latest: Sep 01 2022 at 09:58)
#14703 Poincare metric (7 messages, latest: Aug 31 2022 at 17:27)
#16127 finsupp.lex (22 messages, latest: Aug 31 2022 at 14:24)
#16216 Fix lint in analysis and measure theory (6 messages, latest: Aug 31 2022 at 09:01)
#12988 Far from triangle-free (1 message, latest: Aug 31 2022 at 08:44)
#16141 Positivity extension for coe (3 messages, latest: Aug 30 2022 at 17:45)
#11401 Introduce special Jordan algebras (1 message, latest: Aug 30 2022 at 12:53)
#15983 no-zero divisors and right orderability (2 messages, latest: Aug 29 2022 at 16:24)
#15677 Canonically linear ordered semifields (2 messages, latest: Aug 27 2022 at 08:59)
#16266 (1 message, latest: Aug 26 2022 at 17:14)
#16157 no-zero-divisors in add_monoid_algebras (12 messages, latest: Aug 24 2022 at 18:28)
#15893 Construction of seminorms over fields (3 messages, latest: Aug 24 2022 at 09:29)
Functions bounded at infinity #15009 (9 messages, latest: Aug 24 2022 at 09:18)
#15637 dual of dual cone eq self (2 messages, latest: Aug 24 2022 at 09:15)
#16135 a subgroup of integral multiples ℤ ∙ e is discrete (1 message, latest: Aug 24 2022 at 09:14)
#15676 Move stuff out of algebra.order.with_zero (1 message, latest: Aug 24 2022 at 06:01)
#16172 and #16189, ordered PRs (5 messages, latest: Aug 23 2022 at 17:43)
#11303 Review well-founded set API (1 message, latest: Aug 23 2022 at 14:19)
#15682 (3 messages, latest: Aug 23 2022 at 09:54)
#16152 Moving group seminorms (1 message, latest: Aug 23 2022 at 08:47)
#13749 non-unital subsemirings (13 messages, latest: Aug 23 2022 at 03:41)
#16171 renovate quadratic reciprocity (2 messages, latest: Aug 22 2022 at 19:26)
#16178 (4 messages, latest: Aug 22 2022 at 16:30)
#15906 Matrix conversions of sesquilinear forms (1 message, latest: Aug 21 2022 at 10:59)
#16119 (2 messages, latest: Aug 20 2022 at 17:28)
#16091 ne_locus (3 messages, latest: Aug 19 2022 at 17:24)
#15735 rsufficesI (5 messages, latest: Aug 18 2022 at 14:48)
#15087 Taylor's theorem (7 messages, latest: Aug 18 2022 at 10:53)
#15711 (2 messages, latest: Aug 17 2022 at 05:55)
#15065 polynomial modules (47 messages, latest: Aug 17 2022 at 05:55)
✔ #15977 linter for inst (1 message, latest: Aug 16 2022 at 08:25)
#15462: A variant of finsupp.total for fintypes (2 messages, latest: Aug 15 2022 at 23:21)
#15977 linter for inst (6 messages, latest: Aug 15 2022 at 15:56)
#16004 (4 messages, latest: Aug 15 2022 at 12:56)
#15833 : pi_Lp refactor (11 messages, latest: Aug 14 2022 at 06:44)
#5672 breaks timeout (64 messages, latest: Aug 14 2022 at 00:35)
#16036 is_split_epi/split_epi (2 messages, latest: Aug 13 2022 at 08:44)
#15240 Turn a quiver into a path (2 messages, latest: Aug 12 2022 at 07:03)
#15844 vadd_assoc_class (1 message, latest: Aug 12 2022 at 06:12)
#15717 Extend ×ˢ notation (14 messages, latest: Aug 11 2022 at 21:03)
#16003 Dold-Kan correspondence (1 message, latest: Aug 11 2022 at 12:22)
#15279 Königsberg bridges (13 messages, latest: Aug 11 2022 at 09:22)
#15434 recursion on alist using insert (1 message, latest: Aug 10 2022 at 20:43)
#15449 simplify Cantor normal form definition (1 message, latest: Aug 10 2022 at 20:39)
#14465 basic definitions for subbimodules (5 messages, latest: Aug 09 2022 at 17:44)
#15913 simpler tactic_doc / library_note encoding (8 messages, latest: Aug 09 2022 at 09:27)
#15950 Dold-Kan correspondence (1 message, latest: Aug 09 2022 at 08:37)
✔ #15036 Lagrange interpolant refactor and extension (1 message, latest: Aug 08 2022 at 13:43)
#15746 pseudoabelian categories (1 message, latest: Aug 07 2022 at 06:35)
#15719 additive, multiplicative action (1 message, latest: Aug 06 2022 at 11:52)
#15872 : lp pi_Lp equiv (5 messages, latest: Aug 06 2022 at 00:47)
#15594 Group seminorms (1 message, latest: Aug 04 2022 at 08:18)
#15704 Metrics on multiplicative (9 messages, latest: Aug 03 2022 at 20:45)
#15036 Lagrange interpolant refactor and extension (3 messages, latest: Aug 03 2022 at 16:47)
#14879 Gauge for is_R_or_C (4 messages, latest: Aug 03 2022 at 12:42)
#15667 holomorphic functions on compact manifolds (5 messages, latest: Aug 03 2022 at 06:57)
leanprover-community/leanprover-community.github.io#276 (1 message, latest: Aug 02 2022 at 10:22)
#15310 (1 message, latest: Aug 02 2022 at 00:09)
#15766 dual of convex cone is closed (1 message, latest: Aug 01 2022 at 18:55)
#14854 inter nonempty lemmas (17 messages, latest: Aug 01 2022 at 17:38)
#15240 quiver.path.to_list (4 messages, latest: Aug 01 2022 at 15:15)
✔ #15460 A variant of finsupp.total for ideals. (1 message, latest: Aug 01 2022 at 12:51)
✔ #15355 relation embeddings for sum.lex and prod.lex (1 message, latest: Aug 01 2022 at 12:50)
#15638 I / I ^ 2. (3 messages, latest: Aug 01 2022 at 12:48)
#8002: Bertrand's Postulate (49 messages, latest: Jul 31 2022 at 12:13)
#15460 A variant of finsupp.total for ideals. (1 message, latest: Jul 31 2022 at 01:59)
✔ #14707 ordinal.min → infi (1 message, latest: Jul 30 2022 at 19:43)
#15355 relation embeddings for sum.lex and prod.lex (2 messages, latest: Jul 30 2022 at 19:43)
mathlib_stats #5 (11 messages, latest: Jul 30 2022 at 16:01)
#15765 refactor of lifting properties (1 message, latest: Jul 30 2022 at 03:07)
#15413 sup/inf of add monoid algebras (1 message, latest: Jul 29 2022 at 20:47)
#15691 compute_degree v2 (35 messages, latest: Jul 28 2022 at 08:00)
#15436 Quasi-compact morphisms (2 messages, latest: Jul 27 2022 at 18:06)
#15049 pointwise products of sets (2 messages, latest: Jul 27 2022 at 14:50)
✔ #15399 typeclasses for well-founded < and > (1 message, latest: Jul 27 2022 at 13:45)
✔ #14348 Ore localization of a ring (1 message, latest: Jul 27 2022 at 13:32)
#14348 Ore localization of a ring (3 messages, latest: Jul 27 2022 at 08:29)
#14767 refactor full subcategories (6 messages, latest: Jul 27 2022 at 07:41)
#15961 compute_degree v2 (1 message, latest: Jul 27 2022 at 05:53)
#15961 (4 messages, latest: Jul 26 2022 at 19:23)
✔ #15100 Algebras preadditive (1 message, latest: Jul 26 2022 at 10:12)
✔ #15625 rename nondiscrete_normed_field (1 message, latest: Jul 26 2022 at 10:12)
✔ #14944 Basic framework for classes of morphisms (1 message, latest: Jul 26 2022 at 10:12)
#15100 Algebras preadditive (2 messages, latest: Jul 25 2022 at 05:17)
#14944 Basic framework for classes of morphisms (4 messages, latest: Jul 24 2022 at 09:16)
#15625 rename nondiscrete_normed_field (4 messages, latest: Jul 24 2022 at 00:31)
#15286 induction on an unordered pair (15 messages, latest: Jul 22 2022 at 22:58)
#15088 rewrite cubics (38 messages, latest: Jul 22 2022 at 12:07)
#15616 Dold-Kan correspondence (3 messages, latest: Jul 22 2022 at 07:43)
#12010 Coarse notions on metric spaces (8 messages, latest: Jul 20 2022 at 12:05)
#14896 monotonicity lemmas (1 message, latest: Jul 18 2022 at 14:07)
#14981 add lemmas for GCD domains (1 message, latest: Jul 18 2022 at 10:49)
#14179 Cartan subalgebras as limiting values of UCS (1 message, latest: Jul 18 2022 at 10:29)
Stirling #14874 and #14875 (2 messages, latest: Jul 17 2022 at 20:33)
✔ #15328 move definitions of initial and principal segments (1 message, latest: Jul 17 2022 at 18:45)
#11649 Intersection of affine opens (3 messages, latest: Jul 17 2022 at 17:02)
#15328 move definitions of initial and principal segments (5 messages, latest: Jul 17 2022 at 14:59)
#12301 Change definition of factorization to be computable (26 messages, latest: Jul 17 2022 at 13:20)
#14794 inner prod of matrix (10 messages, latest: Jul 17 2022 at 10:33)
#8632 p^2 is commutative (3 messages, latest: Jul 16 2022 at 12:33)
#14707 ordinal.min → infi (10 messages, latest: Jul 16 2022 at 04:54)
#15399 typeclasses for well-founded < and > (1 message, latest: Jul 15 2022 at 23:43)
#15052 and #15050; pointwise monoid structures (3 messages, latest: Jul 15 2022 at 20:09)
#14581 (3 messages, latest: Jul 15 2022 at 08:45)
ZFC #15208 and #15210 (1 message, latest: Jul 13 2022 at 21:08)
game_add_swap (6 messages, latest: Jul 13 2022 at 15:21)
#15309 extra lemmas about cont_diff_within_at (1 message, latest: Jul 13 2022 at 13:26)
#15281 is_self_adjoint refactor (1 message, latest: Jul 13 2022 at 12:37)
#15296 degree of add_monoid_algebras (3 messages, latest: Jul 13 2022 at 09:25)
#14542 Independence in projective space (5 messages, latest: Jul 12 2022 at 19:32)
#15269 opposites of is_pullback and is_pushout (1 message, latest: Jul 12 2022 at 11:16)
✔ #15232 transferring "enough injectiveness" (2 messages, latest: Jul 11 2022 at 22:07)
✔ #14834 Coalgebras over an endofunctor (1 message, latest: Jul 11 2022 at 21:59)
#14308 add some API for k[G^n] (3 messages, latest: Jul 11 2022 at 13:34)
✔ #13397 continuous map from Proj to Spec (1 message, latest: Jul 11 2022 at 12:21)
✔ #15040 golf using matrix.map (1 message, latest: Jul 11 2022 at 11:33)
✔ #14713 non-class irreducible (1 message, latest: Jul 11 2022 at 11:32)
#14834 Coalgebras over an endofunctor (2 messages, latest: Jul 11 2022 at 07:34)
#13397 continuous map from Proj to Spec (1 message, latest: Jul 11 2022 at 00:28)
#15232 transferring "enough injectiveness" (1 message, latest: Jul 10 2022 at 23:54)
✔ #14347 Cantor Normal Form: cleanup + generalize results (5 messages, latest: Jul 10 2022 at 22:41)
✔ #14955 tweak irreducible attribute in nat_ordinal (11 messages, latest: Jul 10 2022 at 22:37)
#14347 Cantor Normal Form: cleanup + generalize results (3 messages, latest: Jul 10 2022 at 22:10)
#14955 tweak irreducible attribute (1 message, latest: Jul 10 2022 at 22:03)
✔ #14757 review cast API (1 message, latest: Jul 10 2022 at 22:02)
#14497 Harris-Kleitman inequality (2 messages, latest: Jul 10 2022 at 16:10)
#15056 Fixing a diamond (1 message, latest: Jul 10 2022 at 10:28)
#11162 Stars and bars re-revisited (26 messages, latest: Jul 09 2022 at 14:16)
#14876 lemmas about balanced sets (4 messages, latest: Jul 08 2022 at 23:42)
#14928 boring n-ary lemmas (1 message, latest: Jul 08 2022 at 18:06)
#14697 Ruzsa covering (3 messages, latest: Jul 08 2022 at 16:21)
#14549 birthday of addition equals natural addition of birth (4 messages, latest: Jul 07 2022 at 16:37)
#14762 compute_degree_le (1 message, latest: Jul 07 2022 at 10:25)
#14034 induced graphs, cliques, coloring bounds (6 messages, latest: Jul 06 2022 at 18:42)
#15066 pmf is_lawful_monad (5 messages, latest: Jul 06 2022 at 18:39)
#14713 non-class irreducible (3 messages, latest: Jul 05 2022 at 14:05)
#15022 1/x continuous. (1 message, latest: Jul 05 2022 at 08:37)
#15040 golf using matrix.map (1 message, latest: Jul 04 2022 at 16:56)
#14672 mixed characteristic (1 message, latest: Jul 04 2022 at 13:56)
#15106 gaussian integral (11 messages, latest: Jul 04 2022 at 09:48)
#14106 gaussian integral (2 messages, latest: Jul 03 2022 at 16:52)
#14532 function underscores (6 messages, latest: Jul 03 2022 at 16:40)
✔ #15061 add strong_sub_recursion and pincer_recursion (1 message, latest: Jul 02 2022 at 09:01)
#14659 notation and basic API for {x | y}, {x |}, {| x} (9 messages, latest: Jul 01 2022 at 18:40)
✔ #14777 filter_map_join (1 message, latest: Jul 01 2022 at 14:59)
#15061 add strong_sub_recursion and pincer_recursion (1 message, latest: Jul 01 2022 at 09:06)
✔ #15032 split algebra.group.basic (4 messages, latest: Jul 01 2022 at 08:11)
#14757 review cast API (1 message, latest: Jul 01 2022 at 04:37)
#15055 Hellinger-Toeplitz theorem (6 messages, latest: Jul 01 2022 at 00:45)
#14935 golf rec_on_pos_prime_pos_coprime (1 message, latest: Jun 29 2022 at 12:27)
#11053 Prime factorisations in Dedekind domains (8 messages, latest: Jun 28 2022 at 11:28)
#14821 Convexity lemmas (3 messages, latest: Jun 27 2022 at 16:00)
#14930 Lean 3.44.0 (68 messages, latest: Jun 27 2022 at 13:52)
#14714 add lemma linear_independent.finite_of_is_noetherian (6 messages, latest: Jun 26 2022 at 16:50)
#14347 cleanup + generalize results (3 messages, latest: Jun 25 2022 at 22:31)
#14945 quasi_iso.of_homotopy_equiv (3 messages, latest: Jun 25 2022 at 21:48)
#14677 Stone separation theorem (1 message, latest: Jun 25 2022 at 20:15)
#3292 reals aka complete ordered field (8 messages, latest: Jun 23 2022 at 11:14)
#14195 Codisjointness (3 messages, latest: Jun 23 2022 at 10:40)
3185 leanchecker failure (63 messages, latest: Jun 21 2022 at 23:00)
#14777 filter_map_join (1 message, latest: Jun 20 2022 at 18:00)
#14841 ring completions and algebra structures (1 message, latest: Jun 20 2022 at 09:02)
#14676 Join of sets (1 message, latest: Jun 19 2022 at 12:13)
#14463 (1 message, latest: Jun 19 2022 at 09:40)
#14044 Dold-Kan correspondence (2 messages, latest: Jun 18 2022 at 17:44)
#13669 Supremum of pointwise operations (2 messages, latest: Jun 18 2022 at 00:43)
✔ #14271 Delete winner.lean (1 message, latest: Jun 16 2022 at 06:29)
#14271 Delete winner.lean (8 messages, latest: Jun 14 2022 at 19:11)
#13885 Circle integral transform (11 messages, latest: Jun 14 2022 at 17:11)
#14430 Generalize finset.Ioi to empty types (21 messages, latest: Jun 14 2022 at 10:15)
#14174 zero root space is Cartan subalgebra (7 messages, latest: Jun 14 2022 at 09:41)
#14669 and 14680: has_reflect instances (7 messages, latest: Jun 14 2022 at 07:34)
#14307 Supremum of set.image2 (4 messages, latest: Jun 14 2022 at 00:16)
#14581 Exact functors (5 messages, latest: Jun 13 2022 at 10:34)
Dold-Kan correspondence (17 messages, latest: Jun 13 2022 at 06:37)
#14673 finite instances for set (1 message, latest: Jun 11 2022 at 15:56)
#12933 Cauchy functional equation (14 messages, latest: Jun 11 2022 at 14:57)
#14370 list.of_fn_add (5 messages, latest: Jun 09 2022 at 21:15)
#14307 Supremum (1 message, latest: Jun 08 2022 at 20:07)
#14017 Lemmas about the factorisation of 2n choose n (1 message, latest: Jun 06 2022 at 21:43)
8112 Krein-Milman (2 messages, latest: Jun 06 2022 at 11:29)
✔ #14467 change omega to aleph_0 + golf (1 message, latest: Jun 05 2022 at 19:35)
#14373 finite predicate (28 messages, latest: Jun 05 2022 at 18:45)
#14526 opposite of pullbacks/pushouts (co)cones (2 messages, latest: Jun 04 2022 at 13:29)
#14467 change omega to aleph_0 + golf (3 messages, latest: Jun 04 2022 at 05:04)
✔ #14291 define natural addition (1 message, latest: Jun 04 2022 at 00:06)
#14153 congrm = congr + match (1 message, latest: Jun 03 2022 at 11:24)
#14147 Integrability of nonnegative derivatives (1 message, latest: Jun 03 2022 at 09:18)
#14291 define natural addition (1 message, latest: Jun 02 2022 at 18:56)
#14429 recursive ring_nf (1 message, latest: Jun 01 2022 at 19:43)
Vector bundles (2 messages, latest: Jun 01 2022 at 10:29)
#13996 right actions on restrict_scalars (11 messages, latest: May 31 2022 at 08:53)
#14344 make set.finite protected (28 messages, latest: May 30 2022 at 18:37)
✔ #14380 pi_Lp.linear_equiv (2 messages, latest: May 30 2022 at 17:17)
Dependent PRs (1 message, latest: May 30 2022 at 12:35)
#7288 Hahn-Banach (7 messages, latest: May 29 2022 at 00:15)
Localization of categories (9 messages, latest: May 28 2022 at 20:48)
✔ #14140 Generalize theorems on distributivity (1 message, latest: May 28 2022 at 07:45)
✔ #14243 ordinal.succ → order.succ (1 message, latest: May 28 2022 at 01:05)
#14243 ordinal.succ → order.succ (9 messages, latest: May 27 2022 at 22:57)
#14140 Generalize theorems on distributivity (41 messages, latest: May 27 2022 at 21:41)
#13840 Basic lemmas on inv (1 message, latest: May 27 2022 at 02:08)
#14402 The bicategory of algebras and bimodules (1 message, latest: May 26 2022 at 22:08)
#13690 strong law of large numbers (20 messages, latest: May 26 2022 at 19:42)
✔ #13411 Reflexive relation from irreflexive and viceversa (2 messages, latest: May 26 2022 at 18:18)
#13411 Reflexive relation from irreflexive and viceversa (1 message, latest: May 26 2022 at 18:12)
#13245 Equality case of the rearrangement inequality (3 messages, latest: May 25 2022 at 17:27)
#14196 tensor powers (3 messages, latest: May 24 2022 at 11:54)
#12509 A strictly monotone function is unbounded (5 messages, latest: May 22 2022 at 23:48)
#13179 some integral lemmas (3 messages, latest: May 22 2022 at 10:14)
#14136 refactor data/set/finite (7 messages, latest: May 20 2022 at 20:15)
✔ #13611 Tweak pgame.add API (1 message, latest: May 20 2022 at 14:31)
#13611 Tweak pgame.add API (2 messages, latest: May 20 2022 at 05:27)
#14201 minimal period is positive (4 messages, latest: May 19 2022 at 10:05)
#13979 arbitrary proof terms in linear_combination (52 messages, latest: May 18 2022 at 20:10)
#11308 Graded orders (29 messages, latest: May 18 2022 at 19:43)
#11574 group rings (32 messages, latest: May 18 2022 at 13:59)
#12173: Define L-projections, show they form a Boolean alge (3 messages, latest: May 18 2022 at 13:31)
#14096 (1 message, latest: May 18 2022 at 00:56)
#13307 Krull topology is profinite (13 messages, latest: May 16 2022 at 17:02)
#12182 add_monoid_with_one (11 messages, latest: May 16 2022 at 15:06)
#13939 morphism classes for (semi)linear maps (3 messages, latest: May 16 2022 at 09:07)
make discrete a structure #13762 (3 messages, latest: May 14 2022 at 23:07)
[#13963 refactor(set_theory/game/): Fix bad notation < …](topic/.2313963.20refactor(set_theory.2Fgame.2F).3A.20Fix.20bad.20notation.20.60.3C.60.20.2E.2E.2E.html) (29 messages, latest: May 14 2022 at 22:47)
#13963 Fix incorrect definition of < on (pre-)games (11 messages, latest: May 14 2022 at 11:05)
✔ #14031 merge fail (1 message, latest: May 13 2022 at 06:44)
#14031 merge fail (9 messages, latest: May 12 2022 at 21:06)
Linear algebra (1 message, latest: May 12 2022 at 14:15)
✔ #13783 comap_domain.add_monoid_hom (1 message, latest: May 12 2022 at 11:02)
#13783 comap_domain.add_monoid_hom (8 messages, latest: May 12 2022 at 07:51)
#14070 Behrend's construction (2 messages, latest: May 11 2022 at 11:52)
#13462 adic completions of Dedekind Domain FOF (13 messages, latest: May 10 2022 at 17:56)
✔ #13709, submodule.map₂ (1 message, latest: May 10 2022 at 14:50)
#13709, submodule.map₂ (4 messages, latest: May 10 2022 at 08:50)
#13627 (1 message, latest: May 09 2022 at 22:37)
#13788 Missing order dual lemmas (1 message, latest: May 07 2022 at 00:54)
#13208: num.to_bits (12 messages, latest: May 05 2022 at 06:07)
#13719: non-unital normed comm ring (33 messages, latest: May 04 2022 at 22:06)
#9862 the rest of Banach-Alaoglu (12 messages, latest: May 04 2022 at 15:08)
#13946: speed up a proof (1 message, latest: May 04 2022 at 14:53)
✔ #13495 pullbacks/pushouts in opposite category (1 message, latest: May 03 2022 at 20:47)
#13848 Log tonality (2 messages, latest: May 03 2022 at 10:02)
#11458 Separating by convex sets (1 message, latest: Apr 30 2022 at 09:17)
#13576 splitting file (2 messages, latest: Apr 26 2022 at 19:40)
#13569: lemmas about docs#pi_Lp.equiv (1 message, latest: Apr 26 2022 at 16:25)
#13476: non-unital commutative rings (6 messages, latest: Apr 26 2022 at 13:23)
#13414 (6 messages, latest: Apr 26 2022 at 10:55)
#13488 fails_quickly and pi.normed_algebra (3 messages, latest: Apr 22 2022 at 11:42)
#8985 fundamental domain part 2 (18 messages, latest: Apr 22 2022 at 09:02)
#13444 Weaker typeclasses for docs#exp (1 message, latest: Apr 21 2022 at 09:28)
#7498 Oriented incidence matrix (2 messages, latest: Apr 21 2022 at 08:28)
#13483 sort_summands (13 messages, latest: Apr 21 2022 at 06:50)
✔ #12857 Gram-Schmidt Ortho (1 message, latest: Apr 20 2022 at 20:31)
#13495 pullbacks/pushouts in opposite category (1 message, latest: Apr 20 2022 at 10:47)
#12857 Gram-Schmidt Ortho (106 messages, latest: Apr 20 2022 at 08:59)
#13447 (4 messages, latest: Apr 19 2022 at 12:11)
#13498 lemmas about nnnorm and nndist (6 messages, latest: Apr 19 2022 at 11:06)
#13406 (1 message, latest: Apr 19 2022 at 01:30)
#9925 Naming request (factorisation of central binom) (10 messages, latest: Apr 18 2022 at 16:49)
#12078 (16 messages, latest: Apr 17 2022 at 22:07)
✔ #13331 moving lemmas about sum/products indexed by fin (1 message, latest: Apr 17 2022 at 21:34)
#13369 Covariant/contravariant for with_bot/with_top (1 message, latest: Apr 16 2022 at 12:41)
#13480 Uniformly convex spaces (1 message, latest: Apr 16 2022 at 11:22)
#13402 fails_quickly and pi.normed_algebra (2 messages, latest: Apr 15 2022 at 19:23)
#13331 moving lemmas about sum/products indexed by fin (1 message, latest: Apr 15 2022 at 07:49)
#13421 Better simple order lemmas (4 messages, latest: Apr 13 2022 at 21:41)
#13227 apply_rules syntax changes (9 messages, latest: Apr 12 2022 at 19:19)
#13122: monoids in a braided category (44 messages, latest: Apr 12 2022 at 12:10)
#13081 (26 messages, latest: Apr 11 2022 at 21:34)
#12719 – valuation rings (84 messages, latest: Apr 10 2022 at 17:16)
#13072 (3 messages, latest: Apr 10 2022 at 14:45)
#13182: Fundamental group helpers (5 messages, latest: Apr 09 2022 at 13:58)
#13202 - Fixing subgroup (6 messages, latest: Apr 07 2022 at 07:59)
#7803 continuous sections of a vector bundle (8 messages, latest: Apr 06 2022 at 16:38)
#13076 direct sum reindexing (4 messages, latest: Apr 06 2022 at 14:12)
#12799 divisors of prime powers (5 messages, latest: Apr 05 2022 at 16:57)
#12930 is_add_regular (12 messages, latest: Apr 05 2022 at 11:19)
#11207 basics of group representation theory (34 messages, latest: Apr 04 2022 at 11:44)
#12710 discriminant of cyclotomic extensions (2 messages, latest: Apr 03 2022 at 13:27)
#12697 coherence tactic for monoidal categories (5 messages, latest: Apr 02 2022 at 12:09)
#12479 simp_nf linter error in data/sym/basic (37 messages, latest: Mar 31 2022 at 12:21)
#12864 - topological_ring (10 messages, latest: Mar 30 2022 at 07:51)
#12942 Bochner integral refactor (30 messages, latest: Mar 30 2022 at 00:45)
#12844 Borelize tactic (9 messages, latest: Mar 29 2022 at 02:50)
#11794 Strictly convex spaces (12 messages, latest: Mar 26 2022 at 18:00)
#12045 The category of boronologies (1 message, latest: Mar 25 2022 at 08:58)
#12808 Totally bounded sets (2 messages, latest: Mar 24 2022 at 21:10)
#12431 Edge density (19 messages, latest: Mar 24 2022 at 11:28)
✔ #12898 2-out-of-3 property for quasi-iso (1 message, latest: Mar 23 2022 at 11:42)
#12898 2-out-of-3 property for quasi-iso (4 messages, latest: Mar 23 2022 at 10:06)
#12882 even/square (3 messages, latest: Mar 23 2022 at 02:09)
#12754 refactor interval integrals (12 messages, latest: Mar 22 2022 at 02:18)
#12855 Fix definition of frame_hom (12 messages, latest: Mar 21 2022 at 19:01)
#12588 Move complete_lattice.independent (2 messages, latest: Mar 21 2022 at 10:17)
#8545 (21 messages, latest: Mar 21 2022 at 10:16)
#12449 Boundedness in TVS (11 messages, latest: Mar 20 2022 at 16:03)
#12826 (3 messages, latest: Mar 19 2022 at 11:56)
✔ #12778 (1 message, latest: Mar 18 2022 at 12:10)
#12778 (3 messages, latest: Mar 18 2022 at 00:56)
lean#703 noncomputable! (63 messages, latest: Mar 18 2022 at 00:08)
✔ #12467 (3 messages, latest: Mar 17 2022 at 19:30)
#12132 add normed_division_ring (18 messages, latest: Mar 17 2022 at 13:10)
#12759 refactor specific_limits (1 message, latest: Mar 17 2022 at 04:48)
#12512 (11 messages, latest: Mar 17 2022 at 01:00)
#12744 CI problems (3 messages, latest: Mar 16 2022 at 17:49)
#12155 coherence for bicategories (4 messages, latest: Mar 16 2022 at 15:53)
Bounded maps #12046 (13 messages, latest: Mar 16 2022 at 09:29)
#12709 - redefine nat.prime as prime (11 messages, latest: Mar 15 2022 at 18:34)
#12658 equiv_top vs top_equiv (5 messages, latest: Mar 15 2022 at 11:19)
#12403 zeroth derived functor (2 messages, latest: Mar 14 2022 at 20:58)
#12329 (21 messages, latest: Mar 14 2022 at 17:31)
#12645 (6 messages, latest: Mar 14 2022 at 12:14)
#12577 (2 messages, latest: Mar 11 2022 at 22:31)
#12601 unitization (1 message, latest: Mar 11 2022 at 21:37)
#12393 - timeout in simp_nf (4 messages, latest: Mar 11 2022 at 02:05)
#12564 to_additive and units (6 messages, latest: Mar 10 2022 at 16:10)
#7274 - freek #81 divergence of prime reciprocals (2 messages, latest: Mar 09 2022 at 01:52)
has_internal_hom class carrying data #12472 (6 messages, latest: Mar 08 2022 at 07:35)
#12349 fun_like instances on subtypes (3 messages, latest: Mar 06 2022 at 19:13)
#12459 - Relate setoid.is_partition and finpartition (14 messages, latest: Mar 06 2022 at 18:42)
#11233 Signature of a permutation (29 messages, latest: Mar 06 2022 at 12:14)
#12456 - exact g.op f.op (2 messages, latest: Mar 06 2022 at 01:32)
lean#692 (3 messages, latest: Mar 03 2022 at 23:59)
✔ #12435 split bilinear_form (1 message, latest: Mar 03 2022 at 22:19)
#12435 split bilinear_form (1 message, latest: Mar 03 2022 at 21:39)
✔ #12392 null_homotopic_map_comp (1 message, latest: Mar 03 2022 at 18:33)
#12284 weak duals (2 messages, latest: Mar 03 2022 at 11:15)
#12392 null_homotopic_map_comp (1 message, latest: Mar 03 2022 at 11:10)
lean#691 (11 messages, latest: Mar 03 2022 at 09:17)
#12410 split normed_space (11 messages, latest: Mar 02 2022 at 21:09)
#12036 (3 messages, latest: Mar 01 2022 at 18:24)
#11248 LYM, Sperner's theorem (39 messages, latest: Mar 01 2022 at 17:17)
#11595 (16 messages, latest: Mar 01 2022 at 08:51)
#12333 pseudoabelian categories (4 messages, latest: Feb 28 2022 at 22:41)
#11966 Compact opens (10 messages, latest: Feb 28 2022 at 10:37)
#11839 (3 messages, latest: Feb 25 2022 at 17:24)
#12270 pseudoabelian categories (3 messages, latest: Feb 25 2022 at 13:26)
#12054 Move gauge (30 messages, latest: Feb 24 2022 at 09:19)
#12189 Upper/lower sets (14 messages, latest: Feb 23 2022 at 16:35)
#12132 (18 messages, latest: Feb 23 2022 at 10:23)
#12230 decidability in associates (1 message, latest: Feb 23 2022 at 09:38)
#11804 Discriminant of the cyclotomic field (2 messages, latest: Feb 22 2022 at 19:25)
#9345 some lemmas relating shapes of factorisations (3 messages, latest: Feb 22 2022 at 00:35)
#12117 polynomial.eval arguments order (5 messages, latest: Feb 21 2022 at 18:14)
#12023 Equipartitions (1 message, latest: Feb 21 2022 at 14:04)
#12134 (6 messages, latest: Feb 20 2022 at 23:47)
✔ #12056 is_iso.of_iso_comp_left/right (1 message, latest: Feb 20 2022 at 12:10)
✔ #12144 Housework on data/nat/factorization (2 messages, latest: Feb 20 2022 at 10:52)
#12091 First-Order Formula Tweaks (5 messages, latest: Feb 19 2022 at 19:24)
#12035 Turn topological types of sets into structures (1 message, latest: Feb 19 2022 at 16:28)
#12144 Housework on data/nat/factorization (3 messages, latest: Feb 19 2022 at 14:38)
✔ #11332 Euler's product formula for totient function (1 message, latest: Feb 18 2022 at 07:18)
#12057 renaming erase_dup to dedup (2 messages, latest: Feb 18 2022 at 01:01)
#11332 Euler's product formula for totient function (34 messages, latest: Feb 17 2022 at 17:22)
#11946 centralizers (11 messages, latest: Feb 17 2022 at 14:37)
✔ #11960 has_involutive_neg and friends (1 message, latest: Feb 16 2022 at 14:22)
#11960 has_involutive_neg and friends (56 messages, latest: Feb 16 2022 at 09:29)
#11955, lemmas on permutations (15 messages, latest: Feb 15 2022 at 17:03)
#12056 is_iso.of_iso_comp_left/right (1 message, latest: Feb 15 2022 at 14:29)
#11786 lemmas about cyclotomic fields (2 messages, latest: Feb 14 2022 at 18:56)
#11710 Ico_subset lemma (3 messages, latest: Feb 13 2022 at 17:49)
#9795 Finite partitions (50 messages, latest: Feb 12 2022 at 15:28)
#11931 pseudoabelian categories (6 messages, latest: Feb 11 2022 at 18:27)
#11709 Frames (71 messages, latest: Feb 10 2022 at 12:16)
#11817 pseudoabelian categories (11 messages, latest: Feb 09 2022 at 07:17)
#11787 some modeq lemmas (1 message, latest: Feb 08 2022 at 15:50)
#11878 injective objects and resolutions (16 messages, latest: Feb 07 2022 at 18:33)
#11256 refactor(algebra/homology/homotopy) (22 messages, latest: Feb 07 2022 at 14:56)
#11728 Turning a preorder into a partial order (7 messages, latest: Feb 07 2022 at 13:37)
#11868 has_zero for part (5 messages, latest: Feb 06 2022 at 23:37)
#11648 Two pointings (4 messages, latest: Feb 04 2022 at 22:59)
#11770 re-im set product (5 messages, latest: Feb 04 2022 at 16:54)
#11427 make coe_norm_subgroup, submodule.norm_coe consistent (21 messages, latest: Feb 01 2022 at 17:03)
#11720 Typeclass failure (4 messages, latest: Feb 01 2022 at 11:21)
✔ #11570 (2 messages, latest: Jan 31 2022 at 16:06)
#11746 tidy hunting (1 message, latest: Jan 31 2022 at 12:35)
#11459 Fundamental groupoid preserves products (11 messages, latest: Jan 31 2022 at 11:07)
#11742 library_search and negation (2 messages, latest: Jan 31 2022 at 06:19)
#11659 squeeze simp fixes (2 messages, latest: Jan 31 2022 at 00:47)
#11730 enhancing 'equiv_rw' (2 messages, latest: Jan 31 2022 at 00:40)
#11570 (6 messages, latest: Jan 29 2022 at 10:01)
#11696 squeeze_simp providing invalid suggestions (4 messages, latest: Jan 28 2022 at 14:20)
lint: check for unfreeze_local_instances #11509 (1 message, latest: Jan 28 2022 at 13:02)
#11604 Topology induced by seminorms (37 messages, latest: Jan 28 2022 at 09:55)
#11665 diamond (4 messages, latest: Jan 26 2022 at 23:50)
#11313 prime powers (22 messages, latest: Jan 26 2022 at 18:44)
#11602 Semimodular lattices (16 messages, latest: Jan 26 2022 at 16:29)
#11567 partial order on set_semiring (3 messages, latest: Jan 25 2022 at 21:04)
✔ #11632 Notation for monoid_with_zero_hom (1 message, latest: Jan 25 2022 at 13:20)
#11470 Uniform convergence of multiplication and inversion (26 messages, latest: Jan 25 2022 at 12:23)
#11643 trivial' (1 message, latest: Jan 24 2022 at 23:12)
#11624 enhancing filter_upwards tactic (2 messages, latest: Jan 24 2022 at 13:24)
#11632 Notation for monoid_with_zero_hom (6 messages, latest: Jan 24 2022 at 10:08)
#11631 (5 messages, latest: Jan 24 2022 at 04:29)
#11421 Refactor order ideals (1 message, latest: Jan 23 2022 at 10:32)
#11408 Minimal/maximal elements (5 messages, latest: Jan 23 2022 at 10:24)
✔ #11459 Fundamental groupoid preserves products (11 messages, latest: Jan 22 2022 at 22:38)
#11400 Strong antichains (1 message, latest: Jan 22 2022 at 09:58)
#11451 Missing lemmas about cyclotomic extensions (1 message, latest: Jan 20 2022 at 22:07)
#10861 Rearrangement inequality (3 messages, latest: Jan 18 2022 at 16:50)
#11246 Real log with base (19 messages, latest: Jan 18 2022 at 06:45)
#11046 Complexity theory (14 messages, latest: Jan 17 2022 at 15:35)
#11255 Classification of Hilbert spaces (4 messages, latest: Jan 16 2022 at 21:28)
#11162 (5 messages, latest: Jan 16 2022 at 16:41)
#8218 merge normed_space and semi_normed_space (2 messages, latest: Jan 16 2022 at 13:18)
#11351 Sum of locally finite orders (1 message, latest: Jan 15 2022 at 10:07)
#11414 seminorm has_scalar instance (15 messages, latest: Jan 14 2022 at 15:42)
#9080 (3 messages, latest: Jan 14 2022 at 05:12)
#10992 Sesquilinear forms (11 messages, latest: Jan 13 2022 at 12:51)
#11246 logarithm in a base (9 messages, latest: Jan 12 2022 at 22:45)
#11090 integrability on infinite intervals (1 message, latest: Jan 12 2022 at 16:12)
#11366 (2 messages, latest: Jan 11 2022 at 18:44)
#11333 lemmas relating a / b and a when 1 ≤ b and 1 < b (2 messages, latest: Jan 11 2022 at 17:22)
#11302 (9 messages, latest: Jan 10 2022 at 21:36)
#11175 dfinsupp is locally finite (1 message, latest: Jan 10 2022 at 17:06)
#11083 even card vertices of perfect matching (20 messages, latest: Jan 09 2022 at 22:40)
#10929 Sigma types are locally finite (1 message, latest: Jan 09 2022 at 22:22)
#10540 Defining prime_factorization (7 messages, latest: Jan 07 2022 at 22:38)
#10780 Strange CI errors (46 messages, latest: Jan 07 2022 at 17:48)
#11142 Symmetric powers of a finset (2 messages, latest: Jan 07 2022 at 10:45)
#9864 Gluing topology spaces. (15 messages, latest: Jan 06 2022 at 14:28)
#11204 neg one pow (80 messages, latest: Jan 06 2022 at 13:16)
#10497 Freiman homomorphisms (1 message, latest: Jan 06 2022 at 13:01)
Signature of a permutation (2 messages, latest: Jan 06 2022 at 12:07)
#10889 Add more finset induction lemmas (1 message, latest: Jan 06 2022 at 10:17)
#11253 lean bump (4 messages, latest: Jan 06 2022 at 04:22)
Non maths CI failures (7 messages, latest: Jan 06 2022 at 03:53)
notation for units #11236 (5 messages, latest: Jan 05 2022 at 16:56)
#11139 taylor sum and nat_degree_taylor (10 messages, latest: Jan 05 2022 at 16:41)
#11240 writing tests that are expected to fail (4 messages, latest: Jan 04 2022 at 23:21)
#11161 protect polynomial.map_blah (19 messages, latest: Jan 04 2022 at 09:39)
#11052 surreal numbers (1 message, latest: Jan 03 2022 at 22:57)
#11147 function field (10 messages, latest: Jan 02 2022 at 11:14)
#5698 strongly regular graphs (81 messages, latest: Jan 01 2022 at 15:51)
#10867 Incidence matrix (14 messages, latest: Jan 01 2022 at 11:47)
#10743: bors failing (10 messages, latest: Dec 31 2021 at 20:06)
#11128 /data/nat/cast generalization (4 messages, latest: Dec 30 2021 at 13:57)
#10926 lex synonym (21 messages, latest: Dec 30 2021 at 08:42)
#11033 ne_zero (3 messages, latest: Dec 29 2021 at 05:16)
#10958 Lift a finset to a sigma type (2 messages, latest: Dec 28 2021 at 18:54)
#11095 walks, trails, paths pt 3 (1 message, latest: Dec 28 2021 at 06:21)
#9430 pairing measures with nnreal valued test functions (1 message, latest: Dec 27 2021 at 13:21)
#11015 (9 messages, latest: Dec 27 2021 at 05:42)
#10685 Slice of a set family (2 messages, latest: Dec 26 2021 at 11:55)
#10981 walks, trails, paths (11 messages, latest: Dec 24 2021 at 17:39)
#11010 walks, trails, paths pt 2 (1 message, latest: Dec 24 2021 at 17:07)
#10831 order_iso_rpow (3 messages, latest: Dec 24 2021 at 07:37)
#7138 neighbor set of compl (12 messages, latest: Dec 23 2021 at 18:41)
#10849 Cyclotomic extensions (1 message, latest: Dec 22 2021 at 09:56)
✔ #10443 refactoring sesquilinear forms (1 message, latest: Dec 21 2021 at 12:38)
https://github.com/leanprover/vscode-lean/pull/285 (12 messages, latest: Dec 20 2021 at 11:25)
#10864 is_matching iff all degrees = 1 (3 messages, latest: Dec 20 2021 at 09:52)
#10888 filter_Ico_card_eq_of_periodic (8 messages, latest: Dec 20 2021 at 09:12)
#10888 (5 messages, latest: Dec 19 2021 at 01:27)
#10880 list.count_singleton' (46 messages, latest: Dec 18 2021 at 20:57)
#10708 finsupp.mul_prod_erase (12 messages, latest: Dec 18 2021 at 16:08)
#10676 Covering relation (3 messages, latest: Dec 17 2021 at 16:32)
#10443 refactoring sesquilinear forms (1 message, latest: Dec 16 2021 at 13:26)
#10663 banach-steinhaus (2 messages, latest: Dec 15 2021 at 21:02)
#10243 Generalize universes for limits (15 messages, latest: Dec 14 2021 at 19:57)
#10616 divergence thm (special cases) (1 message, latest: Dec 14 2021 at 14:12)
#10700 limits of linear maps (1 message, latest: Dec 13 2021 at 20:59)
leanprover-community/doc-gen#145 Graph links (3 messages, latest: Dec 13 2021 at 12:07)
#10436 gluing data (2 messages, latest: Dec 13 2021 at 07:34)
#9762 simplicial complex (48 messages, latest: Dec 12 2021 at 00:18)
#10667 Change definition of < on α × β (5 messages, latest: Dec 11 2021 at 14:52)
#10668 (24 messages, latest: Dec 11 2021 at 11:12)
#9888 introduce classes for types of homomorphism (8 messages, latest: Dec 09 2021 at 12:03)
#10312 missing type class instance (2 messages, latest: Dec 09 2021 at 10:36)
#10509 Salem-Spencer sets and Roth numbers (1 message, latest: Dec 08 2021 at 14:18)
#10350 DIscriminant (26 messages, latest: Dec 08 2021 at 09:21)
#9836 Polar sets (2 messages, latest: Dec 07 2021 at 22:20)
#10593 (4 messages, latest: Dec 07 2021 at 15:31)
#10476 field-spectrum (2 messages, latest: Dec 06 2021 at 03:08)
#10588 coprime_add_mul_self (7 messages, latest: Dec 04 2021 at 12:52)
#10287 graph coloring and partitions (12 messages, latest: Dec 04 2021 at 03:18)
#10438 Lemmas about preserving pullbacks (2 messages, latest: Dec 02 2021 at 16:04)
#10422 roots of cyclotomic polynomials (1 message, latest: Dec 02 2021 at 14:57)
#10238 UV-compression (2 messages, latest: Nov 30 2021 at 18:18)
#10535 timeouts in wide_pullbacks (9 messages, latest: Nov 29 2021 at 06:19)
#10312 timeouts in cech_nerve (27 messages, latest: Nov 29 2021 at 06:03)
#9985 matrix inverses, bizarre failure (6 messages, latest: Nov 27 2021 at 11:37)
#10506 (2 messages, latest: Nov 26 2021 at 21:40)
#10011 fails quickly (5 messages, latest: Nov 24 2021 at 16:27)
#10210 refactoring graph matchings (13 messages, latest: Nov 24 2021 at 08:27)
#9891 unbundle order_{top,bot} from order hierarchy (18 messages, latest: Nov 23 2021 at 14:27)
#10349 Reduce imports to only those necessary in the entire (226 messages, latest: Nov 22 2021 at 01:26)
#10390 Define the spectrum of elements of algebras (8 messages, latest: Nov 21 2021 at 22:49)
✔ #10384 Naming erase_erase lemmas (7 messages, latest: Nov 19 2021 at 21:20)
#10366 changing < to > (23 messages, latest: Nov 17 2021 at 23:39)
#10353 bilinear form lemmas (1 message, latest: Nov 17 2021 at 15:07)
#10356 (1 message, latest: Nov 16 2021 at 17:00)
#10188 (5 messages, latest: Nov 16 2021 at 15:06)
#10235 split opposites (57 messages, latest: Nov 16 2021 at 13:37)
#10306 orientations of modules (25 messages, latest: Nov 16 2021 at 01:24)
#10115 graded rings (5 messages, latest: Nov 15 2021 at 18:35)
#9995 (4 messages, latest: Nov 11 2021 at 14:09)
#10141 (1 message, latest: Nov 10 2021 at 18:07)
#10163 indentation linter (7 messages, latest: Nov 10 2021 at 08:05)
#10237 (1 message, latest: Nov 09 2021 at 00:17)
#10097 order_{top,bot} as mixin (9 messages, latest: Nov 08 2021 at 13:18)
#8611 (50 messages, latest: Nov 06 2021 at 02:53)
#9985 (co)limits in Top (3 messages, latest: Nov 05 2021 at 03:28)
#9898 Indexing in set.pairwise_disjoint (4 messages, latest: Nov 04 2021 at 14:23)
#9791 Picard-Lindelof/Cauchy-Lipschitz Theorem (7 messages, latest: Nov 04 2021 at 07:47)
#10110 move derivatives of arcsin and arccos to new file (16 messages, latest: Nov 03 2021 at 10:57)
#10069 Open immersions of presheafed spaces (37 messages, latest: Nov 02 2021 at 06:33)
#10004 direct_sum.submodule_coe (2 messages, latest: Nov 01 2021 at 06:27)
#10035 rename set.pairwise_on to set.pairwise (11 messages, latest: Oct 31 2021 at 16:53)
#10018 (16 messages, latest: Oct 29 2021 at 20:53)
#10022 (7 messages, latest: Oct 29 2021 at 01:03)
#8820 Lucas Primality (35 messages, latest: Oct 28 2021 at 23:05)
#9970 new diamond (13 messages, latest: Oct 27 2021 at 15:00)
#9932 Split exponential (3 messages, latest: Oct 24 2021 at 14:33)
#9717 homogeneous ideal (13 messages, latest: Oct 24 2021 at 07:26)
#9834 isomorphic if same card (14 messages, latest: Oct 23 2021 at 18:01)
#9753 central binomial coefficients (7 messages, latest: Oct 23 2021 at 08:58)
#9875 notation for star-linear maps (9 messages, latest: Oct 23 2021 at 01:03)
#8598 Weak star topology (20 messages, latest: Oct 21 2021 at 19:08)
#9834 statement? (14 messages, latest: Oct 21 2021 at 12:57)
#9640 and #9692: replace conj with star (6 messages, latest: Oct 21 2021 at 03:56)
#9792 move IVT to a new file (4 messages, latest: Oct 20 2021 at 16:20)
#9824 bump to 3.34.0 (7 messages, latest: Oct 20 2021 at 15:45)
#9810 Bors is stuck? (2 messages, latest: Oct 20 2021 at 09:53)
#9707 real.Inf of a • s (14 messages, latest: Oct 18 2021 at 13:15)
#9746 (4 messages, latest: Oct 16 2021 at 22:19)
#9490 double cosets (12 messages, latest: Oct 15 2021 at 19:35)
#9705 timeout (4 messages, latest: Oct 14 2021 at 14:06)
#9590 Rename floor and ceil (5 messages, latest: Oct 14 2021 at 13:08)
#9078 Bounds of a • s (1 message, latest: Oct 13 2021 at 21:26)
#9675 generalize universes for sheaves (123 messages, latest: Oct 13 2021 at 14:00)
#9651 (+60, -19) star lemmas (5 messages, latest: Oct 12 2021 at 21:14)
#9671 (3 messages, latest: Oct 12 2021 at 08:17)
#9655 (12 messages, latest: Oct 11 2021 at 18:56)
#9470 (+127,-1) computable cyclic perm notation (14 messages, latest: Oct 09 2021 at 23:23)
#9593 Monotonicity and interval statements using to_dual (10 messages, latest: Oct 08 2021 at 16:17)
#7987 Locally finite orders (25 messages, latest: Oct 08 2021 at 06:49)
#9593 Monotonicity statements using to_dual (11 messages, latest: Oct 07 2021 at 23:02)
#9586 Graded monoids (4 messages, latest: Oct 07 2021 at 15:40)
#9558 Monotonicity of scalar multiplication (2 messages, latest: Oct 07 2021 at 08:16)
#9560 splitting equiv/basic (2 messages, latest: Oct 07 2021 at 01:40)
#9544 nat subtraction lemmas (14 messages, latest: Oct 07 2021 at 01:39)
#9510 (post-review) (2 messages, latest: Oct 04 2021 at 19:58)
#8082 succ_order (60 messages, latest: Oct 03 2021 at 00:27)
#8466 matrix.general_linear_group (23 messages, latest: Oct 01 2021 at 09:18)
#9214 results on internal direct sums (39 messages, latest: Sep 30 2021 at 14:38)
#9119 antitone (72 messages, latest: Sep 30 2021 at 12:13)
#8837 base_at construction (4 messages, latest: Sep 30 2021 at 07:09)
#9103 (+80, -4): lemmas about affine combinations (8 messages, latest: Sep 29 2021 at 14:07)
#9340 splitting trigonometry (2 messages, latest: Sep 27 2021 at 04:21)
#8829 (merged) (4 messages, latest: Sep 24 2021 at 14:42)
#9223 (3 messages, latest: Sep 24 2021 at 08:05)
#9283 refactor of regular measures (8 messages, latest: Sep 24 2021 at 07:49)
#9128 (8 messages, latest: Sep 23 2021 at 15:36)
#9255 ext for derivations (1 message, latest: Sep 22 2021 at 18:30)
#8904 finite_measure and probability_ measure (6 messages, latest: Sep 19 2021 at 08:07)
#9072 (2 messages, latest: Sep 14 2021 at 11:58)
#9185 finset.card_erase (8 messages, latest: Sep 13 2021 at 18:18)
#9092 trivial group quotients (4 messages, latest: Sep 13 2021 at 14:07)
#9018 convex independence (8 messages, latest: Sep 13 2021 at 08:52)
#8995 Z_p is adically complete (3 messages, latest: Sep 13 2021 at 08:00)
#7843 dyadic surreals (81 messages, latest: Sep 13 2021 at 02:59)
#8579 one point compactification (24 messages, latest: Sep 11 2021 at 17:44)
#7825 infinite Hall's marriage theorem (2 messages, latest: Sep 10 2021 at 22:04)
✔ #9094 generalize segments (2 messages, latest: Sep 10 2021 at 20:43)
#9094 generalize segments (4 messages, latest: Sep 10 2021 at 16:44)
#8986 Henselian rings (7 messages, latest: Sep 10 2021 at 12:50)
website 196 (22 messages, latest: Sep 08 2021 at 18:13)
✔ #8868 remove @[ext] tag from tensor_product.mk_compr₂_inj (1 message, latest: Sep 07 2021 at 22:00)
#8930 loosen ordered_module to smul_with_zero (58 messages, latest: Sep 07 2021 at 20:49)
✔ #8870 (1 message, latest: Sep 07 2021 at 05:53)
#8889 (5 messages, latest: Sep 07 2021 at 05:30)
#8868 remove @[ext] tag from tensor_product.mk_compr₂_inj (11 messages, latest: Sep 07 2021 at 04:30)
#8956 (4 messages, latest: Sep 06 2021 at 20:15)
#9024 (14 messages, latest: Sep 06 2021 at 13:15)
#8946 rigid monoidal categories (11 messages, latest: Sep 06 2021 at 10:56)
#7526 number of derangements (20 messages, latest: Sep 03 2021 at 06:20)
#8955 matrix.is_sym or matrix.is_symm (4 messages, latest: Sep 02 2021 at 13:29)
[#8902 {topological,smooth}(semi)rings](topic/.238902.20.7Btopological.2Csmooth.7D(semi)rings.html) (13 messages, latest: Sep 01 2021 at 10:14)
#8002 (22 messages, latest: Aug 30 2021 at 07:27)
#8902 redundant smooth_neg (5 messages, latest: Aug 29 2021 at 07:37)
#8902 redundant smooth_add (1 message, latest: Aug 28 2021 at 18:09)
Irrational Between #8753 (3 messages, latest: Aug 27 2021 at 22:50)
#8870 (16 messages, latest: Aug 27 2021 at 17:10)
#8887 LRS isos (7 messages, latest: Aug 27 2021 at 08:34)
#8867 (5 messages, latest: Aug 26 2021 at 04:46)
#8337 Weak convergence (109 messages, latest: Aug 23 2021 at 20:33)
#8819 suggest using X (7 messages, latest: Aug 23 2021 at 08:48)
#8343 generalizing results on dimensions of modules to rings (7 messages, latest: Aug 20 2021 at 06:40)
#8707 linter weirdness (13 messages, latest: Aug 17 2021 at 22:42)
#8660 (16 messages, latest: Aug 17 2021 at 19:00)
#8667 (35 messages, latest: Aug 16 2021 at 21:09)
#8503 truncated subtraction (2 messages, latest: Aug 16 2021 at 06:36)
change filter inf #8657 (12 messages, latest: Aug 13 2021 at 19:52)
[#8656 Oxfrd Invariants problems](topic/.238656.20Oxfrd.20Invariants.20problems.html) (1 message, latest: Aug 13 2021 at 10:26)
#8426 card of sym2 (19 messages, latest: Aug 12 2021 at 08:32)
✔ #8594 measure theory refactor (1 message, latest: Aug 12 2021 at 03:25)
#8594 measure theory refactor (1 message, latest: Aug 10 2021 at 17:51)
#8327 IMO2001 Q6 (22 messages, latest: Aug 09 2021 at 17:16)
#3980 Cayley's theorem (12 messages, latest: Aug 09 2021 at 12:26)
#8327 IMO2006 Q6 (2 messages, latest: Aug 09 2021 at 08:37)
#8544 (1 message, latest: Aug 09 2021 at 07:04)
#8508 (2 messages, latest: Aug 07 2021 at 20:27)
#8563 (11 messages, latest: Aug 07 2021 at 19:28)
#8507 (3 messages, latest: Aug 06 2021 at 07:00)
#8178 undeprecate (22 messages, latest: Jul 31 2021 at 21:14)
#8082 has_lt_iff_add_one_le (38 messages, latest: Jul 28 2021 at 19:01)
#8382 quotient_group and left_cosets (1 message, latest: Jul 28 2021 at 11:24)
#6476 boolean_algebra.to_boolean_ring (39 messages, latest: Jul 22 2021 at 06:24)
#7525 and #8186 (15 messages, latest: Jul 17 2021 at 02:53)
✔ #8071 Ixx_eq_empty lemmas (1 message, latest: Jul 17 2021 at 02:34)
✔ #8279 timeouts in gromov_hausdorff_realized.lean (1 message, latest: Jul 17 2021 at 02:32)
✔ #8228 (1 message, latest: Jul 17 2021 at 02:30)
#8278 (9 messages, latest: Jul 15 2021 at 21:48)
#8228 (2 messages, latest: Jul 15 2021 at 13:16)
#8289 (9 messages, latest: Jul 13 2021 at 18:38)
#8279 timeouts in gromov_hausdorff_realized.lean (7 messages, latest: Jul 13 2021 at 17:04)
#5823 (22 messages, latest: Jul 13 2021 at 09:26)
#8071 Ixx_eq_empty lemmas (2 messages, latest: Jul 13 2021 at 07:47)
#7645 linear_ordered_comm_group_with_zero (2 messages, latest: Jul 07 2021 at 11:02)
#8164 and #8166 (1 message, latest: Jul 06 2021 at 21:37)
#8190 (20 messages, latest: Jul 05 2021 at 15:29)
#8150 determinant timeouts (10 messages, latest: Jul 01 2021 at 09:51)
#8060 ordered groups (2 messages, latest: Jun 30 2021 at 06:33)
#7876 more ordered stuff (18 messages, latest: Jun 29 2021 at 14:34)
#7708 The Lie algebra of a Lie group (89 messages, latest: Jun 28 2021 at 13:34)
#7759 descending factorial (1 message, latest: Jun 25 2021 at 14:50)
#8001 liouville aux (22 messages, latest: Jun 24 2021 at 13:48)
#7982 generalize Koenig lemma (11 messages, latest: Jun 21 2021 at 13:47)
#7986 has_nnnorm (43 messages, latest: Jun 21 2021 at 12:53)
#7875 (3 messages, latest: Jun 21 2021 at 07:17)
#7214 (62 messages, latest: Jun 20 2021 at 23:02)
#7941 homotopy api (3 messages, latest: Jun 19 2021 at 18:56)
#7948 nontrivial instance for nnreal (20 messages, latest: Jun 15 2021 at 11:14)
#7892 reducible ideal quotient (1 message, latest: Jun 13 2021 at 20:15)
#7504 cycles as quotients of lists (6 messages, latest: Jun 12 2021 at 09:43)
bors timeout (3 messages, latest: Jun 12 2021 at 09:26)
#7754 and #7762 first-order (sub)structures (42 messages, latest: Jun 11 2021 at 19:33)
#7864 continuous primitives (31 messages, latest: Jun 10 2021 at 16:08)
#7876 (1 message, latest: Jun 10 2021 at 10:38)
#7859 notation for continuous functions (54 messages, latest: Jun 09 2021 at 17:30)
#6591 non-unital algebras (204 messages, latest: Jun 09 2021 at 08:37)
#6288 Kőnig's lemma for fintypes (2 messages, latest: Jun 06 2021 at 07:25)
#7645 ordered_monoid (42 messages, latest: Jun 02 2021 at 20:15)
#7654, generalize ideals to left ideals in noncomm rings (84 messages, latest: May 31 2021 at 18:39)
homology redesign and derived functors (36 messages, latest: May 31 2021 at 15:11)
#7604 Laurent Series (2 messages, latest: May 29 2021 at 18:58)
#7748 data.nat.sqrt alternative phrasings (1 message, latest: May 29 2021 at 10:35)
leanprover/vscode-lean#268 (6 messages, latest: May 25 2021 at 17:11)
#7535 comma limits (8 messages, latest: May 20 2021 at 15:57)
#7649 tot disc iff tot sep (3 messages, latest: May 19 2021 at 00:10)
#7438 actions on and by units (1 message, latest: May 18 2021 at 16:56)
#7603 normed group quotients (1 message, latest: May 18 2021 at 05:46)
#7553 (23 messages, latest: May 16 2021 at 07:16)
#7502 A_5 is simple (25 messages, latest: May 15 2021 at 17:23)
#7535 (co)limits in comma categories (2 messages, latest: May 15 2021 at 15:03)
#7507 (19 messages, latest: May 14 2021 at 19:10)
#7363 (7 messages, latest: May 14 2021 at 12:51)
antidiagonals having multiplicity #7595 (36 messages, latest: May 13 2021 at 19:46)
#7574 ordered (126 messages, latest: May 13 2021 at 14:13)
#7495 Hahn series form a field (1 message, latest: May 10 2021 at 17:37)
leanprover/vscode-lean#263 (11 messages, latest: May 10 2021 at 12:28)
#7562 Abel-Ruffini (7 messages, latest: May 10 2021 at 07:24)
#7521 (5 messages, latest: May 07 2021 at 22:22)
#7539 modular_lattice (2 messages, latest: May 07 2021 at 13:11)
#7448 Top.limit_cone change + Profinite.as_limit (1 message, latest: May 07 2021 at 02:39)
#7524 (15 messages, latest: May 06 2021 at 23:30)
#7113 (75 messages, latest: May 06 2021 at 23:21)
#7496 bundled basis (1 message, latest: May 06 2021 at 05:52)
#7452 valuation stuff (4 messages, latest: May 04 2021 at 16:31)
#7416 (33 messages, latest: May 03 2021 at 15:20)
#7118 (24 messages, latest: May 03 2021 at 02:15)
#7324 monoidal coherence theorem (5 messages, latest: May 01 2021 at 00:54)
#7398 split group_power.basic (5 messages, latest: Apr 30 2021 at 15:58)
#7375 new complexes (26 messages, latest: Apr 30 2021 at 13:09)
#7265 monoid_algebra.fg (36 messages, latest: Apr 29 2021 at 18:37)
#7311 (d)finsupp (2 messages, latest: Apr 29 2021 at 11:06)
#7335 (3 messages, latest: Apr 27 2021 at 06:37)
#7240 (1 message, latest: Apr 26 2021 at 18:46)
#7230 - super easy (2 messages, latest: Apr 25 2021 at 13:15)
#6949 (4 messages, latest: Apr 24 2021 at 14:59)
#7243 (4 messages, latest: Apr 22 2021 at 23:04)
#7290 adjunction for the over category (1 message, latest: Apr 22 2021 at 03:33)
#7255 (5 messages, latest: Apr 20 2021 at 22:35)
#7155 & #7156 (14 messages, latest: Apr 19 2021 at 07:51)
#7245 (13 messages, latest: Apr 18 2021 at 22:52)
#7203 subobject/limits API (4 messages, latest: Apr 17 2021 at 00:31)
#6497 (1 message, latest: Apr 16 2021 at 01:24)
#7084 (125 messages, latest: Apr 15 2021 at 10:58)
#7150 and #6840 (5 messages, latest: Apr 14 2021 at 23:56)
sublattice definition #7093 (21 messages, latest: Apr 13 2021 at 22:26)
#7082 (16 messages, latest: Apr 10 2021 at 19:56)
#6355 finsum (71 messages, latest: Apr 08 2021 at 15:14)
leanprover-community/leanprover-community.github.io#174 (1 message, latest: Apr 07 2021 at 17:55)
#6973 (38 messages, latest: Apr 06 2021 at 04:29)
#6840 (2 messages, latest: Apr 05 2021 at 12:01)
#6910 generalize isometry to pseudo_metric spaces (1 message, latest: Apr 02 2021 at 07:57)
#6306 (7 messages, latest: Mar 30 2021 at 18:06)
#6960 (2 messages, latest: Mar 30 2021 at 12:26)
#6852 (1 message, latest: Mar 29 2021 at 10:38)
#6863 simplify proof? (6 messages, latest: Mar 28 2021 at 11:38)
#4658 (82 messages, latest: Mar 24 2021 at 12:51)
#6827 (2 messages, latest: Mar 24 2021 at 06:00)
#6789 intermediate value variations (1 message, latest: Mar 23 2021 at 07:12)
#2311 Poincaré recurrence (1 message, latest: Mar 22 2021 at 17:52)
#6657 (2 messages, latest: Mar 22 2021 at 12:30)
#6746 (25 messages, latest: Mar 20 2021 at 13:18)
#6739 (5 messages, latest: Mar 17 2021 at 21:25)
#6587 (10 messages, latest: Mar 16 2021 at 19:27)
#6694 (6 messages, latest: Mar 16 2021 at 19:16)
#6509 timeout (6 messages, latest: Mar 15 2021 at 17:50)
#6673 totally disconnected (9 messages, latest: Mar 14 2021 at 17:18)
#5269 unrelated timeouts (2 messages, latest: Mar 14 2021 at 01:48)
#6588 + #6590 (110 messages, latest: Mar 12 2021 at 19:12)
#6585 (27 messages, latest: Mar 12 2021 at 15:18)
#6621 - Timeouts in continuous_linear_map (3 messages, latest: Mar 11 2021 at 11:38)
#6551 build failing (3 messages, latest: Mar 09 2021 at 22:30)
#6552 make is_closed a class (1 message, latest: Mar 09 2021 at 19:15)
#5421 (36 messages, latest: Mar 09 2021 at 14:59)
#6572 crashes leanchecker (70 messages, latest: Mar 08 2021 at 14:49)
#6292 (13 messages, latest: Mar 07 2021 at 19:27)
#6494 nat/enat valued card (3 messages, latest: Mar 04 2021 at 18:06)
#6426 (3 messages, latest: Mar 04 2021 at 15:38)
leanprover-community/mathlib-tools#95 (13 messages, latest: Mar 04 2021 at 07:57)
#6518 (16 messages, latest: Mar 03 2021 at 16:39)
#6375 (36 messages, latest: Mar 02 2021 at 18:28)
CI not running on #6485 or #6488 (3 messages, latest: Mar 01 2021 at 16:17)
#6442 (11 messages, latest: Feb 26 2021 at 22:37)
#6241 make mul_action.regular an instance (13 messages, latest: Feb 26 2021 at 09:54)
#6355 finsum – refactor of set.finite? (7 messages, latest: Feb 26 2021 at 09:48)
#6411 upgrade to 3.27.0 (36 messages, latest: Feb 25 2021 at 16:55)
#5145 (9 messages, latest: Feb 25 2021 at 08:51)
#6173, non-terminal simps (6 messages, latest: Feb 24 2021 at 09:04)
#6372 (4 messages, latest: Feb 23 2021 at 05:39)
#6268 missing lemmas about equiv (1 message, latest: Feb 22 2021 at 10:12)
#6333 (4 messages, latest: Feb 22 2021 at 07:58)
#6192 locally constant functions (1 message, latest: Feb 20 2021 at 23:45)
#6308 Moore complex (3 messages, latest: Feb 19 2021 at 07:05)
#4458 smooth bump function (11 messages, latest: Feb 19 2021 at 06:37)
#6199 no_zero_smul_divisors (8 messages, latest: Feb 17 2021 at 13:21)
#6125 (10 messages, latest: Feb 17 2021 at 06:12)
#6167 (3 messages, latest: Feb 16 2021 at 23:06)
#6188 pi_0 (15 messages, latest: Feb 16 2021 at 18:32)
#5795 (2 messages, latest: Feb 15 2021 at 10:36)
#6056 odd Bernoulli (37 messages, latest: Feb 14 2021 at 08:37)
#5361 Liouville (162 messages, latest: Feb 12 2021 at 18:33)
#4684 (16 messages, latest: Feb 11 2021 at 06:20)
#6162 uniform_continuous_norm (8 messages, latest: Feb 11 2021 at 05:39)
Multiplication on direct_sum: #5956 and #6053 (3 messages, latest: Feb 10 2021 at 18:53)
#6149 (2 messages, latest: Feb 10 2021 at 06:55)
#5927 (2 messages, latest: Feb 08 2021 at 00:25)
#5354 (2 messages, latest: Feb 03 2021 at 18:01)
#5939 (1 message, latest: Feb 03 2021 at 13:24)
#5933 (3 messages, latest: Feb 02 2021 at 06:25)
#5991 polynomial.eval2_smul (1 message, latest: Feb 01 2021 at 09:18)
polynomial.eval2_smul (12 messages, latest: Feb 01 2021 at 09:03)
#5852 (3 messages, latest: Jan 27 2021 at 16:13)
#5895 bump to 3.25.0 (27 messages, latest: Jan 27 2021 at 08:18)
#5813 finset.bind -> finset.bUnion (2 messages, latest: Jan 26 2021 at 04:20)
#5695 Hall (13 messages, latest: Jan 24 2021 at 05:55)
#5774 minpoly refactor (48 messages, latest: Jan 18 2021 at 10:46)
#5771 minpoly (12 messages, latest: Jan 18 2021 at 05:32)
LGTM (4 messages, latest: Jan 17 2021 at 23:54)
#5683 (1 message, latest: Jan 15 2021 at 20:09)
#5493 (2 messages, latest: Jan 13 2021 at 19:34)
#5404 (1 message, latest: Jan 10 2021 at 17:59)
#4841 rewrite_search (151 messages, latest: Jan 06 2021 at 13:57)
Style guide (15 messages, latest: Jan 04 2021 at 07:42)
#5539 semifields (2 messages, latest: Jan 01 2021 at 04:40)
#5509 less painful semimodule diamonds (37 messages, latest: Dec 31 2020 at 11:59)
#5510 refactor Bochner integral (3 messages, latest: Dec 29 2020 at 16:52)
#5430 auxiliary typeclasses for has_scalar Z lemmas (2 messages, latest: Dec 28 2020 at 20:48)
#4473 base change (1 message, latest: Dec 26 2020 at 19:02)
#5434 satisfies_acc (2 messages, latest: Dec 23 2020 at 08:53)
4770 smul_comm_class (60 messages, latest: Dec 22 2020 at 23:07)
#3746 deriv tan (23 messages, latest: Dec 20 2020 at 17:23)
#5164 Witt vectors over zmod p (3 messages, latest: Dec 19 2020 at 21:35)
#5409 (14 messages, latest: Dec 18 2020 at 15:59)
#5369 (1 message, latest: Dec 15 2020 at 17:23)
#5285 Is_galois iff is_galois top (4 messages, latest: Dec 12 2020 at 22:42)
#5255 Category of Sheaves over a Site (3 messages, latest: Dec 10 2020 at 07:39)
#5187 Alternatization of multilinear maps (1 message, latest: Dec 09 2020 at 09:34)
#4996 bundled sets closed under a mul action (7 messages, latest: Dec 08 2020 at 15:47)
#5195 – Restrict ultrafilter along large embedding (8 messages, latest: Dec 06 2020 at 04:19)
#5195 (1 message, latest: Dec 04 2020 at 16:14)
#4301 Liouville (23 messages, latest: Dec 03 2020 at 17:48)
#4037 (9 messages, latest: Nov 28 2020 at 01:32)
bundled sets closed under a mul action #4996 (3 messages, latest: Nov 27 2020 at 12:12)
#5093 dead bors (4 messages, latest: Nov 25 2020 at 15:44)
#4773 heterobasic tensor product (1 message, latest: Nov 17 2020 at 18:21)
#4954 - adding opposite to a few more type classes (2 messages, latest: Nov 17 2020 at 11:27)
#4949 (51 messages, latest: Nov 11 2020 at 15:25)
#4916 - removing irreducible on free_algebra (1 message, latest: Nov 09 2020 at 16:35)
#4946 mul_action renames (12 messages, latest: Nov 09 2020 at 10:54)
#4886 (5 messages, latest: Nov 05 2020 at 16:06)
#4810 (1 message, latest: Oct 31 2020 at 06:32)
#4301 liouville (2 messages, latest: Oct 30 2020 at 13:31)
#4832 speedy sheaf (4 messages, latest: Oct 30 2020 at 13:04)
#3490 (49 messages, latest: Oct 29 2020 at 13:25)
#4646 equivalent statements of is_o/is_O (2 messages, latest: Oct 29 2020 at 04:46)
#4786 galois (1 message, latest: Oct 26 2020 at 07:44)
#4406 (1 message, latest: Oct 26 2020 at 00:31)
#4774 Unique Factorization of Polynomials (14 messages, latest: Oct 25 2020 at 16:59)
#4733 restriction of scalars (1 message, latest: Oct 22 2020 at 08:06)
#4648 pretopologies (1 message, latest: Oct 21 2020 at 13:45)
#4672 (10 messages, latest: Oct 18 2020 at 19:43)
#4518 trig IMO problem (5 messages, latest: Oct 16 2020 at 03:58)
#4363 feat(algebra/ordered_semiring): relax 0 < 1 to 0 ≤ 1 (6 messages, latest: Oct 16 2020 at 02:31)
vscode-lean#227 \goal for ⊢ (4 messages, latest: Oct 15 2020 at 10:29)
#4402 monoid_algebra and to_additive (9 messages, latest: Oct 15 2020 at 06:15)
4447 migrate to dense API (9 messages, latest: Oct 15 2020 at 02:42)
#4432 bounds on exp (1 message, latest: Oct 12 2020 at 11:39)
lean#476 conv mode find and for (2 messages, latest: Oct 12 2020 at 09:53)
4574 better nontriviality (16 messages, latest: Oct 11 2020 at 22:34)
4567 linear independent (4 messages, latest: Oct 11 2020 at 07:30)
#4351 (6 messages, latest: Oct 10 2020 at 14:56)
#4527 polynomial.erase_lead (1 message, latest: Oct 10 2020 at 08:40)
#4464 witt_structure_rat (5 messages, latest: Oct 06 2020 at 09:37)
#4268 structure theorem for Witt polynomials (7 messages, latest: Oct 06 2020 at 06:40)
how you do reviews? (4 messages, latest: Oct 05 2020 at 23:23)
88 bottles of maths on the wall (26 messages, latest: Oct 05 2020 at 10:56)
#4393 Gauss's Lemma (1 message, latest: Oct 04 2020 at 01:19)
#4298 move ring_theory/algebra (4 messages, latest: Oct 02 2020 at 08:35)
#4096 pigeonhole principles (55 messages, latest: Oct 01 2020 at 02:56)
roots of unity (1 message, latest: Sep 30 2020 at 07:02)
#4229 (3 messages, latest: Sep 28 2020 at 08:10)
#4267 Cheby (16 messages, latest: Sep 26 2020 at 14:49)
#4273 intervals and with_top/bot (6 messages, latest: Sep 26 2020 at 08:15)
#3641 (15 messages, latest: Sep 25 2020 at 09:43)
#4243 nat.pow, part II (2 messages, latest: Sep 24 2020 at 19:39)
#4239 (5 messages, latest: Sep 24 2020 at 16:01)
#4236 Witt polynomials (3 messages, latest: Sep 24 2020 at 15:46)
#4198 gluing presheaves (15 messages, latest: Sep 24 2020 at 10:35)
#4069 trailing coeff (131 messages, latest: Sep 22 2020 at 12:01)
#3904 bundled smooth maps (13 messages, latest: Sep 15 2020 at 06:52)
#3760 Lebesgue shift/rescale (6 messages, latest: Sep 14 2020 at 19:36)
#4111 (25 messages, latest: Sep 14 2020 at 19:30)
#4135 nat refactor/cleanup (1 message, latest: Sep 14 2020 at 07:22)
#4093: Try this: skeleton for a proof by cases (4 messages, latest: Sep 12 2020 at 18:16)
#3967 slim_check sampleable (7 messages, latest: Sep 11 2020 at 13:55)
#4063 path connected (1 message, latest: Sep 11 2020 at 10:27)
#4057 (Inner product) (5 messages, latest: Sep 11 2020 at 03:40)
#4076 (4 messages, latest: Sep 10 2020 at 09:01)
#3995 (14 messages, latest: Sep 09 2020 at 23:42)
#4070 mv polynomials (1 message, latest: Sep 08 2020 at 14:46)
#3991 (9 messages, latest: Sep 06 2020 at 13:46)
#3976 (4 messages, latest: Sep 06 2020 at 04:30)
#3638 (12 messages, latest: Sep 05 2020 at 06:09)
#4025 (6 messages, latest: Sep 02 2020 at 19:41)
#3913 (5 messages, latest: Sep 01 2020 at 19:47)
#3984 (35 messages, latest: Aug 30 2020 at 20:42)
#3904 (1 message, latest: Aug 29 2020 at 08:58)
#3907 structure sheaf on Spec R (1 message, latest: Aug 28 2020 at 06:06)
lean#452 making fin a subtype (2 messages, latest: Aug 24 2020 at 12:35)
3870 equiv/transfer_instances (5 messages, latest: Aug 22 2020 at 10:08)
#3830 expr binder functions (1 message, latest: Aug 21 2020 at 08:39)
3728: define ordered semimodules and generalize convexity… (14 messages, latest: Aug 20 2020 at 13:36)
3709 FTC again (5 messages, latest: Aug 18 2020 at 21:24)
3844 tower law for modules (6 messages, latest: Aug 18 2020 at 08:52)
#3716 API for with_zero (2 messages, latest: Aug 17 2020 at 03:19)
#3735 (3 messages, latest: Aug 15 2020 at 21:48)
#3742 (1 message, latest: Aug 15 2020 at 06:42)
#3762 (18 messages, latest: Aug 14 2020 at 04:33)
#3733 algebraic closure (24 messages, latest: Aug 11 2020 at 08:34)
#3458 and #3672 (8 messages, latest: Aug 10 2020 at 19:42)
#3717 (3 messages, latest: Aug 09 2020 at 13:03)
#3638 indexed qpf families (2 messages, latest: Aug 05 2020 at 13:55)
#3658 extend Hahn-Banach from ℝ to ℂ (27 messages, latest: Aug 04 2020 at 21:57)
#3627 (13 messages, latest: Aug 04 2020 at 08:34)
splitting 3590 ? (9 messages, latest: Aug 03 2020 at 02:44)
lean#402: set builder notation (15 messages, latest: Jul 29 2020 at 08:26)
Sorry (5 messages, latest: Jul 28 2020 at 21:41)
#3223 homogeneous (6 messages, latest: Jul 28 2020 at 17:46)
#3606 R-Mod is abelian (12 messages, latest: Jul 28 2020 at 14:14)
#3595 mv_poly bundled homs (5 messages, latest: Jul 28 2020 at 08:40)
leanprover/vscode-lean#214 snippets for def, etc. (3 messages, latest: Jul 27 2020 at 13:38)
#3463 (26 messages, latest: Jul 26 2020 at 01:52)
#3473 (2 messages, latest: Jul 21 2020 at 14:10)
#3404 Jacobson (6 messages, latest: Jul 21 2020 at 06:15)
#3403 (20 messages, latest: Jul 21 2020 at 01:32)
#3444 and #3446 (16 messages, latest: Jul 21 2020 at 01:29)
#3384 selecting in widgets (2 messages, latest: Jul 20 2020 at 11:36)
3395: QPF (4 messages, latest: Jul 19 2020 at 23:36)
3454 add ne_bot (1 message, latest: Jul 19 2020 at 14:46)
#3230: padic_val_nat lemmas (8 messages, latest: Jul 18 2020 at 20:16)
#3407: polynomial refactor (41 messages, latest: Jul 16 2020 at 18:28)
#3398 (16 messages, latest: Jul 16 2020 at 06:37)
#3387: smooth functions on manifolds (56 messages, latest: Jul 15 2020 at 22:17)
lean#296 mention tactics in docstrings (1 message, latest: Jul 14 2020 at 06:25)
#3317: qpfs (6 messages, latest: Jul 13 2020 at 18:59)
#2879 continuity tactic (2 messages, latest: Jul 09 2020 at 12:00)
#3275 tensor polynomial (1 message, latest: Jul 07 2020 at 05:07)
3285: reorder imports (2 messages, latest: Jul 07 2020 at 04:38)
#3094, Perfect Numbers (58 messages, latest: Jul 06 2020 at 04:44)
#3200 pythagorean triples (7 messages, latest: Jul 04 2020 at 20:30)
#3274 pnat facts (17 messages, latest: Jul 04 2020 at 16:48)
#3241 rational root thm (1 message, latest: Jul 03 2020 at 17:55)
#3235 reduce imports (5 messages, latest: Jul 02 2020 at 11:16)
#3247 every abelian category is preadditive (11 messages, latest: Jul 02 2020 at 06:40)
#3210, openness of units (20 messages, latest: Jul 01 2020 at 19:42)
3083 finset lattice (120 messages, latest: Jun 30 2020 at 16:33)
3212 compl notation (39 messages, latest: Jun 29 2020 at 17:04)
#3221 remove universe annotations in category_theory (18 messages, latest: Jun 29 2020 at 15:59)
#3172 (3 messages, latest: Jun 29 2020 at 03:29)
#3180 Heine (5 messages, latest: Jun 28 2020 at 20:36)
#3207 padic_val_nat namespacing (7 messages, latest: Jun 28 2020 at 09:54)
lean#352 Syntactic horror or pure elegance? (17 messages, latest: Jun 26 2020 at 11:45)
#3114 rethinking the algebra hieararchy (30 messages, latest: Jun 19 2020 at 17:25)
linarith prs (10 messages, latest: Jun 19 2020 at 09:53)
leanprover/vscode-lean#170 Add missing Unicode subscripts… (1 message, latest: Jun 16 2020 at 05:55)
#1564 Chevalley–Warning (9 messages, latest: Jun 15 2020 at 17:50)
2844 (4 messages, latest: Jun 09 2020 at 20:48)
#2970 padic_val_nat (1 message, latest: Jun 06 2020 at 10:17)
#2953 submodule.subtype (6 messages, latest: Jun 04 2020 at 22:18)
lean#281 assumption? (2 messages, latest: Jun 04 2020 at 16:07)
2947 normal subgroups (5 messages, latest: Jun 04 2020 at 14:26)
#2860 countable categoricity of dense linear orders (7 messages, latest: Jun 03 2020 at 22:03)
2816 affine spaces (1 message, latest: May 31 2020 at 02:22)
#2847 displace zero_ne_one_class (25 messages, latest: May 29 2020 at 21:24)
lean#282 changing structure instance elaboration (7 messages, latest: May 28 2020 at 15:02)
#2843 group axioms (6 messages, latest: May 28 2020 at 08:32)
#2746 adjoints of linear maps (10 messages, latest: May 26 2020 at 04:48)
#2701 Primorial (6 messages, latest: May 24 2020 at 04:04)
#2720 torsors (22 messages, latest: May 23 2020 at 16:08)
lean#260 expr lens (19 messages, latest: May 22 2020 at 18:01)
#2714 localisations (41 messages, latest: May 22 2020 at 08:21)
2749 Implicit function theorem (32 messages, latest: May 21 2020 at 11:36)
2720 torsors (6 messages, latest: May 18 2020 at 15:08)
#2707 merge init_ into algebra (22 messages, latest: May 18 2020 at 12:56)
#2688 sum_choose_halfway (10 messages, latest: May 18 2020 at 07:47)
#2699 decidable_eq lattices (64 messages, latest: May 17 2020 at 18:44)
lean#229 (50 messages, latest: May 16 2020 at 18:18)
#2652 and #2655 left vs right (6 messages, latest: May 12 2020 at 06:54)
lean#216 dot notation (21 messages, latest: May 11 2020 at 21:32)
lean#227 pretty-print using dot notation (16 messages, latest: May 11 2020 at 14:28)
#2589 norm_num (67 messages, latest: May 09 2020 at 21:00)
#2609 reflections (4 messages, latest: May 07 2020 at 16:32)
#2513 formal assoc (9 messages, latest: May 06 2020 at 18:54)
lean#211 don't unfold irred defs (157 messages, latest: May 06 2020 at 00:11)
#2605 turing (2 messages, latest: May 05 2020 at 17:55)
lean#212 renaming tactic combinators (4 messages, latest: May 05 2020 at 11:18)
#2554 split list join (68 messages, latest: May 05 2020 at 09:13)
#2590 finite fields (12 messages, latest: May 02 2020 at 21:47)
#2578 free_monoid_product (11 messages, latest: May 01 2020 at 08:58)
#2566 group actions on ring (19 messages, latest: Apr 30 2020 at 13:20)
#2565 exponential split (11 messages, latest: Apr 29 2020 at 17:30)
#2522 coe lemmas between nat and fin (3 messages, latest: Apr 28 2020 at 04:56)
#2480 bilinear forms (188 messages, latest: Apr 24 2020 at 10:25)
#2511 refactor zmod (45 messages, latest: Apr 24 2020 at 05:20)
#2228 Inverse function thm (2 messages, latest: Apr 23 2020 at 20:29)
#2471 nth_rewrite (1 message, latest: Apr 22 2020 at 07:35)
#2140 bundled subgroups (24 messages, latest: Apr 14 2020 at 17:47)
#2382 is_eq_or_iff (13 messages, latest: Apr 10 2020 at 23:34)
#2303 refactor algebra (3 messages, latest: Apr 09 2020 at 13:55)
#2334 (14 messages, latest: Apr 08 2020 at 14:13)
#2332 (29 messages, latest: Apr 08 2020 at 07:39)
#2242 group with zero (14 messages, latest: Mar 31 2020 at 08:37)
#2264 deploy_docs fix (4 messages, latest: Mar 28 2020 at 17:41)
#2106 bump lean (2 messages, latest: Mar 18 2020 at 17:24)
#2004 monoid localisation (5 messages, latest: Mar 06 2020 at 17:22)
#2064 bump lean (3 messages, latest: Mar 05 2020 at 13:17)
#1368 fin_enum class (3 messages, latest: Mar 05 2020 at 00:56)
#1926 seminorms (6 messages, latest: Mar 04 2020 at 19:54)
#2030 (44 messages, latest: Mar 03 2020 at 04:27)
#2052 galois insertion lemmas (4 messages, latest: Mar 02 2020 at 07:06)
#1540 (short games and domineering) (3 messages, latest: Feb 28 2020 at 18:09)
#1596 case_bash on nat (2 messages, latest: Feb 24 2020 at 03:48)
category PRs (1 message, latest: Feb 21 2020 at 14:39)
#1914 formal roadmap (5 messages, latest: Feb 19 2020 at 17:29)
#2000 :tada: (1 message, latest: Feb 17 2020 at 01:36)
#1460 Infinite Ramsey (57 messages, latest: Feb 15 2020 at 20:46)
#1891 coe_boel_iff (4 messages, latest: Jan 18 2020 at 06:57)
#1835 more lie basics (6 messages, latest: Jan 12 2020 at 22:09)
#1823 (3 messages, latest: Dec 23 2019 at 12:35)
#1800 (3 messages, latest: Dec 13 2019 at 17:16)
#1798 (5 messages, latest: Dec 11 2019 at 20:21)
#1644 lie algebras (44 messages, latest: Nov 12 2019 at 09:56)
#1582 nhds notation (39 messages, latest: Nov 12 2019 at 08:25)
#1562 rel (8 messages, latest: Nov 11 2019 at 21:12)
#1647 push_cast (1 message, latest: Nov 05 2019 at 10:20)
#1601 attribute [class] nat.prime (24 messages, latest: Nov 05 2019 at 09:54)
#1617 and #1619, fixing timeouts with "by exact" (2 messages, latest: Oct 27 2019 at 02:27)
#1595 Dedekind's linear independence of characters (176 messages, latest: Oct 26 2019 at 20:59)
#1548 val_min_abs (1 message, latest: Oct 13 2019 at 16:29)
#1531 adjoin_root alg_hom (7 messages, latest: Oct 12 2019 at 16:51)
#1538 install doc (3 messages, latest: Oct 12 2019 at 16:43)
curly braces (5 messages, latest: Oct 10 2019 at 23:52)
#1521 rename type variables (126 messages, latest: Oct 10 2019 at 09:06)
#1528 sequential (9 messages, latest: Oct 09 2019 at 16:13)
1089 Commuting elements (4 messages, latest: Oct 04 2019 at 12:06)
#1493 (31 messages, latest: Sep 27 2019 at 22:27)
#1485 priority 10 (15 messages, latest: Sep 26 2019 at 01:15)
#1292 order of power series (2 messages, latest: Sep 25 2019 at 11:10)
#1449 minpoly (10 messages, latest: Sep 23 2019 at 10:51)
#1467 fconstructor (5 messages, latest: Sep 20 2019 at 22:47)
#1425 dim_finsupp (36 messages, latest: Sep 19 2019 at 09:32)
#1379 and #1380 concrete categories with bundled homs (3 messages, latest: Sep 19 2019 at 06:28)
Manifolds (73 messages, latest: Sep 09 2019 at 11:42)
#1372 Timeout (30 messages, latest: Sep 06 2019 at 16:14)
#1391 use classical (2 messages, latest: Sep 06 2019 at 11:13)
#1356 derive finite_products (65 messages, latest: Aug 31 2019 at 00:23)
#1368 enumerable class (6 messages, latest: Aug 30 2019 at 20:14)
#1366 add a lt relation independent from le for with_top (7 messages, latest: Aug 30 2019 at 15:38)
#1374 Comparing completions (1 message, latest: Aug 30 2019 at 11:31)
#1339 special shapes of limits (3 messages, latest: Aug 29 2019 at 23:27)
#1274 combinatorial games (4 messages, latest: Aug 25 2019 at 14:08)
#1295 archive (37 messages, latest: Aug 24 2019 at 21:45)
#1234 apply' (9 messages, latest: Aug 21 2019 at 20:51)
#1340 finite products give a monoidal structure (1 message, latest: Aug 20 2019 at 20:24)
#1346 remove simp lemmas for eq_to_hom (1 message, latest: Aug 20 2019 at 11:00)
#1341 produce associativity-friendly lemmas in category the (4 messages, latest: Aug 19 2019 at 13:10)
#1326 parse ematch lemmas with finish using ... (13 messages, latest: Aug 14 2019 at 15:42)
#1269 apply symmetry on assumptions (1 message, latest: Jul 27 2019 at 16:39)
potential PR's (8 messages, latest: Jul 14 2019 at 15:32)
#1222 provide trace! and fail! and allow tactic (2 messages, latest: Jul 13 2019 at 14:50)
#1223 extend the API of finmap (3 messages, latest: Jul 13 2019 at 01:25)
#1194 format! macro using pp instead of to_fmt (4 messages, latest: Jul 09 2019 at 15:49)
#1076 powers mod n (36 messages, latest: Jul 09 2019 at 04:19)
#1136 tangent cone (13 messages, latest: Jul 08 2019 at 15:27)
#768 jacobson radical (2 messages, latest: Jul 08 2019 at 06:47)
#1176 monads (18 messages, latest: Jul 06 2019 at 10:48)
#943 lc refactor (137 messages, latest: Jul 03 2019 at 11:37)
#1160 fundamental groupoid (5 messages, latest: Jul 01 2019 at 20:54)
#1103 fixing norm_cast (3 messages, latest: Jun 20 2019 at 14:37)
#1102 local rings (10 messages, latest: Jun 19 2019 at 11:29)
#461 integral closure (21 messages, latest: Jun 16 2019 at 19:32)
#1119 arrow_congr (1 message, latest: Jun 11 2019 at 17:11)
#840 Hermitian inner product space (28 messages, latest: Jun 10 2019 at 11:17)
#1118 Presented groups (1 message, latest: Jun 07 2019 at 04:26)
#988 norm_cast (27 messages, latest: Jun 04 2019 at 11:27)
#1085 topological modules (4 messages, latest: Jun 03 2019 at 19:47)
#1073 pnat (2 messages, latest: Jun 03 2019 at 13:05)
#1067 open subgroups (1 message, latest: May 30 2019 at 05:29)
#1074 category instances to root (29 messages, latest: May 29 2019 at 17:27)
#1088 counting measure (2 messages, latest: May 27 2019 at 21:14)
#856 submodules of algebra form semiring (8 messages, latest: May 27 2019 at 10:29)
#1080 props of elements in rings (11 messages, latest: May 24 2019 at 14:45)
#1049 refactor CommRing adjunctions (14 messages, latest: May 23 2019 at 06:19)
#1066 Battle of Hastings (2 messages, latest: May 20 2019 at 17:43)
lean –export problems with #999 (12 messages, latest: May 18 2019 at 01:41)
#1029 group conjugates (34 messages, latest: May 17 2019 at 05:05)
#734 free ring (51 messages, latest: May 15 2019 at 17:08)
#1007 compatibility with Lean 3.5.0c (11 messages, latest: May 11 2019 at 16:51)
#1002 monoidal cats (2 messages, latest: May 10 2019 at 06:44)
#963 set-theory cardinals etc (1 message, latest: May 09 2019 at 17:56)
#993 comp2 (11 messages, latest: May 08 2019 at 19:13)
#966 more derivatives (57 messages, latest: May 05 2019 at 05:41)
#835 hyperreals (5 messages, latest: May 04 2019 at 08:28)
#951 inj_iff_trivial_ker (19 messages, latest: May 01 2019 at 18:10)
#878 remove dependencies (64 messages, latest: Apr 28 2019 at 21:52)
#927 operator norm (9 messages, latest: Apr 20 2019 at 22:06)
#931 complete lattices have (co)limits (5 messages, latest: Apr 18 2019 at 18:09)
#938 special shapes (2 messages, latest: Apr 17 2019 at 02:34)
#923 ring of ctu functions (1 message, latest: Apr 15 2019 at 08:45)
#726 bundled bounded linear maps [wip] (44 messages, latest: Apr 14 2019 at 08:59)
#893 whiskering natural isomorphisms (2 messages, latest: Apr 08 2019 at 23:56)
#904-905 (3 messages, latest: Apr 08 2019 at 19:17)
#830 feat(analysis/normed_space/deriv): show that the differ (2 messages, latest: Apr 08 2019 at 09:58)
#881 dual vector spaces (2 messages, latest: Apr 08 2019 at 07:30)
#886 presheaves (28 messages, latest: Apr 08 2019 at 02:55)
mergify (343 messages, latest: Apr 07 2019 at 01:56)
colimits (98 messages, latest: Apr 03 2019 at 21:41)
#883 (1 message, latest: Apr 03 2019 at 14:08)
#854 pointwise operations for sets (10 messages, latest: Apr 03 2019 at 06:32)
#822 Compute the first three digits of pi (47 messages, latest: Apr 01 2019 at 17:09)
#819 card finite fields (3 messages, latest: Apr 01 2019 at 06:56)
#820 lexicographic orders (15 messages, latest: Mar 31 2019 at 23:47)
#766 cache-olean (83 messages, latest: Mar 31 2019 at 23:37)
#850 mul_action (58 messages, latest: Mar 28 2019 at 06:43)
#851 FTA (12 messages, latest: Mar 26 2019 at 21:25)
#789 extensions of equiv (34 messages, latest: Mar 21 2019 at 12:41)
#825 (semi)modules and linear_map (5 messages, latest: Mar 16 2019 at 18:58)
#749 (5 messages, latest: Mar 16 2019 at 12:28)
#801 hyperreals (1 message, latest: Mar 09 2019 at 09:57)
#800 (7 messages, latest: Mar 08 2019 at 14:20)
#802 two lemmas about powers of elements (1 message, latest: Mar 07 2019 at 21:59)
#797 count and bag_inter (3 messages, latest: Mar 07 2019 at 15:12)
#781 fraction_map (4 messages, latest: Mar 05 2019 at 15:54)
#787 uniform split (9 messages, latest: Mar 05 2019 at 12:57)
#748 asymptotics and the Fréchet derivative (55 messages, latest: Mar 05 2019 at 02:35)
#611 limits shapes (2 messages, latest: Mar 01 2019 at 22:16)
#780 (20 messages, latest: Mar 01 2019 at 12:56)
#773 Prime Avoidance (1 message, latest: Mar 01 2019 at 10:01)
#774 Chinese Remainder Theorem (40 messages, latest: Mar 01 2019 at 10:00)
#775 (6 messages, latest: Feb 28 2019 at 15:18)
#705 (2 messages, latest: Feb 28 2019 at 08:30)
#772 remove unnecessary assumption from card_eq_succ (4 messages, latest: Feb 27 2019 at 22:02)
#763 subset/inter/union for opens(X) (61 messages, latest: Feb 26 2019 at 18:30)
#734 free_ring and free_comm_ring (36 messages, latest: Feb 21 2019 at 19:06)
#735 free magma, semigroup, monoid (138 messages, latest: Feb 21 2019 at 15:20)
#717 field_hom (8 messages, latest: Feb 16 2019 at 20:51)
#728 continuation passing monad (12 messages, latest: Feb 15 2019 at 06:05)
#707 Automate the deployment of nightly builds (46 messages, latest: Feb 12 2019 at 14:51)
#711 Calculus (47 messages, latest: Feb 11 2019 at 07:58)
#706 refactor geo_sum (1 message, latest: Feb 09 2019 at 15:40)
#691 quotient.ind' (1 message, latest: Feb 06 2019 at 18:12)
#664 subalgebra_of_subring (3 messages, latest: Feb 02 2019 at 18:40)
#666 div_zero (14 messages, latest: Feb 02 2019 at 02:37)
#665 lcm (9 messages, latest: Feb 01 2019 at 09:55)
#658 multiplication of submodules (5 messages, latest: Jan 31 2019 at 22:18)
#528 splitting fields (4 messages, latest: Jan 29 2019 at 19:45)
#567 (2 messages, latest: Jan 29 2019 at 19:09)
#410 backwards reasoning (175 messages, latest: Jan 26 2019 at 17:27)
#376 foldl (4 messages, latest: Jan 26 2019 at 17:26)
#536 algebra over comm_ring (58 messages, latest: Jan 24 2019 at 17:06)
#619 adjunctions: defs (1 message, latest: Jan 23 2019 at 15:30)
#538 opposites (167 messages, latest: Jan 23 2019 at 15:04)
#593 Add default setup for VS Code (11 messages, latest: Jan 23 2019 at 11:52)
#510 opposite categories (30 messages, latest: Jan 22 2019 at 14:14)
#610 (16 messages, latest: Jan 20 2019 at 20:24)
#605 unique (3 messages, latest: Jan 18 2019 at 21:40)
#598 analysis reorganization (34 messages, latest: Jan 18 2019 at 20:08)
#489 where (83 messages, latest: Jan 17 2019 at 10:21)
#583 move everything into src (25 messages, latest: Jan 16 2019 at 18:29)
#568 metric namespace (14 messages, latest: Jan 13 2019 at 21:59)
#549 over categories (10 messages, latest: Jan 05 2019 at 21:05)
#574 quotient_ker_equiv_range (12 messages, latest: Jan 05 2019 at 14:20)
#376 fold (31 messages, latest: Dec 27 2018 at 20:03)
#483 polar coordinates (110 messages, latest: Dec 27 2018 at 08:50)
#481 localization (18 messages, latest: Dec 22 2018 at 04:40)
Small and straightforward PRs (6 messages, latest: Dec 20 2018 at 14:02)
#512 discrete categories (13 messages, latest: Dec 20 2018 at 09:28)
#428 Banach Contraction (42 messages, latest: Dec 17 2018 at 20:15)
#522 enat (9 messages, latest: Dec 17 2018 at 19:10)
#458 Sylow (5 messages, latest: Dec 17 2018 at 17:05)
#495 multiplicity (24 messages, latest: Dec 17 2018 at 14:06)
#484 miscellaneous topology (7 messages, latest: Dec 10 2018 at 09:09)
#507 functoriality of (co)cones (4 messages, latest: Dec 07 2018 at 17:49)
#494 limits-2 (45 messages, latest: Dec 02 2018 at 22:39)
#473 limits and colimits (100 messages, latest: Dec 02 2018 at 05:10)
#431 apply to_additive recursively (2 messages, latest: Nov 30 2018 at 15:55)
#503 comma (9 messages, latest: Nov 30 2018 at 14:14)
#479 equivalences (44 messages, latest: Nov 28 2018 at 20:39)
#480 Yoneda fixes (14 messages, latest: Nov 28 2018 at 08:05)
#486 use (46 messages, latest: Nov 27 2018 at 08:59)
#496 Ico (16 messages, latest: Nov 26 2018 at 13:55)
#478 associators and unitors for functor composition (1 message, latest: Nov 15 2018 at 20:49)
#468 revised limits PR (6 messages, latest: Nov 15 2018 at 20:07)
rebasing (26 messages, latest: Nov 14 2018 at 11:17)
#392 emetric spaces (31 messages, latest: Nov 09 2018 at 13:48)
#463 removing coercions from category_theory/ (34 messages, latest: Nov 08 2018 at 09:16)
#462 ideal operations (61 messages, latest: Nov 07 2018 at 23:38)
#311 dfinsupp and direct sum (2 messages, latest: Nov 06 2018 at 11:42)
#459 is_iso.inv (9 messages, latest: Nov 05 2018 at 19:11)
#431 recursive to_additive (4 messages, latest: Nov 05 2018 at 17:19)
#453 irrational.lean (4 messages, latest: Nov 05 2018 at 14:14)
#442 troubles with with_bot (4 messages, latest: Nov 02 2018 at 13:19)
#443 docs for N -> Z -> Q -> R -> C (129 messages, latest: Oct 29 2018 at 18:59)
#441 poly_comp (9 messages, latest: Oct 25 2018 at 07:09)
#436 supercharging conv (3 messages, latest: Oct 24 2018 at 08:29)
#438 and #439 conv: ring and norm_num (1 message, latest: Oct 23 2018 at 10:54)
#434 ultrafilter monad (1 message, latest: Oct 22 2018 at 02:27)
#429 finite subgroups of integral domain (7 messages, latest: Oct 20 2018 at 09:18)
#85 monotonicity (52 messages, latest: Oct 18 2018 at 14:03)
#427 opens (3 messages, latest: Oct 18 2018 at 08:08)
#425 perfect closure (4 messages, latest: Oct 18 2018 at 07:32)
vscode - add unicode completion to markdown files (1 message, latest: Oct 17 2018 at 14:20)
#416 limits and colimits (64 messages, latest: Oct 17 2018 at 10:43)
#422 limits in CommRing (49 messages, latest: Oct 15 2018 at 09:07)
#419 nat.prime.dvd_choose (1 message, latest: Oct 14 2018 at 22:51)
#420 constructions of limits (14 messages, latest: Oct 14 2018 at 22:50)
#118 direct limit (23 messages, latest: Oct 14 2018 at 20:34)
#417 open_set (1 message, latest: Oct 12 2018 at 10:56)
trailing whitespace (4 messages, latest: Oct 10 2018 at 18:24)
#412 updates to installation instructions (1 message, latest: Oct 10 2018 at 10:09)
#391 faster (197 messages, latest: Oct 08 2018 at 19:42)
#352 fin_cases (47 messages, latest: Oct 08 2018 at 17:01)
determinants (23 messages, latest: Oct 08 2018 at 08:00)
#406 det is a monoid_hom (1 message, latest: Oct 08 2018 at 07:57)
#397 (8 messages, latest: Oct 08 2018 at 01:13)
#396 squeeze_simp (36 messages, latest: Oct 07 2018 at 19:28)
topic names (10 messages, latest: Oct 07 2018 at 12:20)
documentation PRs (2 messages, latest: Oct 07 2018 at 11:21)
hello (1 message, latest: Oct 07 2018 at 10:24)

Last updated: Dec 20 2025 at 21:32 UTC