Zulip Chat Archive
Stream: PR reviews
Topics:
- Jeremy Tan's open PRs (110 messages, latest: Feb 28 2026 at 08:44)
- #25834 girth-diameter inequality (9 messages, latest: Feb 27 2026 at 22:24)
- PR #35857: Bijective Base-2 Numeration (3 messages, latest: Feb 27 2026 at 20:18)
- mathlib4#34521 & mathlib4#34435 (Probability/MeasureTheory) (1 message, latest: Feb 27 2026 at 14:09)
- #34013 chore: golf with grind to reduce explicit lemma refer (33 messages, latest: Feb 27 2026 at 03:43)
- #34697 the Euclidean volume measure (23 messages, latest: Feb 27 2026 at 02:42)
- #34773 Adds generic Shannon Entropy definition over PMF (5 messages, latest: Feb 26 2026 at 16:53)
- #35732 Reproducing Kernels (8 messages, latest: Feb 26 2026 at 10:13)
- #34554 calculate divisors using prime factorization (7 messages, latest: Feb 25 2026 at 14:12)
- #35464 (2 messages, latest: Feb 25 2026 at 10:25)
- #35753 and #35755: forward Euler method for ODEs (1 message, latest: Feb 25 2026 at 08:28)
- #35467 Schreier and Cayley graphs (8 messages, latest: Feb 24 2026 at 15:56)
- Stieltjes vector measures #34055 (20 messages, latest: Feb 23 2026 at 21:47)
- #34402 UpperHalfPlane invariant measure (1 message, latest: Feb 23 2026 at 17:17)
- #35670 completeness of adic completion (5 messages, latest: Feb 23 2026 at 03:13)
- PRs towards IMO geometry 2024 P4 (20 messages, latest: Feb 21 2026 at 01:50)
- #34866 Adds characteristic function and more to binomial (4 messages, latest: Feb 19 2026 at 03:36)
- #35376 - orientable manifolds (43 messages, latest: Feb 18 2026 at 21:23)
- #26221 Towards geodesics and the Levi-Civita connection (88 messages, latest: Feb 18 2026 at 09:36)
- #34937 adding upper semi lattice instance to Turing degrees (2 messages, latest: Feb 17 2026 at 00:40)
- Heights (22 messages, latest: Feb 16 2026 at 14:49)
- Immersions and smooth embeddings (27 messages, latest: Feb 14 2026 at 19:57)
- Results on maximal acyclic subgraphs (12 messages, latest: Feb 14 2026 at 09:30)
- using
@\[to_dual\]more (20 messages, latest: Feb 14 2026 at 04:33) - Real Closed Field (31 messages, latest: Feb 14 2026 at 00:35)
- Polygons PR (20 messages, latest: Feb 13 2026 at 05:10)
- #33895 primrec list_take, list_drop, list_modify, list_set (1 message, latest: Feb 12 2026 at 10:44)
- #31607 rename continuousOn_const and friends (4 messages, latest: Feb 11 2026 at 20:13)
- #34944 negOnePow ↔ natAbs bridge lemmas (1 message, latest: Feb 11 2026 at 16:05)
- flatness of MvPowerSeries (13 messages, latest: Feb 11 2026 at 08:34)
- More angle bisection lemmas #30474, #30476, #30477, … (14 messages, latest: Feb 10 2026 at 13:45)
- #35010 add notation for whiskerLeftIso and whiskerRightIso (4 messages, latest: Feb 09 2026 at 19:54)
- Tempered distributions (40 messages, latest: Feb 09 2026 at 11:30)
- #34868 – more general polynomial asymptotics (29 messages, latest: Feb 09 2026 at 10:26)
- #35011 add degree of copy less than original (1 message, latest: Feb 09 2026 at 08:27)
- #34830 Adds Categorical Groups aka 2-groups (5 messages, latest: Feb 09 2026 at 05:20)
- #33928 indexed families of tiles (1 message, latest: Feb 09 2026 at 00:22)
- #34875 adds Sherman-Morrison formula (11 messages, latest: Feb 07 2026 at 18:23)
- #33985, #34054, #34093: OmegaCompletePartialOrder instances (1 message, latest: Feb 07 2026 at 15:14)
- #34940 - graph of a continuous function on a mfld is a mfld (1 message, latest: Feb 07 2026 at 06:57)
- #34899 -
SemiLatticeSupinstance for the Turing degrees (1 message, latest: Feb 06 2026 at 06:34) - #34670
(f ⊔ g) iisn't pretty-printed (1 message, latest: Feb 03 2026 at 08:36) - Ore's Theorem (16 messages, latest: Feb 02 2026 at 09:12)
- #34551 Adds HasMulAntidiagonal and links to HasAntidiagonal (10 messages, latest: Jan 31 2026 at 18:14)
- #33257 Odd Cycle Theorem (32 messages, latest: Jan 31 2026 at 14:27)
- #34616 feat(RingTheory/PowerSeries/Derivative): more lemmas (1 message, latest: Jan 30 2026 at 16:17)
- AKS primality test (1 message, latest: Jan 28 2026 at 02:08)
- #30526 use Subrelation in Mathlib.Logic.Relation (22 messages, latest: Jan 26 2026 at 21:55)
- #32851 add exists_accPt_of_noAtoms (3 messages, latest: Jan 22 2026 at 18:50)
- #34220 feat(RingTheory/PowerSeries): dedicated file for exp (5 messages, latest: Jan 22 2026 at 18:34)
- #32856 definition of an irreducible representation (1 message, latest: Jan 22 2026 at 18:00)
- #34249 MulDistribMulActionHom (3 messages, latest: Jan 22 2026 at 12:38)
- #34138 feat(MeasureTheory): Introduce
MassFunction α(1 message, latest: Jan 21 2026 at 19:21) - #30618 Glaisher's theorem & other Nat.Partition stuff (6 messages, latest: Jan 21 2026 at 01:47)
- Simplex reindexing PRs (6 messages, latest: Jan 21 2026 at 00:27)
- #33960 not on queue? (2 messages, latest: Jan 20 2026 at 21:24)
- #32892 arithmetic-geometric mean (6 messages, latest: Jan 20 2026 at 14:58)
- #31719 Borel-Caratheodory (3 messages, latest: Jan 18 2026 at 16:51)
- Add Pi.mulSingle_eq_mulIndicator (13 messages, latest: Jan 18 2026 at 07:28)
- Generalize FinSupp.single_eq_set_indicator (1 message, latest: Jan 18 2026 at 05:14)
- #12076 Orzech's theorem (67 messages, latest: Jan 16 2026 at 22:11)
- #33817 the small Schröder numbers and the generating functio (7 messages, latest: Jan 16 2026 at 07:46)
- #30987 SpecialLinearGroup of a module (10 messages, latest: Jan 15 2026 at 12:54)
- #33851 deprecate CancelMonoidWithZero (7 messages, latest: Jan 15 2026 at 10:28)
- Error: The action 'lint mathlib' has timed out after 30 minu (2 messages, latest: Jan 15 2026 at 07:59)
- Generation of the general linear group (9 messages, latest: Jan 13 2026 at 14:13)
- #31444 fix LaTeX typo (1 message, latest: Jan 12 2026 at 23:03)
- #32702 move
Finite G.ConnectedComponentinstance (1 message, latest: Jan 10 2026 at 20:36) - #33523 tiles and protosets for tilings (1 message, latest: Jan 10 2026 at 01:34)
- #33744 Class Group of a Unique Factorization Domain is trivi (4 messages, latest: Jan 09 2026 at 07:47)
- #33409 Ceva's theorem (1 message, latest: Jan 08 2026 at 14:20)
- #33613 Lint timing out (2 messages, latest: Jan 06 2026 at 20:04)
- #33449 Poisson limit theorem (1 message, latest: Jan 04 2026 at 09:33)
- #33195 stacks (9 messages, latest: Jan 03 2026 at 09:20)
- #33411 Discrete convolution API proposal (3 messages, latest: Dec 31 2025 at 16:34)
- #33130 improved typeclass structure, awaiting review (22 messages, latest: Dec 29 2025 at 05:13)
- #27282 Real algebra (5 messages, latest: Dec 28 2025 at 19:10)
- Adding scan combinators to batteries (1 message, latest: Dec 28 2025 at 03:15)
- #30881 Generating functions for large Schröder numbers (1 message, latest: Dec 27 2025 at 09:46)
- PR 33276 Review (5 messages, latest: Dec 26 2025 at 18:24)
- PR #31821 Singular Value Decomposition (55 messages, latest: Dec 25 2025 at 23:47)
- #32769 Multiplication of functions and distributions (1 message, latest: Dec 23 2025 at 23:56)
- Review request: Rayleigh quotient bounds (PR #33075) (1 message, latest: Dec 21 2025 at 13:21)
- #33034 removing privateInPublic from lakefile (55 messages, latest: Dec 19 2025 at 19:52)
- #26446 full subcategories refactor (5 messages, latest: Dec 18 2025 at 13:51)
- (merged) #32776 grind and aesop annotations for ZMod (8 messages, latest: Dec 17 2025 at 23:18)
- #30089 modular forms bounds (1 message, latest: Dec 16 2025 at 07:03)
- #30511 use fun_prop in measurability (18 messages, latest: Dec 12 2025 at 19:08)
- (Classical) Distributions (42 messages, latest: Dec 12 2025 at 16:32)
- Prokhorov theorem #32701 (11 messages, latest: Dec 12 2025 at 11:59)
- Actually removing deprecated modules (5 messages, latest: Dec 12 2025 at 07:13)
- #32116 - stuck in a pause (2 messages, latest: Dec 12 2025 at 01:19)
- feat: register mathlib tactics with try? (4 messages, latest: Dec 10 2025 at 04:54)
- #32599 – make
Complex.expanirreducible_def(14 messages, latest: Dec 08 2025 at 21:50) - #29422 [LinearOrder α] [DecidableEq α] (33 messages, latest: Dec 08 2025 at 04:06)
- #32079 UniformContinuous version of uniform limit theorem (1 message, latest: Dec 06 2025 at 22:26)
- #30669 doc(Algebra): fix typos (2 messages, latest: Dec 05 2025 at 22:01)
- chore(Algebra): extract
Submonoid.IsLocalizationMap#29596 (8 messages, latest: Dec 04 2025 at 23:20) - #32374 (3 messages, latest: Dec 04 2025 at 22:57)
- #32379 prove smooth function is non-analytic (2 messages, latest: Dec 03 2025 at 18:52)
- #30570 SimpleGraph reachabilitySet (1 message, latest: Dec 02 2025 at 00:54)
- #29602 Infinite conditional sums API (197 messages, latest: Nov 30 2025 at 11:34)
- feat:
#grind_lint check in module Mathlib#31866 (14 messages, latest: Nov 28 2025 at 16:06) - #29734 irreducibility of kernels (3 messages, latest: Nov 27 2025 at 13:41)
- #30273 (already merged) (28 messages, latest: Nov 26 2025 at 19:35)
- #8435: run hint tactics in parallel (10 messages, latest: Nov 26 2025 at 05:24)
- #31294 feat(Analysis): Weierstrass ℘ functions (5 messages, latest: Nov 25 2025 at 11:54)
- feat: fix_deprecations.py script #30994 (4 messages, latest: Nov 24 2025 at 18:11)
- grind annotations (5 messages, latest: Nov 23 2025 at 03:33)
- #28604 NonAssocComm(Semi)ring (3 messages, latest: Nov 21 2025 at 22:29)
- #30678 Module and fast_instance% for Quaternion (1 message, latest: Nov 21 2025 at 16:15)
- #30181 reducible strong recursion (2 messages, latest: Nov 21 2025 at 15:36)
- #29856 add nonassociative normed rings (45 messages, latest: Nov 20 2025 at 12:23)
- #23238 extended floor and ceil (13 messages, latest: Nov 20 2025 at 07:16)
- #31789 More fast_instance% (20 messages, latest: Nov 19 2025 at 13:52)
- #30855 deprecate IsTotal in favour of Std.Total (1 message, latest: Nov 18 2025 at 16:09)
- feat: extract_goal preserves explicit foralls #31342 (1 message, latest: Nov 18 2025 at 01:33)
- #31653 Følner filters (1 message, latest: Nov 16 2025 at 09:05)
- #16981 Open normal subgroup in clopen nhds (45 messages, latest: Nov 15 2025 at 13:52)
- Feedback requested on PR #30962: lattice path lemmas (3 messages, latest: Nov 15 2025 at 00:16)
- #26110 sharp monoid (2 messages, latest: Nov 14 2025 at 17:39)
- [#28325 LocallyCompactSpace Γ₀ ↔ Nonempty (LocallyFiniteOrder](topic/.2328325.20LocallyCompactSpace.20.CE.93.E2.82.80.20.E2.86.94.20Nonempty.20(LocallyFiniteOrder.html) (1 message, latest: Nov 14 2025 at 17:38)
- #24730 feat(RingTheory): group-like elements (3 messages, latest: Nov 14 2025 at 11:12)
- aristotle task for command palette (10 messages, latest: Nov 13 2025 at 08:10)
- #26986 bijection between partitions of n and n - r (3 messages, latest: Nov 10 2025 at 05:40)
- #30791 generalizing
IsGaloisGroup(67 messages, latest: Nov 09 2025 at 19:06) - #30960 golf Combinatorics.SimpleGraph.Walk (1 message, latest: Nov 07 2025 at 04:05)
- #29028 define unitary R →* StarAlgEquiv S R R (30 messages, latest: Nov 06 2025 at 10:09)
- #30913 feat(Computability/Language):add subtraction notation (9 messages, latest: Nov 06 2025 at 10:03)
- #22639 (cyclically) reduced words (40 messages, latest: Nov 06 2025 at 09:22)
- #26510: feat(Matroid): exchange lemmas involving closure (4 messages, latest: Nov 05 2025 at 18:45)
- PRs from Toric (52 messages, latest: Nov 04 2025 at 21:40)
- #30285 document Spec(R) (1 message, latest: Nov 02 2025 at 16:22)
- #11060 add min max list operations (1 message, latest: Nov 02 2025 at 11:13)
- #30881 the generating function for large and small Schroder (1 message, latest: Nov 02 2025 at 04:15)
- #30609 Define large and small Schröder numbers (1 message, latest: Nov 02 2025 at 04:04)
- #27308 IsSymmetricAlgebra (8 messages, latest: Nov 02 2025 at 02:01)
- #27824 exists_gt_of_deriv_pos (18 messages, latest: Oct 31 2025 at 18:28)
- #25140 Hahn embedding theorem (124 messages, latest: Oct 31 2025 at 18:21)
- #12190
havevsletlinter (100 messages, latest: Oct 31 2025 at 18:21) - #28198 instances for EuclideanSpace rank (13 messages, latest: Oct 31 2025 at 17:02)
- #26793 proves on difference sequences in combinatorial Math (14 messages, latest: Oct 31 2025 at 05:06)
- #30759 remove declarations deprecated before 2025-04-21 (8 messages, latest: Oct 30 2025 at 15:46)
- #30854 theorems on affine independence and automorphisms (9 messages, latest: Oct 28 2025 at 13:52)
- #29735 order instances on quotients (2 messages, latest: Oct 27 2025 at 14:40)
- #30553 splitting SchwartzSpace (1 message, latest: Oct 27 2025 at 04:19)
- #30389 correctly apply
hintpriority (1 message, latest: Oct 26 2025 at 01:57) - Request for review: #27414 semilinear sets intersect/compl (1 message, latest: Oct 25 2025 at 15:15)
- #30782 chore(ModelTheory/PartialEquiv): use grind… (1 message, latest: Oct 23 2025 at 12:42)
- #30814 Rank decomposition and bases adapted to a linear map (3 messages, latest: Oct 23 2025 at 10:35)
- #29040 Erroneous "Unused import" linter (10 messages, latest: Oct 23 2025 at 10:05)
- #30783 chore(MeasureTheory/Covering): simp adaptation notes (2 messages, latest: Oct 22 2025 at 18:00)
- #26464 generators of pi tensor products (2 messages, latest: Oct 21 2025 at 14:44)
- #30400 super simple universe change (1 message, latest: Oct 21 2025 at 09:51)
- #30615 norm_num for rpow, renaming of norm_num lemmas (9 messages, latest: Oct 19 2025 at 14:39)
- #28818, style issue for forall implications (7 messages, latest: Oct 19 2025 at 09:21)
- #26330: Junk values (35 messages, latest: Oct 18 2025 at 04:42)
- #28399 feat: ring-theoretic fractions in Rat (2 messages, latest: Oct 17 2025 at 13:57)
- #30586 Inductive definition of IsAdmissible (10 messages, latest: Oct 16 2025 at 10:10)
- #30313 feat(Data/List/Sigma): grind annotations, missing API (2 messages, latest: Oct 14 2025 at 00:48)
- #30341 limits for ProfiniteAddGrp (1 message, latest: Oct 13 2025 at 20:58)
- #29207 reorder Algebra.MonoidAlgebra.Defs (7 messages, latest: Oct 13 2025 at 08:45)
- #9820 homogeneous submodule (8 messages, latest: Oct 11 2025 at 20:42)
- #29413, #29418, #29656 incenter, simplex interior, bisector (4 messages, latest: Oct 07 2025 at 12:20)
- #30244 misc. generalizations by LLM (13 messages, latest: Oct 06 2025 at 06:30)
- #30183 move factorial theorem (11 messages, latest: Oct 05 2025 at 22:07)
- #28871 Tournaments (1 message, latest: Oct 04 2025 at 13:13)
- #29582 rename docs#prop to Prop.finite (43 messages, latest: Sep 30 2025 at 07:53)
- #29914 Infinite conditional sums API (redux) (1 message, latest: Sep 27 2025 at 20:45)
- #29437 Seq.subsequence (8 messages, latest: Sep 26 2025 at 21:22)
- #28818
Setoid.ker_lift(29 messages, latest: Sep 25 2025 at 06:03) - #27082, #27639 preliminary of semilinear set PRs (3 messages, latest: Sep 24 2025 at 13:59)
- #28669 chore: clean up some proofs about locally compact val (15 messages, latest: Sep 23 2025 at 16:48)
- #29362 periods of lists and the Periodicity Lemma (4 messages, latest: Sep 23 2025 at 08:25)
- #26031 the derived category is linear (3 messages, latest: Sep 22 2025 at 14:44)
- #28803 refactor: unbundle algebra from
ENormed*(114 messages, latest: Sep 22 2025 at 09:32) - Simprocs blog post 2 (1 message, latest: Sep 21 2025 at 20:39)
- #29364
field_simpfor inequalities (6 messages, latest: Sep 20 2025 at 14:24) - #29334 Should grind be preferred to linear_combination? (56 messages, latest: Sep 19 2025 at 11:11)
- #29639 (15 messages, latest: Sep 19 2025 at 07:31)
- #29788 add bundled ContinuousMaps: allegedly unused import (14 messages, latest: Sep 19 2025 at 02:21)
- PR #29713: Euler-Poincaré formula (3 messages, latest: Sep 18 2025 at 11:39)
- #28702:
MulOneandMonoidHom(8 messages, latest: Sep 18 2025 at 00:06) - #26129 triangle inequality for angles (9 messages, latest: Sep 17 2025 at 19:05)
- #28484 More golfs in Data (1 message, latest: Sep 17 2025 at 17:24)
- #29058 Colex type alias (4 messages, latest: Sep 17 2025 at 15:21)
- # 29464 corrections to docs by way of LLM (24 messages, latest: Sep 16 2025 at 07:49)
- cutsat and grobner macro frontends to grind #29468 (2 messages, latest: Sep 16 2025 at 01:15)
- #29588 basic residue definitions (14 messages, latest: Sep 14 2025 at 20:29)
- #29115: develop some more limUnder API (16 messages, latest: Sep 12 2025 at 17:51)
- representation of reals in [0, 1] in positional system (39 messages, latest: Sep 11 2025 at 21:01)
- HasPrimitives on disc #9598 (4 messages, latest: Sep 11 2025 at 12:48)
- #6718 Lindemann-Weierstrass Theorem (20 messages, latest: Sep 11 2025 at 11:52)
- #29092 absolutely continuous functions (12 messages, latest: Sep 10 2025 at 19:48)
- #25201 Upper bound of dimension of polynomial ring (14 messages, latest: Sep 10 2025 at 09:02)
- #29057 AddCircle.liftIoc_continuous (3 messages, latest: Sep 09 2025 at 14:56)
- could someone please take a look at mathlib4 PR #28175 (2 messages, latest: Sep 09 2025 at 11:55)
- #28589 More lemmas on char 2 rings (1 message, latest: Sep 06 2025 at 06:54)
- #26453 PNat and Order instances (3 messages, latest: Sep 05 2025 at 15:33)
- 3 basic definitions (39 messages, latest: Sep 04 2025 at 13:30)
- #27288 semilinearizing some of
TensorProduct/Basic(1 message, latest: Sep 03 2025 at 17:01) - #29162 generalize Schroeder-Bernstein theorem (2 messages, latest: Sep 03 2025 at 06:39)
- #28469 WithLp equivalences (16 messages, latest: Sep 02 2025 at 20:14)
- #24532 fill out the `FreeProduct.asPowers namespace (2 messages, latest: Sep 02 2025 at 06:25)
- #28533
linarith?(1 message, latest: Sep 02 2025 at 03:06) - #29114 Mean value theorem for integrals (1 message, latest: Sep 01 2025 at 09:03)
- Basic lemmas for
ContMDiff(3 messages, latest: Sep 01 2025 at 08:57) - #28284 finite product of probability measures (1 message, latest: Aug 31 2025 at 20:41)
- #26790 define standard Bell number (2 messages, latest: Aug 31 2025 at 12:53)
- #28191 tag Injective, Surjective, and Bijective with fun_pro (21 messages, latest: Aug 29 2025 at 06:13)
- #26530, #26529, #26527 location of touchpoints of a simplex (6 messages, latest: Aug 28 2025 at 21:33)
- #29065: make Coverage and Pretopology extend Precoverage (2 messages, latest: Aug 28 2025 at 17:31)
- #29060 refactored: move argument s to last in LSeries_congr (2 messages, latest: Aug 28 2025 at 15:54)
- #28658 New
field_simp(23 messages, latest: Aug 28 2025 at 09:30) - #23594 chore: rename dmaSMul_apply to domSMul_apply (6 messages, latest: Aug 27 2025 at 14:59)
- #28818 Setoid.ker_lift (13 messages, latest: Aug 26 2025 at 07:44)
- #24050 generalise pointwise scalar multiplication of finsupp (1 message, latest: Aug 23 2025 at 15:44)
- #26838 lemmas about
List.scanr(1 message, latest: Aug 23 2025 at 15:38) - #28451 & #28477 Using Oka predicates (2 messages, latest: Aug 22 2025 at 20:55)
- #28710 MulEquivClass := MulHomClass (10 messages, latest: Aug 22 2025 at 00:32)
- #26766 some additions related to IsBounded (2 messages, latest: Aug 21 2025 at 15:31)
- #28661 doc(MeasureTheory): Miscellaneous typo fixes (1 message, latest: Aug 21 2025 at 07:56)
- #28322 chore: remove a now-unneeded maxHeartbeats (2 messages, latest: Aug 21 2025 at 02:26)
- #26804 ZFSet is a model of ZFC (9 messages, latest: Aug 20 2025 at 02:20)
- #27321 Colimit can be computed fiberwise (2 messages, latest: Aug 19 2025 at 13:35)
- #28180 clean up PiFin.mkLiteralQ (1 message, latest: Aug 19 2025 at 11:30)
- #28317 more lemmas about units in ordered monoid (1 message, latest: Aug 19 2025 at 11:20)
- #27562 Deduplicate some meta code (1 message, latest: Aug 18 2025 at 12:15)
- #28148 Simproc for Matrix Transpose (250 messages, latest: Aug 18 2025 at 04:20)
card_Union_le_sum_cardlemmas (7 messages, latest: Aug 16 2025 at 23:20)- #28498 Use the delta deriving handler (2 messages, latest: Aug 16 2025 at 07:02)
- #28169 Monoid of ideals of a Dedekind domain is torsion-free (20 messages, latest: Aug 14 2025 at 19:52)
- #19872 rename relindex to relIndex (15 messages, latest: Aug 13 2025 at 13:52)
- #9915 norm_num for division in NNRat and NNReal (5 messages, latest: Aug 13 2025 at 07:59)
- #28072 tactic for equivalent valuations (79 messages, latest: Aug 12 2025 at 21:01)
- #27552 TypeVec.Arrow over varying universes (1 message, latest: Aug 11 2025 at 19:45)
- #27200 oka condition (1 message, latest: Aug 08 2025 at 13:27)
- Three small PR's to add Finsupp lemmas (2 messages, latest: Aug 05 2025 at 10:51)
- #27852 add Teichmuller-Tukey lemma (2 messages, latest: Aug 02 2025 at 08:51)
- #27076 don't require
DecidablePredto statePrimrecPred(2 messages, latest: Aug 02 2025 at 00:10) - #25730 feat(ZLattice/Covolume): add covolume_div_covolume_eq (1 message, latest: Aug 01 2025 at 01:17)
- #26928 lower set in well-order is open (1 message, latest: Jul 30 2025 at 21:53)
- PRs from FLT (2 messages, latest: Jul 29 2025 at 15:57)
- Filtered Algebra (11 messages, latest: Jul 28 2025 at 19:38)
- Catching typos: a continuous thread (6 messages, latest: Jul 27 2025 at 14:49)
- #27270 Turn
WithLpinto a one field structure (1 message, latest: Jul 26 2025 at 19:19) - #24311 replace Monoid.IsTorsionFree with IsMulTorsionFree (1 message, latest: Jul 26 2025 at 06:05)
- Using enorm more in mathlib (9 messages, latest: Jul 25 2025 at 08:18)
- Refactoring to use ValuativeRel instead of Valued (134 messages, latest: Jul 24 2025 at 20:46)
- #27254 2025 IMO Problem 3 (1 message, latest: Jul 24 2025 at 16:09)
- #27292 Asymptotic cone of a set (5 messages, latest: Jul 20 2025 at 20:02)
- #27215 site on CommRingCatᵒᵖ (1 message, latest: Jul 19 2025 at 11:48)
- #26290 Define Stirling Numbers (10 messages, latest: Jul 19 2025 at 08:24)
- Riemannian manifolds (58 messages, latest: Jul 18 2025 at 20:31)
- #25833 topologist's sine curve (3 messages, latest: Jul 18 2025 at 17:54)
- #26659 algebraize tactic fix & feats (4 messages, latest: Jul 18 2025 at 10:41)
- #24351 Derivatives of powers (3 messages, latest: Jul 18 2025 at 08:37)
- #26070 instances on Dedekind domains (1 message, latest: Jul 15 2025 at 10:36)
- ✔ #26976 Concept lattice renames (95 messages, latest: Jul 11 2025 at 20:37)
- #26923 The pointwise ergodic theorem (Birkhoff's) (11 messages, latest: Jul 11 2025 at 17:46)
- #25961 Improve SetLike ruleset (1 message, latest: Jul 08 2025 at 19:04)
- #22782 Etale space (2 messages, latest: Jul 08 2025 at 16:11)
- multicoequalizers in Type (6 messages, latest: Jul 07 2025 at 12:43)
- #24131 - Primitive subgroups of the permutation group (16 messages, latest: Jul 07 2025 at 07:42)
- Fix broken links in docs #8785 (1 message, latest: Jul 05 2025 at 20:06)
- #26770 Multigraph Subgraph relation (1 message, latest: Jul 04 2025 at 21:57)
- #26718 commandStart linter and
:(3 messages, latest: Jul 04 2025 at 11:05) - #26170 Add an equivalence for Equiv.symm. (1 message, latest: Jul 03 2025 at 12:51)
- #26220 Remove Equiv explict FunLike instance. (2 messages, latest: Jul 03 2025 at 12:49)
- #25304 Joint differentiability from partial derivatives (12 messages, latest: Jul 01 2025 at 17:20)
- ✔ #26400 pigeonhole-like results for Fin (2 messages, latest: Jul 01 2025 at 12:26)
- von Neumann hierarchy: #26543 , #26518 (59 messages, latest: Jun 30 2025 at 21:36)
- #17027 , #26518 von Neumann hierarchy (1 message, latest: Jun 30 2025 at 14:48)
- #23986 (2 messages, latest: Jun 30 2025 at 06:56)
- #26392 maintainer-merge (12 messages, latest: Jun 30 2025 at 02:27)
- #26427 any cyclotomic extension is abelian (2 messages, latest: Jun 29 2025 at 06:10)
- #7300 synthetic geometry (61 messages, latest: Jun 28 2025 at 09:24)
- #26436 - Fuel Nat.minFac (12 messages, latest: Jun 28 2025 at 05:24)
- #22018 (2 messages, latest: Jun 26 2025 at 20:20)
- #25935 incenter, touchpoints and tangency (1 message, latest: Jun 25 2025 at 22:59)
- #26408 Equivalence between Nat and Nat + its first n element (1 message, latest: Jun 25 2025 at 15:58)
- #26285 Resultant of two polynomials (72 messages, latest: Jun 25 2025 at 13:31)
- #26277 - Basic isomorphism theorems for ring congruences (3 messages, latest: Jun 25 2025 at 08:31)
- #25491 Freer Monad (4 messages, latest: Jun 24 2025 at 17:14)
- #26297 (2 messages, latest: Jun 24 2025 at 16:36)
- #26060 Grassmannians (6 messages, latest: Jun 24 2025 at 12:31)
- #18629 runtime complexity of sorting a list (35 messages, latest: Jun 23 2025 at 14:32)
- #21560 Definition of sublocales (11 messages, latest: Jun 23 2025 at 12:46)
- #26203 IsPrime.one_notMem (1 message, latest: Jun 22 2025 at 23:54)
- #26061 define Projective Space (4 messages, latest: Jun 21 2025 at 19:39)
- #25728 PIR => Krull dim LE one without domain condition (1 message, latest: Jun 21 2025 at 07:26)
- Hausdorff–Alexandroff theorem (11 messages, latest: Jun 20 2025 at 07:37)
- Test for emoji reactions #25950 (2 messages, latest: Jun 18 2025 at 23:27)
- #24578 cardinality of product set (+54/-16) (1 message, latest: Jun 18 2025 at 18:51)
- #23678 recursor for nonempty lists (1 message, latest: Jun 17 2025 at 19:37)
- #23926 & #24336 finsum_mem lemmas (5 messages, latest: Jun 16 2025 at 15:48)
- #25168 LinearOrder on HahnSeries (4 messages, latest: Jun 13 2025 at 18:18)
- #24931
(n + 1).sqrtis not greater thann(19 messages, latest: Jun 12 2025 at 16:32) - #23752 incenters and excenters (3 messages, latest: Jun 12 2025 at 11:48)
- #20676 unbundling ordered algebra (111 messages, latest: Jun 12 2025 at 04:40)
- Mysterious CI error in "verify that everything was availa… (3 messages, latest: Jun 10 2025 at 19:34)
- #22834 lifting properties and parametrized adjunctions (1 message, latest: Jun 10 2025 at 05:56)
- #25253 add AlgHom.natCard_of_splits (2 messages, latest: Jun 09 2025 at 21:38)
- #25558 split Mathlib/Topology/Algebra/RestrictedProduct (11 messages, latest: Jun 07 2025 at 22:20)
- #24982 refactor definition of mates (1 message, latest: Jun 07 2025 at 09:58)
- #24540 various quiver shapes (5 messages, latest: Jun 06 2025 at 22:58)
- #23969 feat: add LinearEquiv.ofInjectiveOfFinrankEq (1 message, latest: Jun 06 2025 at 07:48)
- #25449 maintainer merge emoji reaction (1 message, latest: Jun 04 2025 at 19:07)
- #25050 - Adding
VectorandList.Vectorequivalence (17 messages, latest: Jun 04 2025 at 13:55) - #25264 Fairly elementary monoid lifts. (5 messages, latest: Jun 04 2025 at 12:41)
- #24735: define tensorLeft/Right as abbrev for curriedTensor (3 messages, latest: Jun 03 2025 at 16:25)
- #24669 Defining
LinearIsometryEquivfor commuting products (1 message, latest: Jun 02 2025 at 06:29) - #24792 Matrix.vec (2 messages, latest: Jun 02 2025 at 00:36)
- #25218 Tate normal form of elliptic curves (1 message, latest: Jun 01 2025 at 13:04)
- #14752 - Repair the topology of valued fields (8 messages, latest: Jun 01 2025 at 11:24)
- #25087 algebra isomorphisms induced by Weierstrass division (1 message, latest: Jun 01 2025 at 07:40)
- #24303 Reassoc for isomorphisms (2 messages, latest: May 27 2025 at 17:31)
- Boring linear algebra results: #25166, #25169, #25142 (1 message, latest: May 25 2025 at 12:16)
- #24690 Reverse lexicographic order (4 messages, latest: May 24 2025 at 14:44)
- #22653 Bors failure (2 messages, latest: May 24 2025 at 08:09)
- lean-pr-testing-7352 (3 messages, latest: May 21 2025 at 23:26)
- #24295
AffineSubspace.subtypeA(2 messages, latest: May 21 2025 at 19:16) - #24991 Day convolution of functors (9 messages, latest: May 19 2025 at 04:43)
- #24960 PermOf implements more-efficient finite permutations. (2 messages, latest: May 16 2025 at 14:58)
- #23974 Change file name to CamelCase (28 messages, latest: May 16 2025 at 12:57)
- #22884 Turing Degrees (1 message, latest: May 15 2025 at 15:03)
- #24122 Multigraphs (45 messages, latest: May 14 2025 at 18:54)
- #24149 reorder, streamline convex cones (17 messages, latest: May 14 2025 at 11:47)
- #24897 replicate the Algebra subfolders design in Order (1 message, latest: May 14 2025 at 10:41)
- #23507 SummableUniformlyOn (4 messages, latest: May 13 2025 at 13:53)
- #24660 Use Classical or Decidable in definition (74 messages, latest: May 12 2025 at 15:14)
- #22957 row and column functions of matrices (12 messages, latest: May 10 2025 at 15:27)
- #24321 + #24667: adjoint triples & quadruples (9 messages, latest: May 09 2025 at 23:54)
- #24719 cannot find home (4 messages, latest: May 09 2025 at 15:54)
- #24556 Testing the new emojibot label (26 messages, latest: May 08 2025 at 13:27)
- Add "closed-pr" emoji in Zulip? (42 messages, latest: May 07 2025 at 09:21)
- Local diffeomorphism PRs (3 messages, latest: May 06 2025 at 15:14)
- #24452 + #24454 + #24506:
rotate_isostactic (13 messages, latest: May 06 2025 at 13:55) - #23951 matroid rank API (2 messages, latest: May 05 2025 at 07:03)
- #24178 Which order to sort eigenvalues? (9 messages, latest: May 03 2025 at 17:26)
- #24127 PR not on the review queue (11 messages, latest: May 02 2025 at 21:39)
- #24465 maintainer merged PRs (7 messages, latest: May 02 2025 at 14:35)
- #24538
homOfEqlemmas (3 messages, latest: May 02 2025 at 11:55) - #22337 type class generalization (104 messages, latest: Apr 30 2025 at 12:37)
- #22196
lie_ringtactic (12 messages, latest: Apr 30 2025 at 06:52) - #24441 theorem on list commutativity (1 message, latest: Apr 28 2025 at 18:58)
- #22361 NFA closure properties (5 messages, latest: Apr 27 2025 at 13:22)
- #24369 modify the class IsQuadraticExtension (1 message, latest: Apr 25 2025 at 15:37)
- #23715 make
orthogonalProjectiona continuous affine map (4 messages, latest: Apr 23 2025 at 17:59) - #20230 categories of homological complexes are Grothendieck (2 messages, latest: Apr 23 2025 at 15:24)
- #22574 redefine full subcategories using ObjectProperty (3 messages, latest: Apr 23 2025 at 10:32)
- #22355 Some lemmas about
RingQuot.mkRingHom(22 messages, latest: Apr 23 2025 at 06:19) - #19668 define
≤/<onWithBot/WithTopby induction (12 messages, latest: Apr 18 2025 at 23:13) - #24182 Remove IntermediateField.instCoeOutSubtypeMem (1 message, latest: Apr 18 2025 at 20:01)
- #19920 More differential geometry documentation (7 messages, latest: Apr 18 2025 at 19:12)
- #24139 Fin.cycleIcc (4 messages, latest: Apr 17 2025 at 14:07)
- #24125 clean up
WithVal(1 message, latest: Apr 16 2025 at 19:27) - #22929 characterise covering in Pi types (1 message, latest: Apr 16 2025 at 19:16)
- equivalence of stabilizers (2 messages, latest: Apr 16 2025 at 07:44)
- ✔ #17980 Functoriality of the Grothendieck construction (11 messages, latest: Apr 15 2025 at 18:39)
- #23637 Circuit contains a cycle (1 message, latest: Apr 15 2025 at 13:29)
- #23503 ENat and tsum (105 messages, latest: Apr 13 2025 at 16:22)
- Categorical structure of Quiv (5 messages, latest: Apr 13 2025 at 08:58)
- SubMulAction (3 messages, latest: Apr 12 2025 at 11:20)
- #23948 - Eisenstein Criterion (1 message, latest: Apr 11 2025 at 15:08)
- #23946 edge sets of walks (1 message, latest: Apr 11 2025 at 11:31)
- Thread for failed staging PRs (43 messages, latest: Apr 11 2025 at 02:35)
- #23866 and #23867, removing most
\[Nat.AtLeastTwo n\](71 messages, latest: Apr 11 2025 at 02:16) - #23065
eval_of_algHom(1 message, latest: Apr 10 2025 at 14:08) - #23124 nets (1 message, latest: Apr 10 2025 at 13:21)
- #18396 the Lie algebra of a real or complex Lie group (53 messages, latest: Apr 10 2025 at 08:32)
- #23892 Drop
ZeroLeOneClassassumption in some lemmas (4 messages, latest: Apr 10 2025 at 08:16) - #23884 Loopless matroids (1 message, latest: Apr 09 2025 at 17:47)
- #23873 Minors of matroids (1 message, latest: Apr 09 2025 at 16:14)
- #21903 FreeSemigroup and List with relative theorems (4 messages, latest: Apr 08 2025 at 07:55)
- #23798 strict inclusion of unbounded intervals (1 message, latest: Apr 08 2025 at 04:44)
- #22314 leftmost derivations for context-free grammars (3 messages, latest: Apr 07 2025 at 07:17)
- #21603 Basic ChosenFiniteCoproducts class (3 messages, latest: Apr 07 2025 at 05:54)
- #20681 define deleteIncidenceSet (Combinatorics/SimpleGraph) (3 messages, latest: Apr 07 2025 at 01:55)
- #20495 Combinatorial Nullstellensatz (3 messages, latest: Apr 07 2025 at 01:53)
- #23710 - A generalized Eisenstein criterion (2 messages, latest: Apr 07 2025 at 01:52)
- #21488 Premonoidal categories (4 messages, latest: Apr 07 2025 at 01:51)
- #20680 weak factorisation systems (2 messages, latest: Apr 05 2025 at 22:04)
- #23645 (1 message, latest: Apr 05 2025 at 01:36)
- #22127 Module length is additive in short exact sequences (5 messages, latest: Apr 04 2025 at 14:38)
- #23557 matroid contraction (3 messages, latest: Apr 04 2025 at 11:19)
- ✔ #11521 speeding up lots of instances (108 messages, latest: Apr 03 2025 at 16:40)
- #21238 lake exe cache (12 messages, latest: Apr 02 2025 at 10:04)
- #21080 continuous functions on profinites (4 messages, latest: Apr 02 2025 at 09:54)
- #22503 Rewriting Multiplicity in Factorization (3 messages, latest: Apr 02 2025 at 06:56)
- #18397 rename RestrictGenTopology to IsRestrictGen (15 messages, latest: Mar 31 2025 at 13:56)
- #23086 lemmas about
periodicPtsonFintype(2 messages, latest: Mar 31 2025 at 08:49) - #23454 ENat lemmas about
mul/iInf/iSup(1 message, latest: Mar 30 2025 at 17:01) - Frobenius map now in
Mathlib.Algebra.CharP.Frobenius(1 message, latest: Mar 29 2025 at 18:44) - Rings with multiplicative norm (8 messages, latest: Mar 29 2025 at 01:23)
- #23377 Matroid ENat-valued rank (5 messages, latest: Mar 27 2025 at 18:27)
- #23373 Matroid coloops (1 message, latest: Mar 27 2025 at 15:18)
- #23209 add improper integral of complex exp (2 messages, latest: Mar 27 2025 at 15:10)
- #21944 Weierstrass preparation for complete local ring (32 messages, latest: Mar 27 2025 at 07:03)
- #22964 Sum.elim lemmas in Data/Set/Image (3 messages, latest: Mar 26 2025 at 17:49)
- Rewriting Python style linters in Lean (46 messages, latest: Mar 25 2025 at 21:31)
- Ackermann function is computable #22457 (5 messages, latest: Mar 25 2025 at 05:21)
- #23276 Matroid minors (1 message, latest: Mar 24 2025 at 19:28)
- #23196 docstrings for Nat.factorial and Nat.choose (1 message, latest: Mar 21 2025 at 15:53)
- #23150 Matrix row/column rename (1 message, latest: Mar 20 2025 at 23:51)
- #23157 matroid nonloops (1 message, latest: Mar 20 2025 at 17:30)
- #22253 set difference lemmas (1 message, latest: Mar 20 2025 at 15:36)
- #22533 deprime induction' in root files (8 messages, latest: Mar 19 2025 at 02:52)
- #22365 hint tactics (27 messages, latest: Mar 18 2025 at 16:35)
- #23053, merging admit linter into deprecated syntax linter (1 message, latest: Mar 18 2025 at 16:32)
- Eliminating cases' (for real) (17 messages, latest: Mar 17 2025 at 23:45)
- #22226 Infinite matrix rank (29 messages, latest: Mar 17 2025 at 16:25)
- #22366
check_equalitiestactic for defeq problems (5 messages, latest: Mar 17 2025 at 03:06) - #22976 Refactoring
CategoryTheory.Sums(3 messages, latest: Mar 17 2025 at 02:58) - #22631 define associated graded structure for abelian group (2 messages, latest: Mar 16 2025 at 02:44)
- #22948 Definition about morphism of directsum decomposition (9 messages, latest: Mar 16 2025 at 01:39)
- #22614 CanonAtomM (23 messages, latest: Mar 15 2025 at 14:45)
- #22587 chore(Algebra/Group/Basic): rename mul_right_eq_self (3 messages, latest: Mar 14 2025 at 07:06)
- #22892 hint looks for error messages (3 messages, latest: Mar 14 2025 at 00:14)
- #21090 refactor(AlgebraicTopology): use the Subpresheaf API (5 messages, latest: Mar 13 2025 at 10:11)
- PR #22018 localization of a finite direct product (1 message, latest: Mar 12 2025 at 13:52)
- #22851 More LinearIndepOn (4 messages, latest: Mar 12 2025 at 13:26)
- #20488 various lemmas about lists (8 messages, latest: Mar 11 2025 at 09:14)
- #22312 Intrinsic Interior, Closure, and Related Properties (33 messages, latest: Mar 11 2025 at 07:53)
- #21078 WeakBilin eval map (4 messages, latest: Mar 10 2025 at 23:20)
- #21585 lemmas about nonterminals (3 messages, latest: Mar 10 2025 at 23:20)
- #22780 scoping a few instances with weak keys (14 messages, latest: Mar 10 2025 at 20:42)
- lean4#7356 monadic theorems about mapM, foldM, etc (1 message, latest: Mar 10 2025 at 08:42)
- "Add closed-pr emoji in Zulip" failed (32 messages, latest: Mar 09 2025 at 19:30)
- #22678 - bilinearCombination (1 message, latest: Mar 07 2025 at 10:56)
- #22527 ofSetSetoid (1 message, latest: Mar 07 2025 at 09:41)
- #22377 Vandermonde matrices with exceptional rows (16 messages, latest: Mar 05 2025 at 18:45)
- #22230 chore(Algebra/Group):add coercion for subgroup class (1 message, latest: Mar 03 2025 at 07:36)
- #11968 improvements to RefinedDiscrTree (11 messages, latest: Mar 01 2025 at 00:39)
- #21571 normalized trace (1 message, latest: Feb 28 2025 at 23:25)
- #11563 ∑ i ∈ s with hi : p i, f i hi syntax (3 messages, latest: Feb 28 2025 at 13:28)
- #21442 define open covers (6 messages, latest: Feb 28 2025 at 12:57)
- #21341 quotients of multiplicative normed groups (1 message, latest: Feb 28 2025 at 11:46)
- #22368 more linearIndepOn api (2 messages, latest: Feb 27 2025 at 16:26)
- #20744 the minimum cardinality of generating set (17 messages, latest: Feb 26 2025 at 10:14)
- #20688 truncated simplicial notations (3 messages, latest: Feb 24 2025 at 18:42)
- #22208 feat(Algebra):filtered ring hom (1 message, latest: Feb 24 2025 at 10:15)
- #16733 Nonarchimedean locally compact iff complete and DVR (1 message, latest: Feb 24 2025 at 03:12)
- #22105 Discrete spaces are 0-dimensional manifolds (4 messages, latest: Feb 23 2025 at 21:08)
- #22225 move
Polynomial.coeffs(1 message, latest: Feb 23 2025 at 20:33) - #21886 LinearIndepOn refactor (14 messages, latest: Feb 23 2025 at 17:30)
- #22186 some
encardlemmas (1 message, latest: Feb 22 2025 at 18:24) - #22097 dot notation for disjointness (1 message, latest: Feb 19 2025 at 19:02)
- #12259 more
apply(26 messages, latest: Feb 19 2025 at 02:58) - #22045 Matroid loops (1 message, latest: Feb 18 2025 at 16:32)
- #22031 maybe adds emoji to first message (4 messages, latest: Feb 18 2025 at 09:10)
- #21995 deprecate
Complex.abs(7 messages, latest: Feb 18 2025 at 07:20) - #19580 incomparable relation (1 message, latest: Feb 18 2025 at 05:38)
- #20502 generalize IsLUB.mem_of_not_isSuccPrelimit (15 messages, latest: Feb 17 2025 at 09:16)
- #18547 ordinals are uncountable (1 message, latest: Feb 17 2025 at 06:22)
- simplify lakefile post_update hook #21650 (1 message, latest: Feb 16 2025 at 22:14)
- #21768 deprime induction'/cases' in Topology (7 messages, latest: Feb 15 2025 at 12:53)
- #20686 CompletableTopField instance for NormedField (21 messages, latest: Feb 15 2025 at 10:46)
- #21021 Chevalley’s theorem (1 message, latest: Feb 14 2025 at 21:45)
- #21879 Add 'Is' to matroid predicate names (1 message, latest: Feb 14 2025 at 17:07)
- #21799 LinearIndependentOn (1 message, latest: Feb 13 2025 at 11:50)
- #21772 clearing (some of)
docBlame(2 messages, latest: Feb 12 2025 at 07:08) - #21741 -> #21748: presentation of
SimplexCategory(1 message, latest: Feb 11 2025 at 21:53) - feat: erw?, a tool to explain why erw is necessary #21643 (14 messages, latest: Feb 11 2025 at 16:28)
- #21694 Finite-rank sets in matroids (1 message, latest: Feb 10 2025 at 23:36)
- #21692 Matroid cocircuits (1 message, latest: Feb 10 2025 at 23:33)
- #20642 extend API for WithAbs (1 message, latest: Feb 10 2025 at 20:08)
- #17129 add unicode linter for unicode variant-selectors (5 messages, latest: Feb 10 2025 at 10:22)
- #20988 multiequalizer refactor (category theory) (1 message, latest: Feb 10 2025 at 09:19)
- #21582 More APIs for IsAdicComplete (5 messages, latest: Feb 10 2025 at 03:39)
- #21563 the untilt map (1 message, latest: Feb 09 2025 at 17:40)
- #21180 IndepMatroid docstring (1 message, latest: Feb 09 2025 at 17:06)
- #21605 Rk -> Rank in instance names (3 messages, latest: Feb 09 2025 at 16:45)
- #17908 Hopkins–Levitzki theorem (18 messages, latest: Feb 08 2025 at 17:53)
- #21525 Locally Cartesian Closed Categories (7 messages, latest: Feb 07 2025 at 14:28)
- #21372 Exponent for (purely inseparable) field extensions (6 messages, latest: Feb 07 2025 at 08:54)
- #21527 add reassoc tag to
terminal.comp_from(1 message, latest: Feb 07 2025 at 02:17) - #21520 Linear independence and sets of indices (1 message, latest: Feb 06 2025 at 19:25)
- #21296 don't import Ring in GroupTheory.Commutator.Basic (37 messages, latest: Feb 06 2025 at 16:55)
- #21454 Protect some results about
Complex.abs(11 messages, latest: Feb 06 2025 at 16:52) - #21511 Trivial linear independence lemmas (1 message, latest: Feb 06 2025 at 16:48)
- #21097 SetLike instance for equivalence classes (35 messages, latest: Feb 06 2025 at 15:39)
- #21428 Set partitions (6 messages, latest: Feb 05 2025 at 21:22)
- #21172 Circuit elimination and finitary matroids (2 messages, latest: Feb 05 2025 at 14:08)
- #21322 insertion and iUnion (2 messages, latest: Feb 04 2025 at 14:35)
- #17930 introduce Ideal.IsTwoSided class (11 messages, latest: Feb 04 2025 at 08:32)
- #17580 lint declarations which contain a double underscore (17 messages, latest: Feb 04 2025 at 00:38)
- #21383 iff versions of scaling and linear independence (1 message, latest: Feb 03 2025 at 22:28)
- #21357
check_compositions(8 messages, latest: Feb 03 2025 at 10:26) - #20225 - tidy various files (4 messages, latest: Feb 02 2025 at 20:44)
- #21168
IsLocalRingfor sub(semi)rings (3 messages, latest: Jan 31 2025 at 20:45) - ✔ #21199
IsUnit x ↔ x ∈ A⁰in algebras over artinian rings (3 messages, latest: Jan 31 2025 at 19:11) - #20748 don't import MonoidWithZero in submonoids (10 messages, latest: Jan 31 2025 at 12:16)
- #19946 ZFC order instances (4 messages, latest: Jan 31 2025 at 01:36)
- Open PR on group theory (14 messages, latest: Jan 30 2025 at 13:22)
- #21240 Fixed junk values for fundamental circuits. (6 messages, latest: Jan 30 2025 at 13:12)
- #20658 define SubgraphIso (8 messages, latest: Jan 29 2025 at 19:56)
- ✔ #21191
IsIntegraland (cartesian) product (3 messages, latest: Jan 29 2025 at 12:50) - #21005 style PR on Games (5 messages, latest: Jan 29 2025 at 07:45)
- ✔ #21062
Polynomial.aevalfor product algebras (5 messages, latest: Jan 28 2025 at 12:06) - lean4#6269 warnings for declaration/
exportconflicts (20 messages, latest: Jan 28 2025 at 10:38) - #21099 use unification hints for generators (36 messages, latest: Jan 28 2025 at 00:59)
- #21145 (1 message, latest: Jan 27 2025 at 21:31)
- #19571 AntisymmRel lemmas (3 messages, latest: Jan 27 2025 at 01:06)
- #16936 equidecomposition (7 messages, latest: Jan 26 2025 at 23:45)
- ✔ #21019 artinian local reduced ring is a field (6 messages, latest: Jan 25 2025 at 21:01)
- #20182 Distributive Categories (6 messages, latest: Jan 25 2025 at 09:56)
- #20885 Matroid closure lemmas (2 messages, latest: Jan 25 2025 at 06:15)
- #16991 ContinuousMulEquiv (11 messages, latest: Jan 24 2025 at 21:55)
- #20745 don't import MonoidWithZero for results about MonoidH (7 messages, latest: Jan 24 2025 at 16:20)
- #20538 still maintainer-merge (1 message, latest: Jan 23 2025 at 23:09)
- #20721
Equivs involvingcenterandModule.End(1 message, latest: Jan 23 2025 at 18:08) - #20886 Instances for basic matroids (1 message, latest: Jan 23 2025 at 17:53)
- Truncation of (multivariate) power series (7 messages, latest: Jan 23 2025 at 16:54)
- #20995 Matroid circuits (1 message, latest: Jan 23 2025 at 16:49)
- #20977: more on additive contents (4 messages, latest: Jan 23 2025 at 11:53)
- #7162 refactor: separate out PGame.relabelling (26 messages, latest: Jan 23 2025 at 09:58)
- #16993 Galois Group is Profinite (14 messages, latest: Jan 23 2025 at 05:40)
- #19393 Up and down games (6 messages, latest: Jan 23 2025 at 04:37)
- Azumaya algebras #20489 (6 messages, latest: Jan 22 2025 at 07:03)
- #20828
MaximalSpectrum Rinstead of{I \| I.IsMaximal}(45 messages, latest: Jan 21 2025 at 18:05) - #20921 Cardinality-valued matroid rank (1 message, latest: Jan 21 2025 at 17:34)
- #17325 feat(Data/Nat): faster computation of Nat.log (2 messages, latest: Jan 21 2025 at 15:17)
- #20888 Finitary matroid bases are equicardinal (1 message, latest: Jan 21 2025 at 01:10)
- #10186 Defining Greedoid (5 messages, latest: Jan 21 2025 at 01:07)
- #19838 #20876 #20877 Matroid housekeeping (5 messages, latest: Jan 20 2025 at 16:50)
- ✔ #5901 feat: more PGame.identical PGame.memₗ PGame.memᵣ … (2 messages, latest: Jan 20 2025 at 04:59)
- #14990 Linear topologies (3 messages, latest: Jan 17 2025 at 10:17)
- #16992 Profinite Group is limit of finite groups (12 messages, latest: Jan 17 2025 at 09:32)
- #20794
RingEquiv.piUnique(3 messages, latest: Jan 17 2025 at 08:59) - #20772 split off definition of ring spectra (3 messages, latest: Jan 16 2025 at 10:18)
- #20488 setOf_mem_list_eq_singleton_of_nodup (7 messages, latest: Jan 16 2025 at 00:20)
- #20491 generalize
SuccOrdertheorems (1 message, latest: Jan 16 2025 at 00:19) - #19973
¬a < b ↔ ¬a ≤ b ∨ b ≤ a(1 message, latest: Jan 15 2025 at 23:46) - #19115 Generalize flatness to semirings (6 messages, latest: Jan 15 2025 at 14:49)
- #19802 deprecate
Ordinal.IsLimit(1 message, latest: Jan 14 2025 at 15:13) - #17538 automatically add dependency-bump (2 messages, latest: Jan 13 2025 at 14:13)
- #15891 Boundary points of a real interval (6 messages, latest: Jan 12 2025 at 22:45)
- #17522 feat: study the centralizer of a permutation (3 messages, latest: Jan 12 2025 at 16:17)
- Maximal subgroups #20499 (12 messages, latest: Jan 10 2025 at 15:01)
- #19514 Congruence between subtypes and sets/finsets (13 messages, latest: Jan 08 2025 at 05:16)
- #18818 Traversable Tree instance (1 message, latest: Jan 07 2025 at 09:55)
- #16797 Liouville / differential field theory (7 messages, latest: Jan 06 2025 at 11:20)
- #19970 ⨆ a < x, succ a = x (1 message, latest: Jan 04 2025 at 20:59)
- #20282 feat(Topology/Group): Lemmas about profinite group (1 message, latest: Jan 04 2025 at 15:50)
- #20364 fix NatTrans.CommShift (1 message, latest: Jan 03 2025 at 09:52)
- #18461 left and right common multiples mixins (9 messages, latest: Jan 03 2025 at 06:33)
- #20371 sort_antisymmetry and sort_embedding (11 messages, latest: Jan 03 2025 at 05:14)
- L-series (81 messages, latest: Dec 31 2024 at 21:49)
- #20330 (3 messages, latest: Dec 30 2024 at 21:50)
- #20331: rename Nat.lt_div_iff_mul_lt (1 message, latest: Dec 29 2024 at 20:44)
- #20136 rename iteratedDeriv_const_{smul,mul} (1 message, latest: Dec 28 2024 at 10:07)
- ✔ metaprobook needs update!! (2 messages, latest: Dec 25 2024 at 10:46)
- #19163 bounding the coefficients of modByMonic/divByMonic (2 messages, latest: Dec 19 2024 at 10:57)
- #17554 -> #17779 + #17781: sifted categories (RFC!) (10 messages, latest: Dec 19 2024 at 10:55)
- #17758 Ordinal.toENat (57 messages, latest: Dec 16 2024 at 01:12)
- #16688 Fix two PATH resolution issues (3 messages, latest: Dec 15 2024 at 22:11)
- #19977 ChosenFiniteProducts for affine schemes (2 messages, latest: Dec 15 2024 at 17:20)
- #16769 add Walk.penultimate and Walk.snd (1 message, latest: Dec 13 2024 at 13:31)
- #19237: address porting notes (1 message, latest: Dec 12 2024 at 14:41)
- #18778: omega ordinals are principal (1 message, latest: Dec 12 2024 at 14:37)
- #16865: Laurent series are complete (31 messages, latest: Dec 12 2024 at 05:58)
- #16344 induction principle for FreeProduct (22 messages, latest: Dec 12 2024 at 04:07)
- #19757 Algebra/Category/Ring: make morphisms a structure (3 messages, latest: Dec 11 2024 at 22:18)
- #19755 test an executable with import Mathlib (2 messages, latest: Dec 11 2024 at 14:04)
- #14987 Relative rank of intermediate fields (32 messages, latest: Dec 08 2024 at 07:23)
- ✔ #12405 (8 messages, latest: Dec 04 2024 at 20:57)
- Integrate analytic functions in the smooth hierarchy (75 messages, latest: Dec 04 2024 at 06:28)
- #19042 localization of a direct product injects (2 messages, latest: Dec 03 2024 at 22:39)
- #18689 feat(Topology): Introduce HomeomorphClass (2 messages, latest: Dec 03 2024 at 08:55)
- #18611 Veblen hierarchy (3 messages, latest: Dec 03 2024 at 07:14)
- #19068 Dini's theorem (1 message, latest: Dec 02 2024 at 10:37)
- #19435 an equality condition for AM-GM inequality (9 messages, latest: Nov 30 2024 at 13:31)
- #19522: emoji reactions to all public channels (128 messages, latest: Nov 30 2024 at 08:41)
- #18239 cleanup of ZFC rank (3 messages, latest: Nov 27 2024 at 22:25)
- #18990 sup-closed sets are closed under finite suprema (5 messages, latest: Nov 27 2024 at 22:20)
- #19060
IsSuccLimittheorems forSuccAddOrder(2 messages, latest: Nov 27 2024 at 19:30) - #19236 natural addition without
blsub(2 messages, latest: Nov 27 2024 at 19:28) - #19425: gcongr forward-reasoning (1 message, latest: Nov 27 2024 at 17:34)
- Prerequisites for PNT and Dirichlet's Thm (71 messages, latest: Nov 27 2024 at 10:24)
- #17087 Add results about
EReal(4 messages, latest: Nov 27 2024 at 08:03) - Testing new emoji system using #18679 as a guinea PR (3 messages, latest: Nov 26 2024 at 00:40)
- #19447 change the definition of List.finRange (4 messages, latest: Nov 25 2024 at 06:09)
- #18235
typeLTnotation (20 messages, latest: Nov 23 2024 at 19:58) - #19181 cleanup of many set_option deprecated.linter false (2 messages, latest: Nov 23 2024 at 07:32)
- #19367 (5 messages, latest: Nov 22 2024 at 11:48)
HolomorphicOnandHolomorphicAt(30 messages, latest: Nov 21 2024 at 14:49)- #19119 atom representatives for ring and abel (18 messages, latest: Nov 18 2024 at 20:59)
- #19082 linear_combination error message (1 message, latest: Nov 18 2024 at 15:00)
- #18967 has incomplete deprecations (18 messages, latest: Nov 18 2024 at 09:36)
- #18463 type of fundamental sequences (1 message, latest: Nov 17 2024 at 07:38)
- #19080 Theorems about LocalizedModule (5 messages, latest: Nov 16 2024 at 09:40)
- ✔ #16877 Nimber multiplication (8 messages, latest: Nov 15 2024 at 01:48)
- #19042 Ring Theory (3 messages, latest: Nov 14 2024 at 20:11)
- #16311 regular languages are context-free (3 messages, latest: Nov 14 2024 at 10:06)
- #16792 lifting a derivation via an algebra homomorphism (7 messages, latest: Nov 13 2024 at 15:38)
- #18947 bump Mathlib for batteries#1029 (1 message, latest: Nov 13 2024 at 03:19)
- #16105 add Stacks Project tags in Chapter 09FA Fields (5 messages, latest: Nov 12 2024 at 05:53)
- #18043 deprecate
StrictOrder.cof(1 message, latest: Nov 12 2024 at 01:58) - #18667, #18823 Goursat's lemma (4 messages, latest: Nov 10 2024 at 20:21)
- #18032 quasi-compact + specializing <=> closed map (1 message, latest: Nov 10 2024 at 03:28)
- Orthogonality of Dirichlet characters (17 messages, latest: Nov 08 2024 at 21:23)
- #18065 periodic holomorphic functions (1 message, latest: Nov 08 2024 at 16:11)
- #18689 feat(Topology): Introduce HomeomorphClass (8 messages, latest: Nov 08 2024 at 13:15)
- Transcendental and algebraically independent (13 messages, latest: Nov 07 2024 at 08:32)
- #18709 select correct lean4checker version (1 message, latest: Nov 06 2024 at 23:43)
- #16991 feat(Topology/Group): Continuous isomorphism (3 messages, latest: Nov 06 2024 at 11:29)
- #14598 typeclasses for top/bot being additively absorbing… (7 messages, latest: Nov 05 2024 at 17:16)
- ✔ #18495 TU matrices (2 messages, latest: Nov 04 2024 at 16:00)
- #18255 Underlying space of pullback (3 messages, latest: Nov 04 2024 at 15:15)
- #18516: refactor roots of unity (6 messages, latest: Nov 04 2024 at 08:24)
- #18491 removes @[simp] from Sum.forall and Sum.exists (18 messages, latest: Nov 04 2024 at 07:25)
- #17549: Ring Theory (10 messages, latest: Oct 31 2024 at 19:12)
- #18335 Mahler basis functions (1 message, latest: Oct 31 2024 at 14:30)
- #16982 Fundamental Theorem of Infinite Galois Theory (13 messages, latest: Oct 31 2024 at 00:45)
- #17942 avoid Coe.coe in Data.Multiset.Functor (1 message, latest: Oct 30 2024 at 22:15)
- #17674 simpler definition of
Cardinal.aleph(2 messages, latest: Oct 30 2024 at 07:46) - #17751 generalize
nfpFamilyuniverses (3 messages, latest: Oct 30 2024 at 02:40) - #18346 Final iso between K⸨X⸩ and X-adic completion of K(X) (2 messages, latest: Oct 29 2024 at 16:07)
- #18034 finiteness tactic (3 messages, latest: Oct 28 2024 at 07:35)
- #17544 p-adic valuation of casts (1 message, latest: Oct 27 2024 at 14:35)
- #17037 trivialities about Nat.primeCounting and Finsets (2 messages, latest: Oct 27 2024 at 13:15)
- #17097 Measurability of add and mul on EReal (1 message, latest: Oct 27 2024 at 01:55)
- #17881 MultilinearMap operations for Pi and DFinsupp (1 message, latest: Oct 25 2024 at 17:56)
- #15793 Initial development of ordinals in ZFSet (3 messages, latest: Oct 25 2024 at 05:27)
- 18188 T2Space is Antitone: to golf or not to golf (3 messages, latest: Oct 24 2024 at 17:53)
- #17602 fix InitialSeg simp lemmas (2 messages, latest: Oct 24 2024 at 17:29)
- ✔ #17483 more lemmas on characteristic two (3 messages, latest: Oct 24 2024 at 17:28)
- ✔ #16586 WellFounded.rank → IsWellFounded.rank (2 messages, latest: Oct 23 2024 at 20:25)
- #18129 Spanning sets in matroids (1 message, latest: Oct 23 2024 at 15:30)
- !3#16586
push_negoption (1 message, latest: Oct 22 2024 at 11:06) - ✔ #17679 deprecate
blsub₂(2 messages, latest: Oct 22 2024 at 10:09) - #17960 API for separated morphisms (1 message, latest: Oct 22 2024 at 08:13)
- #15897 chore: use Batteries test driver (4 messages, latest: Oct 21 2024 at 22:22)
- #12339 the multi-goal linter (6 messages, latest: Oct 21 2024 at 01:30)
- #17444 make
CanonicallyOrdered*mixin (1 message, latest: Oct 19 2024 at 21:35) - #17945 Move infinite Galois (1 message, latest: Oct 19 2024 at 15:26)
- #17599 Ordinal.typein tweaks (1 message, latest: Oct 19 2024 at 05:11)
- #17901 reorganize ContinuousOn file (1 message, latest: Oct 18 2024 at 09:50)
- #17859 feat: consistent family of kernels (7 messages, latest: Oct 17 2024 at 15:22)
- #17276 feat(Algebra/Homology): study of the target of the… (1 message, latest: Oct 17 2024 at 13:55)
- #17867 some results on Transcendental (1 message, latest: Oct 17 2024 at 13:06)
- #16755 towards sheaf of differentials (1 message, latest: Oct 17 2024 at 09:42)
- Discrete condensed objects #14027 #15321 #15566 #15569 (18 messages, latest: Oct 17 2024 at 08:10)
- #15238 some results of extendScalars (6 messages, latest: Oct 17 2024 at 07:02)
- #16409 doc: fix some issues under RepresentationTheory (1 message, latest: Oct 17 2024 at 06:57)
- #14798 relations between trace maps and quotients (31 messages, latest: Oct 17 2024 at 06:39)
- #15240 morphisms from
Spec RforRlocal (3 messages, latest: Oct 16 2024 at 16:04) - #15093
Scheme.Homrefactor (1 message, latest: Oct 16 2024 at 07:53) - #16881 Multiplicity refactor (8 messages, latest: Oct 16 2024 at 06:55)
- #8885 – fast powering in code generation (2 messages, latest: Oct 15 2024 at 20:39)
- PRs from APAP (17 messages, latest: Oct 15 2024 at 16:25)
- #17431 further properties of j-invariants (2 messages, latest: Oct 15 2024 at 15:40)
- #17766 CartesianClosed refactor (1 message, latest: Oct 15 2024 at 11:00)
- #16041
Ordinal.toNat(8 messages, latest: Oct 15 2024 at 04:50) - ✔ #16283 rewrap and improve docs (2 messages, latest: Oct 15 2024 at 04:38)
- #16818 Basic API for List.GroupBy (3 messages, latest: Oct 15 2024 at 03:00)
- #17176 integrals/integrability with .re (7 messages, latest: Oct 14 2024 at 17:25)
- #17718 bump batteries (3 messages, latest: Oct 14 2024 at 07:28)
- #17348 unused arguments (1 message, latest: Oct 14 2024 at 05:07)
- #17223 use foldr in List.prod (1 message, latest: Oct 14 2024 at 04:56)
- #16159 error in PR (3 messages, latest: Oct 13 2024 at 20:07)
- #11156 basis and dual of PiTensorProduct (19 messages, latest: Oct 13 2024 at 19:40)
- #16392 chore: rename IsAlgClosure fields (2 messages, latest: Oct 12 2024 at 11:33)
- #15779 improve insertLeft / insertRight API (5 messages, latest: Oct 12 2024 at 07:01)
- #6045 refactor
IsLocalRingHom(23 messages, latest: Oct 09 2024 at 13:29) - #15947
prodandpiSetoidlemmas and equivs (2 messages, latest: Oct 09 2024 at 04:58) - #13740 More robust ae notation (2 messages, latest: Oct 06 2024 at 09:04)
- #17262 nonarchimedean property of Qp (3 messages, latest: Oct 04 2024 at 10:58)
- #17273 Lemmas on
Multiset(2 messages, latest: Oct 03 2024 at 17:18) - #16020: store
oleansizes (6 messages, latest: Oct 03 2024 at 13:56) - #16840 "ring" tactic variant handling inequalities (5 messages, latest: Oct 02 2024 at 16:04)
- #16735 Clean up sSup/sInf API for Real (1 message, latest: Oct 02 2024 at 13:07)
- #15743 Jacobi sums (14 messages, latest: Oct 01 2024 at 18:30)
- #15815 Generalise the rearrangement inequality (2 messages, latest: Oct 01 2024 at 13:11)
- #8013 Walking Reflexive Pair (4 messages, latest: Oct 01 2024 at 09:10)
- #15914 feat(Data/List/Sort): List.Sorted.cons (1 message, latest: Oct 01 2024 at 09:01)
- #14999 Convex functions are continuous (5 messages, latest: Oct 01 2024 at 07:01)
- #16651
fin_omega(6 messages, latest: Sep 29 2024 at 23:14) - #15624 computable
ZFSet.sUnion(5 messages, latest: Sep 29 2024 at 09:30) - #17220 and #17222 (2 messages, latest: Sep 29 2024 at 07:22)
- #16976 limits in the category of profinite groups (2 messages, latest: Sep 28 2024 at 15:04)
- #17197 move galois file (1 message, latest: Sep 28 2024 at 08:50)
- #17199 split WeierstrassCurve.VariableChange to a new file (2 messages, latest: Sep 28 2024 at 05:39)
- #16864 normal forms of elliptic curves (3 messages, latest: Sep 27 2024 at 18:19)
- #17140 (7 messages, latest: Sep 26 2024 at 07:54)
- #16666 abandon
ringandlinarithmore quickly (2 messages, latest: Sep 26 2024 at 00:16) - #17139 morphism properties respects left and respects right (1 message, latest: Sep 25 2024 at 20:41)
- #16916-19 Galois-group-is-profinite and Fundamental Theorem (7 messages, latest: Sep 24 2024 at 06:12)
- #16816 Limit of finite group is profinite group (17 messages, latest: Sep 24 2024 at 06:11)
- #17042 use
Std.HashMapin linarith (3 messages, latest: Sep 23 2024 at 08:57) - #15915 Cantor Normal Form (8 messages, latest: Sep 23 2024 at 03:11)
- #14269 feat(NumberTheory/FactorisationProperties): abundant, (2 messages, latest: Sep 23 2024 at 03:09)
- #15764 pre-game product cannot be lifted to games (2 messages, latest: Sep 21 2024 at 09:42)
- #15527 partition of a space into fibres (14 messages, latest: Sep 19 2024 at 11:54)
- #16897 weaken assumptions on local ring hom properties (5 messages, latest: Sep 18 2024 at 11:46)
- #13810 – branch has unmerged commits. (2 messages, latest: Sep 18 2024 at 11:18)
- #16489 chore: split Topology.Algebra.Module.WeakDual (7 messages, latest: Sep 17 2024 at 10:30)
- Work on MvPowerSeries (3 messages, latest: Sep 17 2024 at 09:57)
- #16828 ext lemma for EllipticCurve (3 messages, latest: Sep 16 2024 at 17:14)
- #16648 feat(Topology/Group/Profinite)Define Profinite Groups (28 messages, latest: Sep 16 2024 at 16:43)
- #16531 split Algebra.MonoidAlgebra.Basic (1 message, latest: Sep 16 2024 at 04:30)
- #16405 remove duplicate ToExpr Fin instance (3 messages, latest: Sep 16 2024 at 03:08)
- #16234 use List.eraseDups in simps (1 message, latest: Sep 16 2024 at 02:36)
- Further cleanup of Init.Logic (39 messages, latest: Sep 15 2024 at 11:53)
- #16349 golf proof of Sprague-Grundy (4 messages, latest: Sep 15 2024 at 04:28)
- #15535 Pedantic Linter (1 message, latest: Sep 13 2024 at 09:30)
- #16446 even and odd functions (2 messages, latest: Sep 12 2024 at 09:18)
- #16119 to_app attribute (2 messages, latest: Sep 12 2024 at 09:11)
- #14702 feat(Algebra/Polynomial/Derivation): coefficient-wise (1 message, latest: Sep 11 2024 at 11:42)
- #16088 Initial development of nimbers (9 messages, latest: Sep 11 2024 at 02:19)
- #16585 purely insep. ext. non-commutative case (1 message, latest: Sep 10 2024 at 18:40)
- #16584 Monomial orders and Groebner bases (7 messages, latest: Sep 10 2024 at 07:41)
- [#16630 feat: Pi.{zero,one}{mono,anti}](topic/.2316630.20feat.3A.20Pi.2E.7Bzero.2Cone.7D.7Bmono.2Canti.7D.html) (2 messages, latest: Sep 09 2024 at 18:15)
- #13416: define prefibered categories (2 messages, latest: Sep 09 2024 at 11:16)
- #16250 removing primed tactics from Combinatorics (6 messages, latest: Sep 09 2024 at 01:04)
- #15335 meta code for monoidal categories (41 messages, latest: Sep 09 2024 at 01:03)
- #16401 prove
Ordinallinear order instance earlier (3 messages, latest: Sep 07 2024 at 22:57) - ✔ #15722 tweak ordinal
simplemmas (4 messages, latest: Sep 06 2024 at 05:58) - #15383 needs a nudge (1 message, latest: Sep 05 2024 at 08:24)
- chore: deprecate unused MLList material (1 message, latest: Sep 05 2024 at 03:52)
- Approved PRs (2 messages, latest: Sep 03 2024 at 08:52)
- #16096 (2 messages, latest: Sep 02 2024 at 23:31)
- #15977 Add PSet.rank and ZFSet.rank (1 message, latest: Sep 01 2024 at 23:10)
- #15990 more lemmas on
Ordinal.log(1 message, latest: Sep 01 2024 at 17:04) - #9857 update nolints periodically (52 messages, latest: Sep 01 2024 at 01:06)
- #15522 feat: monotonicity lemmas for OrdinalApprox (9 messages, latest: Aug 31 2024 at 12:22)
- #15716 combinatorial game birthday (1 message, latest: Aug 31 2024 at 04:16)
- #16189 / #16198 removing induction' and cases' (5 messages, latest: Aug 30 2024 at 15:51)
- #15610 the longFile linter (8 messages, latest: Aug 30 2024 at 11:56)
- #15097 the long line linter as a syntax linter (39 messages, latest: Aug 29 2024 at 22:55)
- #16253 Basics of Discrete Fair Division (17 messages, latest: Aug 29 2024 at 21:43)
- #14739 Measure: add
gcongrlemmas (5 messages, latest: Aug 29 2024 at 04:47) - #16140 and relative representability (3 messages, latest: Aug 27 2024 at 11:26)
- #13997 analytic continuation of Dirichlet L-series (2 messages, latest: Aug 27 2024 at 07:33)
- #15686 FreeAlgebra asPowers, simp opts (3 messages, latest: Aug 26 2024 at 04:33)
- #15813 Actions on and by an order synonym (2 messages, latest: Aug 25 2024 at 20:26)
- #13950 Dualisable notion of ExistsAddOfLE (45 messages, latest: Aug 25 2024 at 15:23)
- #16120 Ring homomorphisms as a StrongHomClass (7 messages, latest: Aug 25 2024 at 01:52)
- #14660 Put a simplex between a point and a neighborhood (3 messages, latest: Aug 22 2024 at 22:12)
- #16018 SimpleGraph extending Digraph (24 messages, latest: Aug 22 2024 at 06:21)
- #15555: feat(RelSeries): LTSeries.iota (1 message, latest: Aug 21 2024 at 16:45)
- #15521 enable the setOption, longLine, missingEnd linters (3 messages, latest: Aug 20 2024 at 07:47)
- #15758 Nat.descFactorial_le (1 message, latest: Aug 19 2024 at 19:32)
- #15759 chore: backports from byAsSorry (1 message, latest: Aug 19 2024 at 11:10)
- #15960
Fintype (LTSeries α)ifFintype α(3 messages, latest: Aug 19 2024 at 04:33) - #15371 Remove some uses of
open Classical(25 messages, latest: Aug 17 2024 at 21:23) - #15920 functor
product : (A ⥤ B) × (C ⥤ D) ⥤ A × C ⥤ B × D(1 message, latest: Aug 17 2024 at 13:42) - #14091 on digraphs (13 messages, latest: Aug 17 2024 at 04:28)
- #14162 (3 messages, latest: Aug 16 2024 at 06:23)
- #15854 Make rel_iso_iff universe polymorphic (1 message, latest: Aug 15 2024 at 19:10)
- #13973
lake exe refactor(3 messages, latest: Aug 14 2024 at 08:04) - #15794 DocModule syntax linter (6 messages, latest: Aug 14 2024 at 08:01)
- #15635 ensure Batteries is fully built in
lake test(1 message, latest: Aug 14 2024 at 02:04) - #15258 Cat is monoidal with the cartesian product of categor (3 messages, latest: Aug 14 2024 at 01:33)
- #15380 topology on ENat (8 messages, latest: Aug 13 2024 at 22:24)
- #15614
typeToCatis right adjoint toconnectedComponents(2 messages, latest: Aug 13 2024 at 20:15) - #15756 backports from nightly-testing-2024-08-12 (2 messages, latest: Aug 13 2024 at 09:16)
- #15762 (2 messages, latest: Aug 13 2024 at 09:14)
- #15116 Make circle a type (8 messages, latest: Aug 13 2024 at 09:09)
- #15726 move to v4.11.0-rc2 (new
variable) (59 messages, latest: Aug 13 2024 at 00:13) - #15318 flexible linter fixes (2 messages, latest: Aug 12 2024 at 14:25)
- #15717 (8 messages, latest: Aug 12 2024 at 14:03)
- Style linter for ← (5 messages, latest: Aug 09 2024 at 19:58)
- Too many lines linter (28 messages, latest: Aug 09 2024 at 18:05)
- #15606 backports for leanprover/lean4#4814 (part 35) (1 message, latest: Aug 08 2024 at 20:15)
- #15221 remove outdated comment about
Bundled.map(3 messages, latest: Aug 08 2024 at 18:33) - #15424 Residue field is finite iff totally bounded DVR (19 messages, latest: Aug 07 2024 at 16:57)
- #15180 fix minImports for server (1 message, latest: Aug 07 2024 at 06:22)
- #14991 scalar tower instances for Module.End (1 message, latest: Aug 05 2024 at 21:04)
- #14721 change minimality to a predicate (20 messages, latest: Aug 05 2024 at 16:45)
- The category of pointed objects of a concrete category (20 messages, latest: Aug 05 2024 at 08:54)
- Speeding up Geometry/ (24 messages, latest: Aug 04 2024 at 13:53)
- #15447 union of an infinite collection of sets is infinite (1 message, latest: Aug 02 2024 at 15:20)
- [#15188 cleanup in Mathlib/Init/](topic/.2315188.20cleanup.20in.20Mathlib.2FInit.2F.html) (4 messages, latest: Aug 02 2024 at 11:20)
- squashing commits + keeping up with master in PR (2 messages, latest: Aug 02 2024 at 05:02)
- #15145 report commits in nightly testing bot (1 message, latest: Jul 31 2024 at 23:53)
- #13486 API for essentially small sites (2 messages, latest: Jul 31 2024 at 14:57)
- #15061 direct sums of matroids (6 messages, latest: Jul 31 2024 at 11:46)
- Algebraic geometry PRs (9 messages, latest: Jul 31 2024 at 06:53)
- #12273 Konig's infinity lemma (1 message, latest: Jul 30 2024 at 17:31)
- #15177 Renaming snorm to eLpNorm (4 messages, latest: Jul 30 2024 at 17:02)
- #9781 Dyck words (7 messages, latest: Jul 30 2024 at 07:37)
- #15171 move 'Walk' from
Connectivityinto its own file (16 messages, latest: Jul 30 2024 at 07:37) - #14699: Differential rings and notation (9 messages, latest: Jul 29 2024 at 12:27)
- #8304 Extended Hales-Jewett (25 messages, latest: Jul 29 2024 at 06:43)
- #13424 NormedSpace.Core (5 messages, latest: Jul 29 2024 at 01:34)
- #14927 clopen inside another set (1 message, latest: Jul 28 2024 at 16:39)
- #10541: SkewMonoidAlgebra (6 messages, latest: Jul 24 2024 at 10:41)
- #13514 CF languages union (2 messages, latest: Jul 23 2024 at 20:00)
- #14992: algebraic geometry: HasRingHomProperty (3 messages, latest: Jul 23 2024 at 19:33)
- #15001: algebraic geometry: opens of a scheme (1 message, latest: Jul 23 2024 at 19:21)
- #15028 More matroid closure + insertion (1 message, latest: Jul 22 2024 at 19:10)
- #15025 matroid closure and independence (1 message, latest: Jul 22 2024 at 17:16)
- #13483 update_deprecations (22 messages, latest: Jul 22 2024 at 17:06)
- #14975 define closed n-manifolds (5 messages, latest: Jul 21 2024 at 17:53)
- #14887 remove #align and #align_import statements (172 messages, latest: Jul 20 2024 at 16:34)
- quote4#47 documentation for
~q()(2 messages, latest: Jul 19 2024 at 21:27) - #14882: Being an isomorphism is local at the target (2 messages, latest: Jul 19 2024 at 10:49)
- #14858: AlgebraCat.FilteredColimits begins (29 messages, latest: Jul 19 2024 at 00:20)
- #14479 Antidiagonals for SMul and VAdd (2 messages, latest: Jul 18 2024 at 18:32)
- #14874 Euler's proof and counterexample of prime Fermat … (1 message, latest: Jul 18 2024 at 17:52)
- #14418 : the Laurent series valuation saga continues (8 messages, latest: Jul 18 2024 at 13:06)
- #14430 algebraic geometry morphisms refactor (4 messages, latest: Jul 18 2024 at 11:40)
- #14826 Split RingTheory.IntegralClosure (42 messages, latest: Jul 18 2024 at 11:04)
- #12016: unfold? tactic (1 message, latest: Jul 18 2024 at 10:01)
- #9249 suffix
ₚfor positivity assumptions (35 messages, latest: Jul 18 2024 at 01:00) - #14466 chore: split Algebra/Module/Equiv (1 message, latest: Jul 16 2024 at 16:58)
- #14437 – the
#min_importscommand (59 messages, latest: Jul 16 2024 at 15:12) - ✔ #13939 Multiplicative characters (9 messages, latest: Jul 15 2024 at 20:38)
- ✔ #14458 Polar set of a submodule (14 messages, latest: Jul 15 2024 at 20:38)
- #12221 Subbasis closed under intersection (4 messages, latest: Jul 15 2024 at 17:52)
- ✔ #14540 chore: remove scripts/mk_all.sh (6 messages, latest: Jul 15 2024 at 04:37)
- #14452 Coefficients of products of univ. power series (5 messages, latest: Jul 13 2024 at 17:19)
- #14704 typeclass for simple field extensions (1 message, latest: Jul 13 2024 at 09:50)
- #13317 Hopf monoids in braided categories (14 messages, latest: Jul 12 2024 at 20:44)
- #13972 Noetherian Schemes (1 message, latest: Jul 12 2024 at 17:56)
- #12572 Complete homogeneous, monomial symmetric polynomials (2 messages, latest: Jul 12 2024 at 11:21)
- #14647, splitting Combinatorics/SimpleGraph/Connectivity (9 messages, latest: Jul 11 2024 at 12:25)
- #14542 Making Equiv.Perm.support a Set (6 messages, latest: Jul 10 2024 at 22:24)
- #14616 Slightly strength Fin.completeLinearOrder (1 message, latest: Jul 10 2024 at 15:52)
- #14004 Strong atomicity (4 messages, latest: Jul 10 2024 at 15:41)
- Dualizing category theory API (6 messages, latest: Jul 10 2024 at 09:58)
- #13724 SubtractionMonoid instance for LinearOrderedAddCommGr (3 messages, latest: Jul 09 2024 at 17:35)
- #14571 Order and LexOrder of multivariate power series (1 message, latest: Jul 09 2024 at 16:43)
- #14163 (2 messages, latest: Jul 09 2024 at 16:29)
- #14557 extensible unused tactics (3 messages, latest: Jul 09 2024 at 08:39)
- #14454 Invertibility of power series (2 messages, latest: Jul 06 2024 at 16:33)
- #14431 Induction principles for ≤ on Nat (1 message, latest: Jul 06 2024 at 09:12)
- #13012 functors preserving 1-hypercovers are continuous (2 messages, latest: Jul 04 2024 at 12:51)
- #14197 Matroid closure (3 messages, latest: Jul 04 2024 at 07:31)
- #13210 shorten names of continued fraction declarations (19 messages, latest: Jul 03 2024 at 08:17)
- leanprover-community.github.io#480, #482,#483 Lean 4 update (4 messages, latest: Jul 03 2024 at 07:24)
- #13162 algebras essentially of finite type (1 message, latest: Jul 03 2024 at 07:10)
- #13637 (1 message, latest: Jul 02 2024 at 16:19)
- #14034 Well-founded of strictly monotone (1 message, latest: Jul 02 2024 at 14:21)
- #14195 Injections from disjoint sets (1 message, latest: Jul 02 2024 at 13:54)
- #14335 avoid order in
Module.LinearMap.End(4 messages, latest: Jul 01 2024 at 18:44) - #14233 scope
simps inAlgebra.AddConstMap(14 messages, latest: Jul 01 2024 at 15:50) - #13585 BinomialRing instance for NNRat algebras (2 messages, latest: Jul 01 2024 at 08:26)
- #13178 Krull dimension of a topological space (2 messages, latest: Jul 01 2024 at 01:03)
- #14060 bounded recursion on ordinals and clubs (1 message, latest: Jun 30 2024 at 12:13)
- #12346 Colexicographic order on
Finset Nat(15 messages, latest: Jun 29 2024 at 19:16) - #14219 delay imports of Star (1 message, latest: Jun 28 2024 at 11:47)
- ✔ #14095 Build fails in the checks (12 messages, latest: Jun 28 2024 at 08:30)
- #14188 blind abel to ordered algebra (2 messages, latest: Jun 28 2024 at 01:39)
- #14069 if the RHS constrains universes, make it explicit (7 messages, latest: Jun 27 2024 at 07:42)
- PRs for Turán's theorem (28 messages, latest: Jun 26 2024 at 14:44)
- #13145 : Removing finiteness requirement for cycleOf (27 messages, latest: Jun 26 2024 at 12:47)
- #13960 Matroid maps (2 messages, latest: Jun 26 2024 at 12:27)
- #9814 Tweak of
BoundedOrderandLatticeforFin(16 messages, latest: Jun 26 2024 at 10:33) - #13694 chore: reverse gdelta/separation dependency (3 messages, latest: Jun 26 2024 at 02:14)
- #14047 removing CI surrounding
move-decls(1 message, latest: Jun 23 2024 at 07:45) - #14002 making
TensorProduct.mulirreducible (1 message, latest: Jun 21 2024 at 16:56) - channel events (1 message, latest: Jun 21 2024 at 01:34)
- Porting notes (1 message, latest: Jun 20 2024 at 07:58)
- #13638 - set insertion / maximality (4 messages, latest: Jun 20 2024 at 03:23)
- #13929, doc-strings in Analysis/Convex/Slope (3 messages, latest: Jun 18 2024 at 17:48)
- #13692 Bijectivity on supersets (2 messages, latest: Jun 18 2024 at 16:06)
- subsingleton tactic #12525 (5 messages, latest: Jun 17 2024 at 22:24)
- #13887 Statement of Poincaré conjecture (7 messages, latest: Jun 17 2024 at 05:40)
- #13746: deprecate unused HashMap API additions (1 message, latest: Jun 16 2024 at 00:25)
- #12058 Diameter of simple graphs (2 messages, latest: Jun 15 2024 at 19:18)
- #13353 discrete Fourier transform on ZMod N (50 messages, latest: Jun 14 2024 at 17:01)
- #9398 itauto tactic (2 messages, latest: Jun 12 2024 at 17:47)
- #13013 bounded, a.e. cont. function is integrable on a box (4 messages, latest: Jun 12 2024 at 11:31)
- #11143 Bergelson Intersectivity Lemma (1 message, latest: Jun 11 2024 at 17:23)
- #13719: trans for implications (10 messages, latest: Jun 11 2024 at 11:00)
- #13716 add commit hash to PR summary (1 message, latest: Jun 11 2024 at 08:40)
- #13589 deprecate duplicate definitions about Bool (1 message, latest: Jun 11 2024 at 03:39)
- #12875 pairs (10 messages, latest: Jun 10 2024 at 13:37)
- ✔ #13605 cleanup redundant type arguments (4 messages, latest: Jun 10 2024 at 08:53)
- #13176 Feat: weaken 2ndCnt to Lindelof in Reg+Lind=>Normal (10 messages, latest: Jun 10 2024 at 08:43)
- #13540 move GaussSums from under LegendreSymbol (6 messages, latest: Jun 10 2024 at 04:34)
- #12555 inj/bij/surjectivity (4 messages, latest: Jun 08 2024 at 18:05)
- #9334 Sesquilinear Maps and Matrices (1 message, latest: Jun 08 2024 at 10:12)
- #12415 matroid constructions (9 messages, latest: Jun 07 2024 at 11:29)
- #13500 bors failed because of merge conflict (1 message, latest: Jun 07 2024 at 09:57)
- #12731 Make CompleteLinearOrder extend BiheytingAlgebra (4 messages, latest: Jun 06 2024 at 08:44)
- #3730 Remove
Catsuffix (6 messages, latest: Jun 06 2024 at 08:39) - #12544 Add regular sequence (1 message, latest: Jun 05 2024 at 20:03)
- #1388 Redefine pow in terms of iterate (31 messages, latest: Jun 05 2024 at 07:10)
- #13525 fix names for String lemmas (1 message, latest: Jun 05 2024 at 04:33)
- #13489 regularly update dependencies (1 message, latest: Jun 05 2024 at 01:53)
- #13521 chore(Data/UInt): deprecate UInt8.isUpper etc (1 message, latest: Jun 04 2024 at 23:31)
- #13489 chore: regularly update dependencies (2 messages, latest: Jun 04 2024 at 02:13)
- #13472 removing refine' (3 messages, latest: Jun 03 2024 at 09:12)
- #13170 remove accidental global instance (15 messages, latest: Jun 02 2024 at 20:59)
- #13392 Multiplicative characters (5 messages, latest: Jun 01 2024 at 20:11)
- #13413 fix to @[elementwise] (1 message, latest: Jun 01 2024 at 15:47)
- #13395 Add success message to the cache (3 messages, latest: Jun 01 2024 at 12:27)
- leanprover-community.github.io#391 calc mode for Lean 4 (3 messages, latest: Jun 01 2024 at 11:50)
- #13164 chore: remove bad simps, and add test (16 messages, latest: May 31 2024 at 21:35)
- #7386 Linear Programming (167 messages, latest: May 31 2024 at 19:29)
- ✔ #13065 normalized factors (5 messages, latest: May 31 2024 at 08:28)
- #13319 refactor of light profinite sets (3 messages, latest: May 30 2024 at 13:37)
- #13287 more refine' replacements (10 messages, latest: May 30 2024 at 11:19)
- #13357
refine'torefinefinal(?) batch (2 messages, latest: May 29 2024 at 23:12) - #13037 New simp lemmas for HomogeneousLocalization (1 message, latest: May 28 2024 at 18:25)
- #12986 second countable profinite spaces (1 message, latest: May 28 2024 at 12:21)
- #12498 some linear maps induced by mul. for submodules (1 message, latest: May 27 2024 at 22:36)
- #13115 smooth numbers (9 messages, latest: May 27 2024 at 12:00)
- #12551 No wrap-around principle for 3APs (1 message, latest: May 27 2024 at 07:02)
- #12992 (3 messages, latest: May 27 2024 at 06:16)
- #12653 More ways of bijecting finsets (1 message, latest: May 26 2024 at 10:12)
- #13142 Removing the hash-command linter script (6 messages, latest: May 25 2024 at 21:41)
- ✔ #11945 distance between vertices is 1 iff they are adja… (5 messages, latest: May 24 2024 at 19:48)
- ✔ feat: add competely normal (non-Hausdorff) property #12458 (2 messages, latest: May 24 2024 at 18:28)
- #13166
refine'torefine(43 messages, latest: May 24 2024 at 16:10) - #12769: Fourier transform of iterated derivatives (1 message, latest: May 24 2024 at 07:24)
- #13110 aesop_cat uses sorry if there is a sorry (7 messages, latest: May 23 2024 at 07:10)
- bimonoid objects (1 message, latest: May 23 2024 at 05:17)
- #13109 simp lemmas for unbundled comp and categorical ids (1 message, latest: May 23 2024 at 01:47)
- ✔ Docstrings for Computability: #12480 and #13087 (3 messages, latest: May 22 2024 at 06:50)
- concrete categories (4 messages, latest: May 22 2024 at 05:40)
- #13080 minor cleanup in aisle AG (5 messages, latest: May 22 2024 at 05:06)
- #12849 relax condition of Subalgebra.eq_bot_of_finrank_one (14 messages, latest: May 21 2024 at 19:44)
- #13045 (5 messages, latest: May 21 2024 at 04:08)
- #13054 simp normal form for Abelianization.map (1 message, latest: May 21 2024 at 01:50)
- #11920 towards proj construction (18 messages, latest: May 20 2024 at 15:44)
- #13046 backporting some additional implicit arguments (1 message, latest: May 20 2024 at 00:49)
- #12947, use
since := "YYYY-MM-DD"in @[deprecated] (5 messages, latest: May 17 2024 at 09:14) - #12567 chore: remove an unused congr lemma (5 messages, latest: May 17 2024 at 07:39)
- feat(Topology): stoneCechUnit injective for T35Space #12536 (4 messages, latest: May 16 2024 at 02:40)
- #12886 new CI check for noisy files (1 message, latest: May 15 2024 at 23:06)
- #12425 split RatFunc (2 messages, latest: May 15 2024 at 15:46)
- #12648 regular expression nfa equivalence (1 message, latest: May 14 2024 at 18:54)
- #12781 rename a few lemmas exp –> rexp (16 messages, latest: May 14 2024 at 11:28)
- #9733 (2 messages, latest: May 13 2024 at 01:04)
- #12705 Prime ideal separator in bounded dist lattices (10 messages, latest: May 11 2024 at 18:49)
- #12515: reduced diff in CI (24 messages, latest: May 11 2024 at 05:57)
- #12004 switch lean4checker to a cron job (2 messages, latest: May 10 2024 at 10:24)
- #11853 lake exe mkAll (6 messages, latest: May 10 2024 at 10:22)
- removing things labeled helper (1 message, latest: May 09 2024 at 20:25)
- #12777 split RingTheory.Ideal.Operations (6 messages, latest: May 09 2024 at 15:43)
- #12636 make Opposite.op the constructor for Opposite (2 messages, latest: May 08 2024 at 14:57)
- #12755 remove another refine' {..} pattern (1 message, latest: May 08 2024 at 12:17)
- #10681 positivity extension for posPart (1 message, latest: May 08 2024 at 06:24)
- #12741 even more universe annotations (1 message, latest: May 07 2024 at 21:15)
- #12729 clean up copying orders (1 message, latest: May 07 2024 at 16:51)
- feat: Positivity extension for Finset.prod #9365 (3 messages, latest: May 07 2024 at 15:14)
- #12546 Turn Freiman homs into predicates (6 messages, latest: May 07 2024 at 12:32)
- #12570 Construct a tripartite graph from its triangles (2 messages, latest: May 07 2024 at 06:23)
- #12144 Fourier transform on Schwartz space (10 messages, latest: May 06 2024 at 19:10)
- #12569 More additive energy lemmas (1 message, latest: May 06 2024 at 07:34)
- #12394 defines tight measures, is it too long? (18 messages, latest: May 05 2024 at 11:07)
- #12526 Locally linear graphs (1 message, latest: May 04 2024 at 18:22)
- #10824 Tensor products of finsupp types (26 messages, latest: May 04 2024 at 17:58)
- #12397 - some List.nthLe -> get migration (3 messages, latest: May 02 2024 at 15:53)
- #12563 slightly less defeq abuse in AG (7 messages, latest: May 01 2024 at 13:02)
- #12523 Triangle removal (1 message, latest: May 01 2024 at 07:49)
- #12422 multi-goal linter (5 messages, latest: Apr 30 2024 at 14:07)
- #12470 split MeasureTheory.Constructions.BorelSpace.Basic (7 messages, latest: Apr 29 2024 at 22:56)
- #10551 More big operators lemmas (7 messages, latest: Apr 29 2024 at 22:10)
- #8896 Triangle counting (2 messages, latest: Apr 29 2024 at 09:34)
- #12364 Move NormalizedGCDMonoid Int to reduce imports (9 messages, latest: Apr 27 2024 at 10:59)
- #3976 instance LawfulFunctor Array (4 messages, latest: Apr 27 2024 at 04:42)
- metapro book, #136, "run on Lean4 playground" (2 messages, latest: Apr 26 2024 at 16:18)
- #12380 direct sum of matroids (39 messages, latest: Apr 26 2024 at 12:27)
- std4#314 (8 messages, latest: Apr 26 2024 at 07:32)
- (deleted) (1 message, latest: Apr 25 2024 at 21:55)
- #9513 co/limits in
LightProfinite(2 messages, latest: Apr 23 2024 at 13:28) - Adding dates to remaining deprecations (2 messages, latest: Apr 22 2024 at 22:51)
- ✔ metaprogramming in lean, #131 (2 messages, latest: Apr 21 2024 at 08:49)
- #12279 Hölder's inequality (8 messages, latest: Apr 20 2024 at 19:11)
- #11774 Cocardinal, cocountable filters (1 message, latest: Apr 20 2024 at 11:27)
- std4#748 unbundle array size constraint from hash map bucket (12 messages, latest: Apr 19 2024 at 16:14)
- #10603 ae_toKernel_eq_one disappearing (3 messages, latest: Apr 17 2024 at 06:59)
- review request: #12120 (new theorems about Real.rpow) (12 messages, latest: Apr 16 2024 at 03:02)
- ✔ metapro book/#137 (6 messages, latest: Apr 15 2024 at 18:46)
- #12104 shorten long pole (2 messages, latest: Apr 15 2024 at 06:38)
- #7898 (3 messages, latest: Apr 14 2024 at 07:21)
- #11798 remove autoImplicit from more files (12 messages, latest: Apr 13 2024 at 22:19)
- #11620 add a few new theorems (2 messages, latest: Apr 13 2024 at 19:23)
- #12048 - The Iwasawa criterion for simplicity (5 messages, latest: Apr 13 2024 at 12:47)
- #12037 remove an instance (1 message, latest: Apr 09 2024 at 19:14)
- #11800 K-Lindelöf spaces (5 messages, latest: Apr 09 2024 at 18:08)
- PRs from sphere eversion (11 messages, latest: Apr 09 2024 at 12:50)
- #12023 Generalize preimage_smul_set etc to equivariant maps (1 message, latest: Apr 09 2024 at 06:38)
- #11822 flexible tactics linter (17 messages, latest: Apr 08 2024 at 11:27)
- metaprogramming in lean, #115 (1 message, latest: Apr 06 2024 at 13:38)
- #11867 eq_on versions of deriv lemmas (2 messages, latest: Apr 06 2024 at 06:22)
- #10515 and #10531 : cocardinal and CardinalInterFilter (13 messages, latest: Apr 04 2024 at 06:23)
- #10856 Measurability Modulo a filter (2 messages, latest: Apr 02 2024 at 17:11)
- PR #11851 Multigraphs, Paths, Homotopy (7 messages, latest: Apr 02 2024 at 13:48)
- > PR #11604: Serre graphs, fundamental groups, covering spac (9 messages, latest: Apr 02 2024 at 12:34)
- #11832 (4 messages, latest: Apr 01 2024 at 23:58)
- #11019: a syntax linter for #-commands (23 messages, latest: Mar 31 2024 at 07:55)
- #11776 higher derivative of Fourier transform (2 messages, latest: Mar 29 2024 at 20:34)
- bors crashed on #11322 and closed the PR (7 messages, latest: Mar 28 2024 at 16:44)
- #9163 Vitali's convergence theorem (2 messages, latest: Mar 27 2024 at 19:21)
- #11591 (3 messages, latest: Mar 27 2024 at 17:57)
- #11689 VCSP expressive power (12 messages, latest: Mar 27 2024 at 11:06)
- #11470 Uniform convergence topology type-synonym (1 message, latest: Mar 27 2024 at 05:11)
- PRs from new contributors (5 messages, latest: Mar 26 2024 at 22:12)
- #16040 Spin Group (40 messages, latest: Mar 26 2024 at 06:49)
- renaming symmetric MvPolynomials #11251 (7 messages, latest: Mar 24 2024 at 22:02)
- CI fails with unused variable error (19 messages, latest: Mar 24 2024 at 07:25)
- #11451 : change order of expansion for powers (5 messages, latest: Mar 23 2024 at 21:43)
- #11231 fix a crash in slim_check (2 messages, latest: Mar 22 2024 at 22:53)
- #10661 Positivity extension for integrals (2 messages, latest: Mar 22 2024 at 22:43)
- #11534: norm on a
PiTensorProduct(3 messages, latest: Mar 21 2024 at 20:23) - #11542 Splitting Data.List.Basic (3 messages, latest: Mar 21 2024 at 03:21)
- #11530 Rename
mul-divcancellation lemmas (2 messages, latest: Mar 20 2024 at 21:29) - characterize roots of unity in cyclotomic extensions #10710 (4 messages, latest: Mar 20 2024 at 16:34)
- #11247 non-terminal
simplinter (10 messages, latest: Mar 20 2024 at 15:54) - #10924: remove unnecessary assumptions (36 messages, latest: Mar 18 2024 at 08:37)
- #9736 single-edge graph (3 messages, latest: Mar 18 2024 at 04:02)
- #10565 Topological properties of order-connected sets in ℝⁿ (2 messages, latest: Mar 17 2024 at 18:02)
- #11372 DFA.acceptsFrom, DFA.map, DFA.equiv (2 messages, latest: Mar 17 2024 at 14:00)
- #11257 Basic lemmas about List recursion principles (1 message, latest: Mar 17 2024 at 12:54)
- [#11418 chore(): remove empty lines between variable](topic/.2311418.20chore().3A.20remove.20empty.20lines.20between.20variable.html) (4 messages, latest: Mar 16 2024 at 17:18)
- #11069 (sums over Int) (2 messages, latest: Mar 14 2024 at 13:01)
- #11303 (generalize and add 2 thms) (1 message, latest: Mar 12 2024 at 14:44)
- #11312 (move AddChar definitions) (1 message, latest: Mar 12 2024 at 09:59)
- #11305 — shrink
CategoryTheory.Subterminalby 95% (2 messages, latest: Mar 11 2024 at 22:12) - #11235 (1 message, latest: Mar 11 2024 at 09:31)
- #11214 L-series: naming (4 messages, latest: Mar 10 2024 at 16:53)
- #6307 refactor of monoidal categories (18 messages, latest: Mar 07 2024 at 23:11)
- #10562 feat(Tactic.Bound): Add a bound tactic for ineq… (2 messages, latest: Mar 06 2024 at 08:32)
- fix(fun_prop): few bug fixes for fun_prop #11092 (1 message, latest: Mar 05 2024 at 14:22)
- #10725 and #10728: L-series (112 messages, latest: Mar 05 2024 at 12:36)
- #6057 MulActionHom in the semilinear style (30 messages, latest: Mar 05 2024 at 10:42)
- #11002 (operator norm) (2 messages, latest: Mar 04 2024 at 20:27)
- #7496 add nonterminal simp checker (10 messages, latest: Mar 03 2024 at 10:48)
- #11049 (1 message, latest: Feb 29 2024 at 19:47)
- #10000 Abel's limit theorem (3 messages, latest: Feb 29 2024 at 12:50)
- ✔ #11050: split InfiniteSum.Basic (4 messages, latest: Feb 29 2024 at 10:29)
- Positivity extensions (5 messages, latest: Feb 29 2024 at 09:14)
- #10566 - bounded sets of PGames (2 messages, latest: Feb 28 2024 at 15:58)
- #11027 - First isomorphism theorem for algebras (1 message, latest: Feb 28 2024 at 06:45)
- #10833 cleanup Fourier (1 message, latest: Feb 28 2024 at 06:07)
- #10909 porting notes in
RingTheory.Polynomial.Basic(3 messages, latest: Feb 28 2024 at 04:47) - #11022 remove an
erw(1 message, latest: Feb 27 2024 at 20:06) - #9815 split
Topology/MetricSpace/Pseudometric.lean(6 messages, latest: Feb 26 2024 at 16:30) - #7894 fractional polymorphisms for VCSP (6 messages, latest: Feb 26 2024 at 08:42)
- #10910 appropriate transparency level for diamond checks (7 messages, latest: Feb 25 2024 at 17:17)
- #10907 split Mathlib.GroupTheory.Perm.Cycle.Basic (16 messages, latest: Feb 24 2024 at 17:06)
- #10900 split off ordered instances for subalgebraic things (3 messages, latest: Feb 23 2024 at 22:57)
- #10581 string diagrams (1 message, latest: Feb 23 2024 at 04:10)
- #10828 - generalizing CommRing to CommSemiring etc. (11 messages, latest: Feb 21 2024 at 22:54)
- #10724
fun_proprefactor and bug fixes (1 message, latest: Feb 19 2024 at 18:26) - #10715 - correct a docstring (1 message, latest: Feb 19 2024 at 10:49)
- #10637 - correct bug in Mathlib.Data.Finset.Sym (12 messages, latest: Feb 18 2024 at 07:03)
- #10640 - remove old style uses of
have(7 messages, latest: Feb 17 2024 at 12:02) - #8187 & #8788 (4 messages, latest: Feb 16 2024 at 14:40)
- #9933 actually check cache works (12 messages, latest: Feb 16 2024 at 10:47)
- #10415 Add yang baxter equation and the opposite braided mon (5 messages, latest: Feb 15 2024 at 23:22)
- feat: define PGame.identical PGame.memₗ PGame.memᵣ #5901 (14 messages, latest: Feb 15 2024 at 21:31)
- #10009 Dilation equiv in normed spaces (1 message, latest: Feb 14 2024 at 18:52)
- PR #6042 Singular Value Decomposition (41 messages, latest: Feb 13 2024 at 19:00)
- chore: add setting to prevent accidental editing of depende (3 messages, latest: Feb 13 2024 at 18:58)
- #10496 address porting notes in
Order.Grade(5 messages, latest: Feb 13 2024 at 17:32) - #9372, convolution of measures (1 message, latest: Feb 12 2024 at 19:07)
- #10139 everywhere positive sets (7 messages, latest: Feb 12 2024 at 13:17)
- #10403 notation scopes for arith funs (1 message, latest: Feb 12 2024 at 11:05)
- #8979 making Finsupp.filter computable (10 messages, latest: Feb 12 2024 at 08:33)
- #9920 reorganisation of coherent files (3 messages, latest: Feb 11 2024 at 10:50)
- ✔ #9910 generalizing mkPiField (2 messages, latest: Feb 09 2024 at 19:26)
- #10344 removing norm_num support for Nat.sub, Sub.sub, etc (17 messages, latest: Feb 09 2024 at 05:38)
- #10316 remove duplicate instances (1 message, latest: Feb 07 2024 at 00:00)
- #10099 Integration by parts (5 messages, latest: Feb 05 2024 at 08:46)
- "Staging failed at cache" bell (6 messages, latest: Feb 04 2024 at 21:54)
- #8773 Extensionality principle for bitvectors (1 message, latest: Feb 03 2024 at 20:47)
- #10191 heartbeat bumped files down into the single digits (12 messages, latest: Feb 02 2024 at 22:23)
- #10185 renaming with deprecation (4 messages, latest: Feb 02 2024 at 22:19)
- #10187 ensure that the linter fails when it should (9 messages, latest: Feb 02 2024 at 14:15)
- Preliminary PRs for L-series (5 messages, latest: Feb 01 2024 at 20:05)
- #10077 rename _0 -> _zero, _1 -> _one (3 messages, latest: Jan 31 2024 at 21:34)
- #10129 Make
infsepconsistent withdiamandinfdist(1 message, latest: Jan 30 2024 at 17:31) - #9961
positivityextension foralgebraMap(1 message, latest: Jan 30 2024 at 13:36) - #9145 Refactor of succAbove etc. (96 messages, latest: Jan 30 2024 at 13:02)
- #10042 New lemmas for succAbove (3 messages, latest: Jan 26 2024 at 22:30)
- ✔ #9869 splitting Data.ENNReal.Basic (2 messages, latest: Jan 26 2024 at 01:29)
- #9658
avoidfix tc search (1 message, latest: Jan 25 2024 at 22:32) - #9564 Weaken commutativity assumptions for AdjoinRoot.lift a (23 messages, latest: Jan 25 2024 at 15:37)
- #9847, #9889 arctangent API (1 message, latest: Jan 23 2024 at 01:59)
- Rename and small lemma (1 message, latest: Jan 21 2024 at 20:46)
- #8735 finpartitions from setoids (9 messages, latest: Jan 21 2024 at 02:55)
- ✔ #9783 and #9666 Modular forms (12 messages, latest: Jan 20 2024 at 12:19)
- #9728 tidying (5 messages, latest: Jan 17 2024 at 22:58)
- #9791 + #9793: Redefine predAbove and succAbove (4 messages, latest: Jan 17 2024 at 00:41)
- #9588, #9565 Splitting MFDeriv (5 messages, latest: Jan 16 2024 at 23:00)
- ✔ #9780 Redefinition of castPred (11 messages, latest: Jan 16 2024 at 20:58)
- ✔ #9652
Matrix.dotProductinequalities (16 messages, latest: Jan 15 2024 at 14:55) - #9658 avoid tc search (4 messages, latest: Jan 15 2024 at 14:07)
- Move set definitions to a new file #9737 (24 messages, latest: Jan 15 2024 at 13:54)
- #9251 caratheodory theorem for convex cones (10 messages, latest: Jan 15 2024 at 10:13)
- #9006 Unit subgroup (56 messages, latest: Jan 15 2024 at 01:02)
- #9695 Performance issues refactoring
Submodulelattice def (1 message, latest: Jan 12 2024 at 17:40) - (Frechet) derivative of the Fourier transform (1 message, latest: Jan 11 2024 at 22:04)
- #9655 de-prioritize
Subalgebra.module'(4 messages, latest: Jan 11 2024 at 18:39) - #9267 local graph operations (13 messages, latest: Jan 11 2024 at 16:06)
- #9636 and #9637 speed up CategoryTheory files (7 messages, latest: Jan 11 2024 at 09:38)
- HasPrimitives on disc (1 message, latest: Jan 09 2024 at 22:48)
- chore(Covby): rename Covby to CovBy #9578 (7 messages, latest: Jan 09 2024 at 09:06)
- #9555 speed up ProjectiveResolution (7 messages, latest: Jan 08 2024 at 20:22)
- #9556 Removing yet another commutativity assumption (5 messages, latest: Jan 08 2024 at 19:49)
- #9495 Remove yet another commutativity instance (1 message, latest: Jan 06 2024 at 23:30)
- #9493 Weaken an instance (3 messages, latest: Jan 06 2024 at 23:21)
- #9404 EReal (2 messages, latest: Jan 05 2024 at 21:21)
- ✔ #9408 and #9200 (2 messages, latest: Jan 05 2024 at 13:39)
- Integral curves on manifolds (9 messages, latest: Jan 05 2024 at 09:11)
- #9399 and #9400 (2 messages, latest: Jan 04 2024 at 07:13)
- #9359 Centralizer of a permutation (1 message, latest: Dec 31 2023 at 13:20)
- #9270 estimates for the complex logarithm (3 messages, latest: Dec 29 2023 at 21:26)
- #13483
move_add(69 messages, latest: Dec 27 2023 at 19:28) - #7904 Antidiagonal for finsupp-orted functions (3 messages, latest: Dec 26 2023 at 15:57)
- #6057 refactor MulActionHom to allow “semilinear”-style maps (2 messages, latest: Dec 26 2023 at 15:18)
- #9159 dimension of dual space (Erdős-Kaplansky) (8 messages, latest: Dec 25 2023 at 19:43)
- #8878 refactor(ProperCone) (2 messages, latest: Dec 24 2023 at 05:31)
- ✔ Linear maps and DistribMulAction hom (#6057) (8 messages, latest: Dec 23 2023 at 16:19)
- #9116 Introducing Complex.slitPlane (57 messages, latest: Dec 23 2023 at 06:53)
- #7506 : compatible measures on quotient spaces and groups (3 messages, latest: Dec 19 2023 at 04:09)
- #9114 API for
ltByCases(101 messages, latest: Dec 17 2023 at 09:12) - #9079 Golfing simps (10 messages, latest: Dec 17 2023 at 00:28)
- #7795 Nonterminal simps (14 messages, latest: Dec 16 2023 at 00:06)
- #8809 positive semidef matrices (29 messages, latest: Dec 15 2023 at 18:00)
- #15763: Lie group of ring units (19 messages, latest: Dec 14 2023 at 13:39)
- #8732 (Matroid Duality) (1 message, latest: Dec 12 2023 at 15:07)
- #8727 refactoring sheafification (10 messages, latest: Dec 11 2023 at 21:29)
- #7506 aesop timeout (6 messages, latest: Dec 08 2023 at 20:11)
- #6582 (7 messages, latest: Dec 08 2023 at 17:46)
- #8559 Character module (5 messages, latest: Dec 08 2023 at 15:42)
- #8614 and #8615 (derivatives, fundamental thm of calculus) (11 messages, latest: Dec 07 2023 at 19:56)
- #8480 (1 message, latest: Dec 07 2023 at 17:19)
- #8178 space after ← (47 messages, latest: Dec 04 2023 at 16:55)
- #7815 some matrix results (2 messages, latest: Dec 04 2023 at 14:41)
- #8751 Euler products (1 message, latest: Dec 04 2023 at 11:17)
- Quick style PRs (2 messages, latest: Dec 03 2023 at 07:50)
- #8721 Binary products of finite measures (3 messages, latest: Dec 02 2023 at 23:18)
- #8774 special unitary group (3 messages, latest: Dec 01 2023 at 19:34)
- #8725 review normed group structure on ContinuousLinearMap (2 messages, latest: Dec 01 2023 at 17:40)
- #7810 LibrarySearch test failures (5 messages, latest: Nov 30 2023 at 13:51)
- #8642 Lemmas about List.map (1 message, latest: Nov 30 2023 at 11:46)
- #7843 Homomorphism from centre into centroid (1 message, latest: Nov 28 2023 at 19:17)
- #8071 Matroid axioms (4 messages, latest: Nov 28 2023 at 17:41)
- #8397 Lie group structure on units of a complete normed ring (1 message, latest: Nov 28 2023 at 08:28)
- #8449 Bounds for Dirichlet character values (23 messages, latest: Nov 27 2023 at 20:37)
- #8584 TensorProduct.liftAddHom (8 messages, latest: Nov 27 2023 at 16:55)
- #7394 Tensor products of graded algebras (1 message, latest: Nov 27 2023 at 12:34)
- #6856 match_xYz (25 messages, latest: Nov 25 2023 at 22:17)
- #8440 Dirichlet characters (1 message, latest: Nov 23 2023 at 09:49)
- #7060 Separate commutative and associative multiplication (1 message, latest: Nov 21 2023 at 20:39)
- #8498 uniqueness of weak limits of finite Borel measures (4 messages, latest: Nov 20 2023 at 09:17)
- ✔ #8524 easy liminf / limsup lemmas (3 messages, latest: Nov 20 2023 at 08:10)
- hint tactic (10 messages, latest: Nov 19 2023 at 02:43)
- #8410 Euler products (1 message, latest: Nov 18 2023 at 11:06)
- Dirichlet characters (10 messages, latest: Nov 17 2023 at 20:27)
- ✔ #8406 IsIntegral dot notation, noncomm generalization &… (2 messages, latest: Nov 17 2023 at 17:46)
- #8086 Removing Add.add from theorem statements (6 messages, latest: Nov 16 2023 at 14:27)
- #8189 add Trans instance for List.Perm and a lemma on Lists (1 message, latest: Nov 16 2023 at 08:44)
- #8409 (1 message, latest: Nov 15 2023 at 20:03)
- #8107 (3 messages, latest: Nov 15 2023 at 18:55)
- #7801 split LinearAlgebra.Basic (2 messages, latest: Nov 15 2023 at 09:47)
- #7905 instance for non-dependent
FunLike(34 messages, latest: Nov 15 2023 at 09:38) - #8389 split MeasureSpace.lean into 3 files (20 messages, latest: Nov 13 2023 at 21:52)
- #8325 (3 messages, latest: Nov 13 2023 at 18:44)
- #7903 define UnboundedSpace (11 messages, latest: Nov 11 2023 at 18:20)
- #8252 smooth numbers (1 message, latest: Nov 11 2023 at 10:44)
- #6363 feat: More to #find! (18 messages, latest: Nov 11 2023 at 00:25)
- #8068 (1 message, latest: Nov 06 2023 at 16:23)
- #7341 updateFinset (19 messages, latest: Nov 06 2023 at 12:47)
- #7790 polyrith radicals (7 messages, latest: Nov 03 2023 at 15:56)
- #7894 VCSP theory RFC (3 messages, latest: Nov 03 2023 at 13:45)
- #6996 Define the centre … for non-associative algebras (26 messages, latest: Nov 03 2023 at 10:59)
- #7885 add namespace
UpperHalfPlane.ModularGroup(10 messages, latest: Nov 01 2023 at 09:03) - #8029: replace ContinuousMap.Homotopy with Function.Homotopy (14 messages, latest: Oct 31 2023 at 18:04)
- #7860 ClosableCompactSubsetOpenSpace (1 message, latest: Oct 31 2023 at 15:39)
- #7685 peel tactic (13 messages, latest: Oct 30 2023 at 16:41)
- #5376
reduce_mod_chartactic (6 messages, latest: Oct 30 2023 at 15:10) - #8006 ofNat lemmas (11 messages, latest: Oct 29 2023 at 18:34)
- #7883 rings vs orders (22 messages, latest: Oct 26 2023 at 00:26)
- #7404 VCSP (21 messages, latest: Oct 24 2023 at 13:32)
- #7854 split
CategoryTheory/Sites/SheafOfTypes(2 messages, latest: Oct 23 2023 at 22:06) - #5901
PGame.Identical(1 message, latest: Oct 22 2023 at 07:00) - #7506 inferInstance issues (17 messages, latest: Oct 20 2023 at 21:02)
- #7606, adaptations for lean4#2644 (34 messages, latest: Oct 20 2023 at 13:12)
- !4#4593 (23 messages, latest: Oct 20 2023 at 10:17)
- #7205 pp.beta (33 messages, latest: Oct 19 2023 at 14:00)
- ✔ #7664 and #7723: boring lemmas about quadratic forms (2 messages, latest: Oct 19 2023 at 13:01)
- #7552 analytic functions (6 messages, latest: Oct 18 2023 at 11:10)
- #7040 Uniformly and strongly convex functions (4 messages, latest: Oct 18 2023 at 04:55)
- #7586 / !3#17142: polyrith crash (7 messages, latest: Oct 18 2023 at 01:44)
- #7486 antidiagonal (21 messages, latest: Oct 11 2023 at 15:36)
- #6578 compact subsets in products as limits in
Profinite(3 messages, latest: Oct 10 2023 at 15:45) - #6223 the Unfolding Trick (56 messages, latest: Oct 07 2023 at 09:52)
- #7326 suppress_compilation tactic (17 messages, latest: Oct 04 2023 at 08:36)
- #7368 lean4checker (2 messages, latest: Oct 03 2023 at 02:05)
- std4#243 (7 messages, latest: Oct 02 2023 at 08:58)
- #7433 cycleTypes of perm (2 messages, latest: Sep 29 2023 at 15:03)
- ✔ #7367 CONTRIBUTING.md (3 messages, latest: Sep 29 2023 at 14:19)
- #6589 LocallyConstant.piecewise' (3 messages, latest: Sep 29 2023 at 13:10)
- #7319 harmonic number not an integer (15 messages, latest: Sep 28 2023 at 22:46)
- super factorial and vandermonde determinant (5 messages, latest: Sep 26 2023 at 19:35)
- #6310 OrderedAddCommMonoidWithOne (17 messages, latest: Sep 24 2023 at 01:09)
- #7203
R\[A\]forAddMonoidAlgebra R A(1 message, latest: Sep 16 2023 at 06:00) - #7148 bump to nightly-2023-09-14 (2 messages, latest: Sep 15 2023 at 00:27)
- #6755 UniqueProds: subsingleton and MulOpposite lemmas (6 messages, latest: Sep 14 2023 at 12:43)
- !3#18732 Bergelson intersectivity (10 messages, latest: Sep 14 2023 at 06:33)
- #6998 (8 messages, latest: Sep 11 2023 at 19:16)
- #6385 context-free grammars (25 messages, latest: Sep 11 2023 at 10:20)
- #6880 Zeckendorf's Theorem (2 messages, latest: Sep 07 2023 at 20:32)
- #3464 nondeterminism monad (8 messages, latest: Sep 07 2023 at 09:19)
- #6437 pointed cones (12 messages, latest: Sep 05 2023 at 15:31)
- #6870 change junk value for supremum of unbounded sets (5 messages, latest: Sep 05 2023 at 13:40)
- #6896 regular and extensive coverages (1 message, latest: Sep 05 2023 at 09:48)
- #6151 adn #6153 lake exe graph (4 messages, latest: Sep 05 2023 at 09:20)
- #232 (4 messages, latest: Sep 05 2023 at 06:02)
- #6568 and #6569 (3 messages, latest: Sep 04 2023 at 16:38)
- #6342 (14 messages, latest: Sep 04 2023 at 14:19)
- #6864 (4 messages, latest: Sep 03 2023 at 07:23)
- fix ODE theorem (1 message, latest: Sep 03 2023 at 05:01)
- #6588 nilpotent matrices have nilpotent trace (3 messages, latest: Sep 02 2023 at 19:34)
- #6447 Right exactness of tensor product (55 messages, latest: Sep 02 2023 at 10:10)
- ✔ #6920 Correct a name (2 messages, latest: Sep 02 2023 at 09:32)
- #6808 vertex replacement (4 messages, latest: Sep 01 2023 at 03:25)
- #6866 (12 messages, latest: Sep 01 2023 at 02:01)
- #6728 sorting lemmas (1 message, latest: Aug 31 2023 at 21:31)
- #6729 Add lemmas to working with LiftRel (11 messages, latest: Aug 31 2023 at 11:47)
- ✔ #6756 mem_doubleton (20 messages, latest: Aug 29 2023 at 20:52)
- docker (1 message, latest: Aug 29 2023 at 18:41)
- #6842, deleting an empty file (1 message, latest: Aug 29 2023 at 09:10)
- #6736 Bool consistency. (18 messages, latest: Aug 28 2023 at 22:18)
- #6663 Create direct versions of getLeft? and getRight? (1 message, latest: Aug 28 2023 at 09:49)
- #6714 Generalisation of nodal polynomial. (1 message, latest: Aug 28 2023 at 09:46)
- #6372 maps from the unitization of non-unital subobjects (5 messages, latest: Aug 25 2023 at 18:00)
- #6696 clique folder (6 messages, latest: Aug 24 2023 at 07:24)
- #5930 Ring.divide (4 messages, latest: Aug 22 2023 at 17:15)
- #5858 Profinite is precoherent (1 message, latest: Aug 22 2023 at 10:53)
- #5808 projectivity of Stonean spaces in CompHaus (1 message, latest: Aug 22 2023 at 10:34)
- #6365
GametoSetTheory.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?andext!?(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
FunLikeforOrderHom(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 yby 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_negoption (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_mapahas_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
qifytactic (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
ℤ ∙ eis 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
degreeof 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-
classirreducible(1 message, latest: Jul 11 2022 at 11:32) - #14834 Coalgebras over an endofunctor (2 messages, latest: Jul 11 2022 at 07:34)
- #13397 continuous map from Proj to Spec (1 message, latest: Jul 11 2022 at 00:28)
- #15232 transferring "enough injectiveness" (1 message, latest: Jul 10 2022 at 23:54)
- ✔ #14347 Cantor Normal Form: cleanup + generalize results (5 messages, latest: Jul 10 2022 at 22:41)
- ✔ #14955 tweak irreducible attribute in nat_ordinal (11 messages, latest: Jul 10 2022 at 22:37)
- #14347 Cantor Normal Form: cleanup + generalize results (3 messages, latest: Jul 10 2022 at 22:10)
- #14955 tweak irreducible attribute (1 message, latest: Jul 10 2022 at 22:03)
- ✔ #14757 review cast API (1 message, latest: Jul 10 2022 at 22:02)
- #14497 Harris-Kleitman inequality (2 messages, latest: Jul 10 2022 at 16:10)
- #15056 Fixing a diamond (1 message, latest: Jul 10 2022 at 10:28)
- #11162 Stars and bars re-revisited (26 messages, latest: Jul 09 2022 at 14:16)
- #14876 lemmas about balanced sets (4 messages, latest: Jul 08 2022 at 23:42)
- #14928 boring n-ary lemmas (1 message, latest: Jul 08 2022 at 18:06)
- #14697 Ruzsa covering (3 messages, latest: Jul 08 2022 at 16:21)
- #14549 birthday of addition equals natural addition of birth (4 messages, latest: Jul 07 2022 at 16:37)
- #14762
compute_degree_le(1 message, latest: Jul 07 2022 at 10:25) - #14034 induced graphs, cliques, coloring bounds (6 messages, latest: Jul 06 2022 at 18:42)
- #15066
pmfis_lawful_monad (5 messages, latest: Jul 06 2022 at 18:39) - #14713 non-
classirreducible(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
finiteinstances forset(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
finitepredicate (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.addAPI (1 message, latest: May 20 2022 at 14:31) - #13611 Tweak
pgame.addAPI (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_duptodedup(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_searchand 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_simpproviding 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.Infofa • 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
floorandceil(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
nontrivialinstance fornnreal(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
oppositeto 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_enumclass (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
enumerableclass (6 messages, latest: Aug 30 2019 at 20:14) - #1366 add a
ltrelation independent fromlefor 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!andfail!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
ppinstead ofto_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_additiverecursively (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: Feb 28 2026 at 14:05 UTC