Zulip Chat Archive

Stream: PR reviews

Topics:

#9116 Introducing Complex.slitPlane (38 messages, latest: Dec 19 2023 at 18:41)
#16040 Spin Group (35 messages, latest: Dec 19 2023 at 14:22)
#7506 : compatible measures on quotient spaces and groups (3 messages, latest: Dec 19 2023 at 04:09)
#9145 Refactor of succAbove etc. (1 message, latest: Dec 19 2023 at 00:41)
#9114 API for ltByCases (101 messages, latest: Dec 17 2023 at 09:12)
Integral curves on manifolds (7 messages, latest: Dec 17 2023 at 06:21)
#9079 Golfing simps (10 messages, latest: Dec 17 2023 at 00:28)
#9006 Unit subgroup (3 messages, latest: Dec 16 2023 at 02:58)
#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)
#7386 Linear Programming (34 messages, latest: Dec 12 2023 at 21:00)
#8732 (Matroid Duality) (1 message, latest: Dec 12 2023 at 15:07)
PR #6042 Singular Value Decomposition (40 messages, latest: Dec 12 2023 at 09:22)
#8435: run hint tactics in parallel (9 messages, latest: Dec 12 2023 at 01:12)
#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)
#8878 refactor(ProperCone) (1 message, latest: Dec 07 2023 at 19:54)
#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)
#6045 refactor IsLocalRingHom (19 messages, latest: Nov 28 2023 at 21:24)
#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)
std4#314 (2 messages, latest: Nov 15 2023 at 12:18)
#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)
#8013 Walking Reflexive Pair (3 messages, latest: Nov 04 2023 at 10:55)
#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)
#6057 MulActionHom in the semilinear style (6 messages, latest: Oct 27 2023 at 16:07)
#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)
#6307 refactor of monoidal categories (16 messages, latest: Sep 21 2023 at 09:32)
#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)
#3730 Remove Cat suffix (4 messages, latest: Aug 30 2023 at 06:59)
✔ #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)
#13483 move_add (65 messages, latest: Jul 10 2022 at 10:56)
#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 2023 at 11:08 UTC