Zulip Chat Archive

Stream: triage

---

Topics:

• PR !4#6183: chore: remove normalizeScaleRoots (1 message, latest: Sep 29 2023 at 14:04)
• issue !4#430: tactic porting tracking issue (1 message, latest: Sep 29 2023 at 14:04)
• PR !4#6605: feat: add Fin.cons_mem_piFinset_iff (1 message, latest: Sep 28 2023 at 14:04)
• issue !4#4955: Make inhabit use simp \[nontriviality\] … (1 message, latest: Sep 28 2023 at 14:04)
• PR !4#6856: feat(Data/List): match_xYz (1 message, latest: Sep 27 2023 at 14:04)
• issue !4#1074: to_additive feature requests (1 message, latest: Sep 27 2023 at 14:04)
• PR !4#3042: perf: preprocess tc instances to avoid nested tc (1 message, latest: Sep 26 2023 at 14:04)
• issue !4#6091: My 100 theorems (1 message, latest: Sep 26 2023 at 14:04)
• PR !4#290: feat: profunctor optics (1 message, latest: Sep 25 2023 at 14:04)
• issue !4#5164: sometimes rw worked in mathlib3 but we h… (1 message, latest: Sep 25 2023 at 14:04)
• PR !4#6385: feat(Computability/CFG): define context-free … (1 message, latest: Sep 24 2023 at 14:03)
• issue !4#5379: Extend basic API about DomMulAct (1 message, latest: Sep 24 2023 at 14:03)
• PR !4#7205: feat: pp.beta (1 message, latest: Sep 23 2023 at 14:04)
• issue !4#6607: Write a custom elaborator/unification hint… (1 message, latest: Sep 23 2023 at 14:04)
• [PR !4#7079: fix(): theorem to lemma](topic/PR.20!4.237079.3A.20fix().3A.20.60theorem.60.20to.20.60lemma.60.html) (5 messages, latest: Sep 22 2023 at 18:12)
• issue !4#6814: allow Cache use alternative mirror URL v… (1 message, latest: Sep 22 2023 at 14:04)
• PR !4#7101: feat: self_le_pow (1 message, latest: Sep 21 2023 at 14:04)
• issue !4#5030: continuity tactic is not as capable as i… (1 message, latest: Sep 21 2023 at 14:04)
• PR !4#6930: feat: resynth_instances tactic for resynthe… (1 message, latest: Sep 20 2023 at 14:04)
• issue !4#2202: Redesign bundled morphisms and sets (1 message, latest: Sep 20 2023 at 14:04)
• PR !4#6268: Fixups to #3838 (1 message, latest: Sep 19 2023 at 14:04)
• issue !4#740: add protected after the fact? (1 message, latest: Sep 19 2023 at 14:04)
• PR !4#6926: feat: environment extension for #align_import (1 message, latest: Sep 18 2023 at 14:04)
• issue !4#6376: Refactor of Algebra/Order/LatticeGroup w… (1 message, latest: Sep 18 2023 at 14:04)
• [PR !4#6931: refactor(Analysis/Normed): use `RingHomIsome…](topic/PR.20!4.236931.3A.20refactor(Analysis.2FNormed).3A.20use.20.60RingHomIsome.2E.2E.2E.html) (2 messages, latest: Sep 17 2023 at 22:07)
• issue !4#5343: notation3 doesn't work with scoped (1 message, latest: Sep 17 2023 at 14:03)
• PR !4#6859: TryLean4Bundle: Windows Bundle Creator (1 message, latest: Sep 16 2023 at 14:03)
• issue !4#2427: positivity enhancement (1 message, latest: Sep 16 2023 at 14:03)
• PR !4#6583: feat: Asymptotic order of divide-and-conquer … (3 messages, latest: Sep 15 2023 at 15:26)
• issue !4#5017: Missing FunLike instances for Quivers (1 message, latest: Sep 15 2023 at 14:04)
• PR !4#1470: feat: attach and filter lemmas (10 messages, latest: Sep 14 2023 at 17:39)
• issue !4#6646: Make use of loopy instances for implicatio… (1 message, latest: Sep 14 2023 at 14:03)
• PR !4#5383: feat: define Bitvec constants for -1, INT_MIN… (1 message, latest: Sep 13 2023 at 14:03)
• issue !4#5026: Tracking issue for unknown simp regressions (1 message, latest: Sep 13 2023 at 14:03)
• PR !4#282: feat: deriving optics (1 message, latest: Sep 12 2023 at 14:04)
• issue !4#5265: Improve positivity extension for norm (1 message, latest: Sep 12 2023 at 14:04)
• PR !4#6808: feat: vertex replacement (1 message, latest: Sep 11 2023 at 14:04)
• issue !4#2136: norm_num functionality tracking issue (1 message, latest: Sep 11 2023 at 14:04)
• PR !4#5280: feat: a convex set is homeomorphic to the uni… (1 message, latest: Sep 10 2023 at 14:03)
• issue !4#994: decide regression (1 message, latest: Sep 10 2023 at 14:03)
• PR !4#5745: feat: a tactic to consume type annotations, a… (1 message, latest: Sep 09 2023 at 14:03)
• issue !4#2030: refactor: add TC cycles (1 message, latest: Sep 09 2023 at 14:03)
• PR !4#6500: feat: add theorem cast_subgroup_of_units_card… (1 message, latest: Sep 08 2023 at 14:04)
• issue !4#5539: Orthogonality for affine subspaces (1 message, latest: Sep 08 2023 at 14:04)
• is the bot dead (4 messages, latest: Sep 07 2023 at 14:41)
• PR #14960: feat(group_theory/subgroup/basic): add center_… (2 messages, latest: Aug 31 2023 at 14:07)
• issue #15907: Refactor bilinear forms (4 messages, latest: Aug 31 2023 at 14:07)
• [PR #16351: feat(analysis/inner_product_space/reproducing_…](topic/PR.20.2316351.3A.20feat(analysis.2Finner_product_space.2Freproducing_.2E.2E.2E.html) (1 message, latest: Aug 30 2023 at 14:07)
• issue #4906: Redefine linear_map.tensor to be a bundled… (8 messages, latest: Aug 30 2023 at 14:07)
• PR #17769: feat(data/list/off_diag): add list.off_diag (2 messages, latest: Aug 29 2023 at 14:07)
• issue #13461: to_ framework (3 messages, latest: Aug 29 2023 at 14:07)
• PR #10253: feat(group_theory/iwasawa.lean): add a proof o… (1 message, latest: Aug 28 2023 at 14:07)
• issue #2102: Document _eta, _beta etc in naming (9 messages, latest: Aug 28 2023 at 14:07)
• PR #16681: feat(analysis/locally_convex/barrel): barreled… (2 messages, latest: Aug 27 2023 at 14:35)
• issue #4014: Miracle Flatness and Zariski's Main Theorem (35 messages, latest: Aug 27 2023 at 14:07)
• PR #8913: feat(ring_theory/mv_polynomial/homogeneous): Mu… (3 messages, latest: Aug 26 2023 at 14:07)
• issue #7189: Lemmas produced by @\[elementwise\] aren't u… (10 messages, latest: Aug 26 2023 at 14:07)
• PR #18754: feat(order/flag): Order isomorphisms act on flags (1 message, latest: Aug 25 2023 at 14:07)
• issue #10728: Alternative dot notation (6 messages, latest: Aug 25 2023 at 14:07)
• PR #18258: chore(order/filter/n_ary): redefine, golf (1 message, latest: Aug 24 2023 at 14:07)
• issue #14994: nth_rewrite incorrectly unifies universe va… (5 messages, latest: Aug 24 2023 at 14:07)
• PR #15983: feat(algebra/monoid_algebra/no_zero_divisors):… (3 messages, latest: Aug 23 2023 at 14:48)
• issue #15734: Banach-Alaoglu for topological vector spaces (5 messages, latest: Aug 23 2023 at 14:07)
• PR #11448: feat(algebraic_geometry): Quasi-compact morphisms (3 messages, latest: Aug 22 2023 at 14:07)
• issue #3095: Document rw configuration (12 messages, latest: Aug 22 2023 at 14:07)
• issue #5059: Geometric Algebra (14 messages, latest: Aug 21 2023 at 14:12)
• PR #14350: refactor(linear_algebra/clifford_algebra): rel… (2 messages, latest: Aug 21 2023 at 14:07)
• issue #3088: Towards a more beginner-friendly tactic doc (23 messages, latest: Aug 21 2023 at 14:07)
• PR #14522: feat(algebra/module/submodule/lattice): `submo… (1 message, latest: Aug 20 2023 at 14:07)
• [PR #10205: Prove the solutions (and uniqueness of those s…](topic/PR.20.2310205.3A.20Prove.20the.20solutions.20(and.20uniqueness.20of.20those.20s.2E.2E.2E.html) (4 messages, latest: Aug 19 2023 at 14:08)
• issue #4973: Jordan-Chevalley decomposition (8 messages, latest: Aug 19 2023 at 14:07)
• [PR #17472: feat(ring_theory/local_properties): Being (in/…](topic/PR.20.2317472.3A.20feat(ring_theory.2Flocal_properties).3A.20Being.20(in.2F.2E.2E.2E.html) (2 messages, latest: Aug 18 2023 at 14:07)
• issue #3349: assoc_rw can leave side-goals as metavariables (19 messages, latest: Aug 18 2023 at 14:07)
• PR #15070: feat(model_theory/algebraic): add algebraic la… (2 messages, latest: Aug 17 2023 at 14:07)
• issue #14781: Approximation tactic (2 messages, latest: Aug 17 2023 at 14:07)
• [PR #15742: feat(topology/sheaves/): sheaves have enough …](topic/PR.20.2315742.3A.20feat(topology.2Fsheaves.2F).3A.20sheaves.20have.20enough.20.2E.2E.2E.html) (1 message, latest: Aug 16 2023 at 14:07)
• [issue #15053: Add an instance `{add_,}sub{monoid,group}c…](topic/issue.20.2315053.3A.20Add.20an.20instance.20.60.7Badd.2C.7Dsub.7Bmonoid.2Cgroup.7D_c.2E.2E.2E.html) (5 messages, latest: Aug 16 2023 at 14:07)
• issue #4709: Type vars in data/polynomial/splitting_field (6 messages, latest: Aug 15 2023 at 19:57)
• PR #15425: feat(tactic/polyrith): solve more problems by … (1 message, latest: Aug 15 2023 at 14:07)
• PR #18462: refactor(analysis/normed/group/basic): unbundl… (1 message, latest: Aug 14 2023 at 14:08)
• issue #1868: Tactic to transfer theorems / definitions us… (7 messages, latest: Aug 14 2023 at 14:08)
• issue #18010: (a :: l ++ \[b\]).last' does not simplify t… (4 messages, latest: Aug 13 2023 at 14:49)
• PR #16538: feat(data/list/rotate): rotate right (1 message, latest: Aug 13 2023 at 14:07)
• PR #17984: feat(counterexamples): non-normalizable gcd_mo… (2 messages, latest: Aug 12 2023 at 14:07)
• issue #4033: properties of (sub)modules (21 messages, latest: Aug 12 2023 at 14:07)
• PR #5829: feat(data/equiv/one_sided): Add bundled one-sid… (5 messages, latest: Aug 11 2023 at 14:43)
• issue #10954: Add an @[intuit] attribute or similar (9 messages, latest: Aug 11 2023 at 14:08)
• PR #17879: feat(number_theory/modular_forms): gcomm_ring … (5 messages, latest: Aug 10 2023 at 14:35)
• issue #13574: padic_norm file maintenance (4 messages, latest: Aug 10 2023 at 14:08)
• [PR #16040: feat(linear_algebra/clifford_algebra/spin_grou…](topic/PR.20.2316040.3A.20feat(linear_algebra.2Fclifford_algebra.2Fspin_grou.2E.2E.2E.html) (2 messages, latest: Aug 09 2023 at 14:13)
• PR #16774: feat(information_theory/linear_code): Define l… (1 message, latest: Aug 08 2023 at 14:07)
• issue #1260: documenting mathlib (16 messages, latest: Aug 08 2023 at 14:07)
• PR #15135: feat(order/complete_lattice_intervals): comple… (1 message, latest: Aug 07 2023 at 14:07)
• issue #15749: Remove has_coe_to_fun instance for `unita… (2 messages, latest: Aug 07 2023 at 14:07)
• [PR #18969: refactor(linear_algebra/): Rename `linear_equ…](topic/PR.20.2318969.3A.20refactor(linear_algebra.2F).3A.20Rename.20.60linear_equ.2E.2E.2E.html) (1 message, latest: Aug 06 2023 at 14:06)
• issue #8590: Test that the input .bib file is exactly t… (6 messages, latest: Aug 06 2023 at 14:06)
• issue #11388: Limits and continuity for real.logb (4 messages, latest: Aug 05 2023 at 14:06)
• PR #4739: feat(group_theory/perm/sign): Add `equiv.perm.m… (3 messages, latest: Aug 04 2023 at 14:07)
• PR #18776: feat(topology/noetherian_space): use `well_fou… (1 message, latest: Aug 03 2023 at 14:07)
• issue #3655: interval_cases for pnats does not work, … (6 messages, latest: Aug 03 2023 at 14:07)
• PR #14250: feat(computability): prove equivalence of NFAs… (3 messages, latest: Aug 02 2023 at 14:07)
• issue #4779: refine_struct: case tags not working? (9 messages, latest: Aug 01 2023 at 14:07)
• PR #14378: feat(algebra/order/digits): the digits of a li… (1 message, latest: Jul 31 2023 at 14:07)
• issue #2725: push_hom and pull_hom tactics (15 messages, latest: Jul 31 2023 at 14:07)
• PR #18640: feat(ring_theory/mv_polynomial/symmetric): sum… (1 message, latest: Jul 30 2023 at 14:06)
• PR #12795: feat(order/filter/archimedean): Generalize ten… (1 message, latest: Jul 29 2023 at 14:07)
• issue #17141: polyrith fails if expression is an equali… (1 message, latest: Jul 29 2023 at 14:07)
• issue #3975: remove the coercion from zmod n to other rings (15 messages, latest: Jul 29 2023 at 10:53)
• PR #18256: feat(group_theory/marking): Group markings (7 messages, latest: Jul 28 2023 at 14:06)
• PR #16415: feat(logic/encodable): Encoding of elements as… (1 message, latest: Jul 27 2023 at 14:07)
• issue #14993: apply' can close the goal with metavariables (2 messages, latest: Jul 27 2023 at 14:07)
• PR #15347: feat(tactic/polyrith): polyrith at h (2 messages, latest: Jul 26 2023 at 14:07)
• issue #18135: The Shapley-Folkman lemma (3 messages, latest: Jul 26 2023 at 14:07)
• PR #14067: feat(linear_algebra/basis): strictly triangula… (1 message, latest: Jul 25 2023 at 14:07)
• issue #11186: Make to_ring_hom_eq_coe into a simp lem… (6 messages, latest: Jul 25 2023 at 14:07)
• PR #18581: refactor(data/list/nat_antidiagonal): extend t… (2 messages, latest: Jul 24 2023 at 14:07)
• issue #11022: The long line (12 messages, latest: Jul 24 2023 at 14:07)
• PR #16449: feat(algebra/order/monoid_lemma_zero_lt): chan… (1 message, latest: Jul 23 2023 at 14:07)
• PR #15368: feat(order/initial_seg): initial and principal… (1 message, latest: Jul 22 2023 at 14:06)
• issue #12685: let linear_combination solve ≠ goals (4 messages, latest: Jul 22 2023 at 14:06)
• issue #18164: Tracking: attribute semireducible/irreducible (3 messages, latest: Jul 19 2023 at 14:07)
• issue #2910: Port convexity to affine spaces (9 messages, latest: Jul 18 2023 at 14:07)
• issue #1509: wlog (7 messages, latest: Jul 17 2023 at 14:07)
• PR #12933: feat(analysis/cauchy_equation): Add Cauchy's F… (6 messages, latest: Jul 16 2023 at 14:07)
• issue #2726: a multiplicative version of the abel tactic (9 messages, latest: Jul 15 2023 at 15:30)
• PR #15088: feat(algebra/cubic_discriminant): remove custo… (1 message, latest: Jul 14 2023 at 14:07)
• issue #2534: Get rid of is_(semi)ring_hom (11 messages, latest: Jul 14 2023 at 14:07)
• PR #8592: feat(group_theory/group_action/subgroup): Conju… (1 message, latest: Jul 13 2023 at 14:07)
• PR #4798: feat(analysis/normed_space/dual): dual inner pr… (9 messages, latest: Jul 12 2023 at 19:07)
• PR #17201: feat(data/int/gcd): Extended gcds involving 1 (2 messages, latest: Jul 11 2023 at 14:08)
• [PR #18838: feat(data//interval): finset.uIcc on concre…](topic/PR.20.2318838.3A.20feat(data.2F.2Finterval).3A.20.60finset.2EuIcc.60.20on.20concre.2E.2E.2E.html) (4 messages, latest: Jul 10 2023 at 14:07)
• issue #5489: @[simps] improvements (4 messages, latest: Jul 10 2023 at 14:07)
• PR #17608: feat(linear_algebra/matrix_group): introduce `… (1 message, latest: Jul 09 2023 at 14:07)
• issue #16386: Basics of tempered distributions (4 messages, latest: Jul 09 2023 at 14:07)
• PR #12514: feat(probability): define conditional independ… (1 message, latest: Jul 08 2023 at 14:08)
• issue #11407: Arithmetic of quadratic fields (7 messages, latest: Jul 08 2023 at 14:08)
• PR #18806: feat(analysis/convex/function): Product of con… (1 message, latest: Jul 07 2023 at 14:07)
• issue #7003: Add a user command to print the declarations… (7 messages, latest: Jul 07 2023 at 14:07)
• issue #1867: Rethink and document the import hierarchy … (9 messages, latest: Jul 05 2023 at 14:08)
• PR #17817: feat(analysis/normed/ring/seminorm): add `equi… (2 messages, latest: Jul 05 2023 at 14:07)
• PR #15476: feat(data/polynomial/of_list): polys formed by… (1 message, latest: Jul 04 2023 at 14:07)
• PR #18513: feat(set_theory/zfc/ordinal): definition of vo… (1 message, latest: Jul 03 2023 at 14:07)
• issue #5525: Unify (or at least connect) order_hom and … (3 messages, latest: Jul 03 2023 at 14:07)
• PR #10963: feat(combinatorics/graph): typeclasses for gra… (7 messages, latest: Jul 02 2023 at 14:07)
• issue #2367: interval_cases bugs (15 messages, latest: Jul 02 2023 at 03:12)
• PR #19203: feat(combinatorics/simple_graph): More clique … (2 messages, latest: Jul 01 2023 at 14:07)
• issue #7051: Predicate for Kan extensions (10 messages, latest: Jun 30 2023 at 21:16)
• issue #4616: Follow-ups from free_algebra, `exterior_al… (9 messages, latest: Jun 29 2023 at 14:07)
• PR #7707: fix(tactic/induction): fix generalisation with … (6 messages, latest: Jun 28 2023 at 14:07)
• PR #7093: feat(order/sublattice): sublattice definition (4 messages, latest: Jun 27 2023 at 14:08)
• issue #2730: computer algebra system style tactics? (10 messages, latest: Jun 26 2023 at 14:46)
• PR #17802: refactor(analysis/calculus/fderiv): use right … (1 message, latest: Jun 26 2023 at 14:07)
• PR #12313: feat(analysis/inner_product_space/adjoint): `o… (1 message, latest: Jun 25 2023 at 14:07)
• PR #14812: refactor(algebra/direct_sum/module): use `deco… (3 messages, latest: Jun 24 2023 at 14:07)
• PR #8516: refactor(data/matrix/basic): Remove matrix.scalar (5 messages, latest: Jun 23 2023 at 14:07)
• issue #1654: Replace manually defined extensionality lemm… (2 messages, latest: Jun 23 2023 at 14:07)
• issue #7626: Create has_antidiagonal class (10 messages, latest: Jun 22 2023 at 14:07)
• PR #3169: feat(ring_theory/mv_polynomial/symmetric): Symm… (4 messages, latest: Jun 21 2023 at 15:06)
• PR #18999: feat(order/irreducible): Sup-irreducible elements (2 messages, latest: Jun 20 2023 at 14:26)
• issue #4971: Jordan normal form (9 messages, latest: Jun 19 2023 at 14:06)
• PR #18967: chore(algebra/ring/defs): backport reordering … (1 message, latest: Jun 18 2023 at 14:07)
• issue #2409: Linter doc_blame generates unwanted warnin… (14 messages, latest: Jun 18 2023 at 14:07)
• PR #12345: feat(probability): define joint and marginal d… (7 messages, latest: Jun 17 2023 at 14:45)
• issue #15860: Pi is irrational (3 messages, latest: Jun 17 2023 at 14:07)
• issue #1484: unexpected failures with omega (11 messages, latest: Jun 16 2023 at 14:53)
• PR #7217: feat(data/finsupp/equiv_dfinsupp): add an equiv… (1 message, latest: Jun 16 2023 at 14:07)
• PR #18652: feat(field_theory/ratfunc): The numerator and … (2 messages, latest: Jun 15 2023 at 14:08)
• issue #7691: to_additive-like attribute for order_dual (9 messages, latest: Jun 15 2023 at 14:07)
• issue #1063: homological algebra (11 messages, latest: Jun 14 2023 at 14:07)
• [PR #12349: feat(): fun_like instances on subtypes](topic/PR.20.2312349.3A.20feat().3A.20fun_like.20instances.20on.20subtypes.html) (2 messages, latest: Jun 13 2023 at 14:06)
• PR #18454: feat(combinatorics/simple graph/connectivity):… (1 message, latest: Jun 12 2023 at 14:06)
• issue #15992: evaluate int.floor and int.fract with `… (6 messages, latest: Jun 12 2023 at 14:06)
• PR #18289: feat(linear_algebra/invariant_submodule): inva… (1 message, latest: Jun 11 2023 at 14:07)
• issue #4688: Unify char_zero with char_p (5 messages, latest: Jun 11 2023 at 14:07)
• PR #18275: fix(tactic/core): plug leaks from classical (3 messages, latest: Jun 10 2023 at 14:17)
• issue #1038: Implement computable real numbers (9 messages, latest: Jun 10 2023 at 14:07)
• PR #18066: chore(deprecated): delete deprecated folder (2 messages, latest: Jun 08 2023 at 14:07)
• issue #11571: Lipschitz embeddings into ℓ^∞ (6 messages, latest: Jun 08 2023 at 14:07)
• PR #17010: feat(src/ring_theory/is_tensor_product): Base … (2 messages, latest: Jun 07 2023 at 14:07)
• PR #12237: feat(tactic/interval_cases): faster implementa… (1 message, latest: Jun 06 2023 at 14:07)
• PR #18887: feat(analysis/specific_limits/complex) (1 message, latest: Jun 05 2023 at 14:07)
• PR #16645: chore(data/real/nnreal): make real.to_nnreal… (2 messages, latest: Jun 04 2023 at 14:06)
• PR #15614: feat(order/succ_pred/limit): predecessor from … (2 messages, latest: Jun 03 2023 at 14:07)
• PR #15168: feat(order/antisymm_incomp): move antisymmetri… (2 messages, latest: Jun 02 2023 at 14:07)
• PR #7834: wip(data/subtype_instances): introduce closed_u… (1 message, latest: Jun 01 2023 at 14:07)
• issue #1496: Merge 3 files about basic properties of rela… (13 messages, latest: Jun 01 2023 at 14:07)
• PR #18692: feat(combinatorics.simple_graph.metric): `enat… (1 message, latest: May 31 2023 at 14:06)
• issue #15565: Locally convex Hausdorff spaces (6 messages, latest: May 30 2023 at 14:06)
• PR #14494: feat(computability/timed): add complexity anal… (2 messages, latest: May 29 2023 at 14:07)
• PR #15849: feat(data/nat/basic): add_base_rec (2 messages, latest: May 28 2023 at 14:06)
• issue #3186: add nice VSCode settings (7 messages, latest: May 28 2023 at 14:06)
• PR #16574: feat (group_theory/amenable) : define amenable… (2 messages, latest: May 26 2023 at 18:47)
• issue #199: TODO: unify disjoint (8 messages, latest: May 26 2023 at 14:06)
• PR #13280: feat(analysis/locally_convex): weakly bounded … (1 message, latest: May 25 2023 at 14:07)
• PR #18865: chore(analysis/convex/combination): remove unn… (1 message, latest: May 24 2023 at 14:07)
• PR #14855: feat(order/upper_lower, order/hom/basic): Uppe… (2 messages, latest: May 23 2023 at 14:07)
• did the bot die? (1 message, latest: Apr 17 2023 at 23:06)
• PR #15047: feat(data/matrix/companion): Companion matrix (2 messages, latest: Apr 17 2023 at 22:57)
• PR #15732: feat(tactic/expand_exists): create in namespac… (1 message, latest: Mar 17 2023 at 14:09)
• issue #15566: Define Hermite polynomials (6 messages, latest: Mar 17 2023 at 14:09)
• PR #8496: refactor(order/conditionally_complete_lattice):… (5 messages, latest: Mar 16 2023 at 14:09)
• issue #10248: fin_cases for finsets not as versatile as m… (4 messages, latest: Mar 16 2023 at 14:09)
• PR #7803: feat(topology): continuous sections of a vector… (3 messages, latest: Mar 15 2023 at 14:08)
• issue #2724: have solve_by_elim call intro1 before gi… (8 messages, latest: Mar 14 2023 at 23:21)
• PR #17257: feat(analysis/normed/order/upper_lower): Thick… (4 messages, latest: Mar 14 2023 at 14:10)
• issue #3082: Hasse invariant of quadratic forms (9 messages, latest: Mar 13 2023 at 14:11)
• PR #18059: chore(ring_theory/ideal/operations): shave off… (1 message, latest: Mar 12 2023 at 14:09)
• PR #10151: chore(data/equiv/transfer_instance): avoid `le… (2 messages, latest: Mar 11 2023 at 14:09)
• issue #13506: convert is_monoid_hom etc to structures, … (4 messages, latest: Mar 11 2023 at 14:09)
• PR #7652: feat(tactic/frozen): add tactics about frozen l… (5 messages, latest: Mar 10 2023 at 14:09)
• issue #3273: squeeze_simp also simplify targets (8 messages, latest: Mar 10 2023 at 14:09)
• PR #11609: feat(bors.toml): let bors wait for PRs to be g… (3 messages, latest: Mar 09 2023 at 14:09)
• PR #18179: feat(linear_algebra/clifford): make clifford_a… (4 messages, latest: Mar 08 2023 at 14:54)
• issue #9945: to_additive guesses a bad name in some edg… (7 messages, latest: Mar 07 2023 at 14:08)
• PR #17275: feat(analysis/locally_convex/with_seminorms): … (2 messages, latest: Mar 06 2023 at 14:51)
• issue #17919: Q: LLM and/or an RL agent trained on mathli… (5 messages, latest: Mar 05 2023 at 14:45)
• [PR #16340: chore(): remove is_absolute_value](topic/PR.20.2316340.3A.20chore().3A.20remove.20is_absolute_value.html) (1 message, latest: Mar 05 2023 at 14:09)
• issue #4013: properties of ring homomorphisms (17 messages, latest: Mar 04 2023 at 14:09)
• PR #6799: chore(analysis/normed_space/inner_product): euc… (4 messages, latest: Mar 01 2023 at 14:09)
• PR #13418: feat(category_theory/bicategory/adjunction): a… (1 message, latest: Feb 28 2023 at 14:09)
• issue #1847: Write a tactic to copy a structure while upd… (3 messages, latest: Feb 28 2023 at 14:09)
• PR #14916: feat(data/polynomial/root_isolation): root_par… (1 message, latest: Feb 27 2023 at 14:08)
• PR #13675: refactor(topology/metric_space/basic): migrate… (2 messages, latest: Feb 26 2023 at 14:09)
• issue #2268: caching olean files on a per file basis (5 messages, latest: Feb 25 2023 at 14:14)
• PR #18374: chore(analysis/inner_product_space/basic): red… (1 message, latest: Feb 25 2023 at 14:09)
• PR #15412: feat(set_theory/cardinal/basic): `#α ≤ ℵ₀ ↔ co… (1 message, latest: Feb 24 2023 at 14:08)
• issue #1858: Define Banach algebras (10 messages, latest: Feb 23 2023 at 14:08)
• PR #10716: feat(algebra/algebra/basic): Algebras are bimo… (2 messages, latest: Feb 22 2023 at 14:08)
• PR #18138: feat(proj construction) (1 message, latest: Feb 21 2023 at 14:09)
• PR #16231: feat(data/nat/factorization/basic): lemmas abo… (1 message, latest: Feb 20 2023 at 14:09)
• PR #11233: feat (group_theory/perm/cycle_type) : add form… (4 messages, latest: Feb 19 2023 at 14:08)
• PR #7498: feat(combinatorics/simple_graph/inc_matrix): Or… (2 messages, latest: Feb 18 2023 at 14:08)
• PR #10119: feat(ring_theory/graded_algebra): `mv_polynomi… (4 messages, latest: Feb 17 2023 at 14:09)
• PR #9626: feat(analysis/conformal/inner_product_space): t… (4 messages, latest: Feb 16 2023 at 14:09)
• issue #15723: expand_exists improvements (4 messages, latest: Feb 16 2023 at 14:09)
• PR #6514: chore(group_theory/submonoid/operations): use c… (2 messages, latest: Feb 14 2023 at 14:09)
• PR #16338: feat(analysis/convex/body): endow with Hausdor… (2 messages, latest: Feb 13 2023 at 14:08)
• PR #18148: feat(representation_theory/Rep): describe mono… (2 messages, latest: Feb 13 2023 at 05:49)
• PR #10712: feat(logic/indexed_eq): Indexed equality (1 message, latest: Feb 11 2023 at 14:08)
• PR #14315: feat(topology/metric_space/dilation): Dilation… (1 message, latest: Feb 10 2023 at 14:09)
• PR #17654: feat(combinatorics/simple_graph/connectivity):… (2 messages, latest: Feb 09 2023 at 14:09)
• PR #16656: chore(analysis/special_functions/pow): change … (2 messages, latest: Feb 07 2023 at 16:12)
• PR #17973: feat(algebra/module/localized_module): add is_… (1 message, latest: Feb 06 2023 at 14:09)
• issue #6123: ext recurses into subgoals, ext x y z an… (10 messages, latest: Feb 06 2023 at 14:09)
• [PR #17949: refactor(algebra/star/): Allow for star opera…](topic/PR.20.2317949.3A.20refactor(algebra.2Fstar.2F).3A.20Allow.20for.20star.20opera.2E.2E.2E.html) (2 messages, latest: Feb 04 2023 at 14:22)
• PR #18165: chore(scripts/list-attributes.sh): script to t… (1 message, latest: Feb 02 2023 at 14:09)
• PR #13862: feat(ring_theory/ideal/nc_jacobson_radical): J… (2 messages, latest: Jan 31 2023 at 14:09)
• PR #14694: refactor(topology): drop uniformity (2 messages, latest: Jan 30 2023 at 14:09)
• PR #17142: fix(tactic/polyrith): fix crash when hypothese… (3 messages, latest: Jan 29 2023 at 16:08)
• PR #10255: feat(linear_algebra/tensor_power): the tensor … (7 messages, latest: Jan 29 2023 at 14:46)
• PR #17921: feat(category_theory/idempotents): idempotent … (1 message, latest: Jan 27 2023 at 14:09)
• PR #9692: refactor(algebra/star): replace star_ring_aut… (3 messages, latest: Jan 26 2023 at 14:08)
• PR #14870: feat(analysis/inner_product_space/spectrum): a… (1 message, latest: Jan 25 2023 at 14:08)
• issue #1142: Etale cohomology (10 messages, latest: Jan 24 2023 at 16:14)
• [PR #17006: feat(category_theory/): Monoid objects in Abe…](topic/PR.20.2317006.3A.20feat(category_theory.2F).3A.20Monoid.20objects.20in.20Abe.2E.2E.2E.html) (1 message, latest: Jan 23 2023 at 14:08)
• PR #13937: WIP(analysis/convolution): Define convolution … (2 messages, latest: Jan 22 2023 at 14:08)
• issue #2016: Formal roadmaps need to be explained and doc… (5 messages, latest: Jan 22 2023 at 14:08)
• PR #17886: chore(data/finset/image): reduce imports (1 message, latest: Jan 21 2023 at 14:08)
• [PR #8196: feat(topology/{extremally_disconnected, stone_c…](topic/PR.20.238196.3A.20feat(topology.2F.7Bextremally_disconnected.2C.20stone_c.2E.2E.2E.html) (5 messages, latest: Jan 20 2023 at 14:08)
• issue #3120: a non-interactive version of squeeze_simp,… (5 messages, latest: Jan 19 2023 at 14:09)
• [PR #17164: feat(analysis/normed_space/star/continuous_fun…](topic/PR.20.2317164.3A.20feat(analysis.2Fnormed_space.2Fstar.2Fcontinuous_fun.2E.2E.2E.html) (1 message, latest: Jan 18 2023 at 14:09)
• PR #11771: feat(computability/partrec_arity): partial rec… (2 messages, latest: Jan 17 2023 at 14:08)
• issue #5659: suggest and show_term give incorrect suggest… (5 messages, latest: Jan 16 2023 at 14:08)
• issue #5901: simp? and squeeze_simp (11 messages, latest: Jan 15 2023 at 14:12)
• PR #3515: feat(data/dfinsupp): Add an equivalence between… (7 messages, latest: Jan 15 2023 at 14:08)
• PR #6887: feat(analysis/special_functions/pow): Add Berno… (4 messages, latest: Jan 14 2023 at 14:09)
• PR #13500: uniform_limit_of_holo_is_holo (4 messages, latest: Jan 13 2023 at 14:30)
• issue #10696: @\[mk_iff\] causes a type error (3 messages, latest: Jan 13 2023 at 14:09)
• PR #6045: refactor(algebra/group/type_tags): make additiv… (1 message, latest: Jan 12 2023 at 14:10)
• issue #16932: Diamond of complete boolean algebras on sets (1 message, latest: Jan 12 2023 at 14:10)
• PR #14863: refactor(order/complete_lattice): ditch `compl… (1 message, latest: Jan 11 2023 at 14:09)
• PR #10632: feat(geometry/euclidean/ceva) : Ceva's Theorem… (5 messages, latest: Jan 10 2023 at 14:08)
• PR #17291: feat(geometry/manifold/cont_mdiff): local stru… (1 message, latest: Jan 09 2023 at 14:09)
• PR #11000: feat(combinatorics/graph/basic): Graph hierarc… (5 messages, latest: Jan 08 2023 at 14:08)
• PR #17302: feat(geometry/manifold/vector_bundle): `smooth… (2 messages, latest: Jan 08 2023 at 13:31)
• issue #11523: Develop basic theory of integrally closed d… (3 messages, latest: Jan 07 2023 at 16:21)
• PR #15910: feat(data/multiset/basic): more basic lemmas o… (1 message, latest: Jan 06 2023 at 14:09)
• issue #1539: Improve dense_embedding documentation (10 messages, latest: Jan 06 2023 at 14:09)
• PR #5891: feat(combinatorics/simple_graph/basic): add edg… (6 messages, latest: Jan 05 2023 at 14:12)
• PR #9828: feat(group_theory): class equation for finite g… (5 messages, latest: Jan 04 2023 at 14:08)
• issue #17919: Q: ChatGPT etc. trained on mathlib and tests (2 messages, latest: Jan 04 2023 at 00:44)
• PR #17483: feat(algebra/group/basic): add some lemmas on … (1 message, latest: Jan 03 2023 at 14:08)
• PR #11364: feat(algebra/char_p/basic): refactor proof of … (1 message, latest: Jan 02 2023 at 14:08)
• PR #13791: refactor(algebra/monoid_algebra): remove simp … (2 messages, latest: Dec 31 2022 at 14:08)
• PR #14228: chore(various files): move_add-driven acts o… (1 message, latest: Dec 30 2022 at 14:08)
• issue #2179: Define exact sequences (11 messages, latest: Dec 28 2022 at 14:08)
• PR #17653: feat(ring_theory/integral_domain): generalize … (1 message, latest: Dec 27 2022 at 14:08)
• PR #17939: feat(order/locally_finite): finset.interval (2 messages, latest: Dec 26 2022 at 14:09)
• PR #15954: feat(analysis/transcendental): e is transcende… (2 messages, latest: Dec 25 2022 at 14:09)
• PR #16998: feat(ring_theory/zmod): add criterion for zmod… (1 message, latest: Dec 24 2022 at 14:08)
• issue #10704: partial_order.lift vs `function.injective… (2 messages, latest: Dec 24 2022 at 14:08)
• PR #17012: feat(data/finsupp/basic): Lemmas regarding `fi… (2 messages, latest: Dec 22 2022 at 14:13)
• issue #3533: document derive / derive_handler attributes (4 messages, latest: Dec 22 2022 at 14:09)
• PR #16983: feat(geometry/manifold/cont_mdiff_mfderiv): mo… (1 message, latest: Dec 21 2022 at 14:09)
• PR #17426: feat(topology/order/lower_topology): Introduce… (1 message, latest: Dec 20 2022 at 14:08)
• PR #17081: feat(analysis/convex/continuous): Convex funct… (4 messages, latest: Dec 19 2022 at 08:28)
• PR #15171: chore(topology/algebra/group): generalise inst… (1 message, latest: Dec 17 2022 at 14:08)
• PR #17200: feat(tactic/abel): separate out abel_nf (1 message, latest: Dec 16 2022 at 14:08)
• PR #17715: feat(analysis/normed_space/compact_operator): … (1 message, latest: Dec 15 2022 at 14:08)
• PR #15289: chore(set_theory/game/pgame): golf le and `l… (1 message, latest: Dec 14 2022 at 14:08)
• [✔ PR #11545: WIP feat(): define subobject classes up to …](topic/.E2.9C.94.20PR.20.2311545.3A.20WIP.20feat().3A.20define.20subobject.20classes.20up.20to.20.2E.2E.2E.html) (3 messages, latest: Dec 13 2022 at 14:32)
• PR #6485: Add a linter for incorrectly used decidable arg… (33 messages, latest: Dec 12 2022 at 14:08)
• PR #10645: feat(combinatorics/additive/small_roth): Small… (7 messages, latest: Dec 11 2022 at 17:40)
• PR #17249: feat(analysis/seminorm): characterize continui… (2 messages, latest: Dec 10 2022 at 17:18)
• issue #1465: Probably setup_tactic_parser can be integr… (17 messages, latest: Dec 07 2022 at 22:04)
• PR #12992: feat(algebra/parity): Squares and primality (1 message, latest: Dec 07 2022 at 14:09)
• [PR #17643: feat(linear_algebra/affine_space/finite_dimens…](topic/PR.20.2317643.3A.20feat(linear_algebra.2Faffine_space.2Ffinite_dimens.2E.2E.2E.html) (1 message, latest: Dec 04 2022 at 14:08)
• issue #2710: More on quotients of categories (8 messages, latest: Dec 04 2022 at 14:08)
• PR #13412: feat(topology/algebra/affine): define topologi… (1 message, latest: Dec 03 2022 at 14:08)
• PR #15260: feat(set_theory/game/pgame): small sets of pre… (1 message, latest: Dec 01 2022 at 14:08)
• PR #10683: feat(geometry/manifold): The preimage straight… (2 messages, latest: Nov 30 2022 at 14:09)
• PR #17525: feat(geometry/euclidean/angle/oriented/basic):… (1 message, latest: Nov 29 2022 at 14:08)
• PR #17055: feat(group_theory/group_action/support): Suppo… (1 message, latest: Nov 28 2022 at 14:08)
• PR #17590: feat(measure_theory/group/action): `smul_invar… (1 message, latest: Nov 27 2022 at 14:08)
• PR #16997: feat(algebra/ring/divisibility): add sub versi… (1 message, latest: Nov 26 2022 at 14:09)
• PR #15681: feat(topology/homotopy/homotopy_group): `group… (1 message, latest: Nov 24 2022 at 14:08)
• PR #10254: feat(tactic/declare): canonical declarations (2 messages, latest: Nov 23 2022 at 14:08)
• PR #15179: feat(order/rel_iso): well_founded_lt instanc… (1 message, latest: Nov 20 2022 at 14:07)
• PR #16760: refactor(algebra/opposites): remove irreducibl… (1 message, latest: Nov 19 2022 at 14:07)
• PR #15901: feat(data/mv_polynomial/pi): `exists_smodeq_of… (1 message, latest: Nov 17 2022 at 14:08)
• PR #4348: feat(order/omega-cpo): cpos form a cartesian cl… (3 messages, latest: Nov 16 2022 at 14:08)
• PR #16820: feat(algebra/category/Group/injective): Prereq… (1 message, latest: Nov 15 2022 at 14:07)
• PR #11807: feat(algebra/category/Module/monoidal): Genera… (1 message, latest: Nov 13 2022 at 14:07)
• [PR #15592: feat(combinatorics/hales_jewett, combinatorics…](topic/PR.20.2315592.3A.20feat(combinatorics.2Fhales_jewett.2C.20combinatorics.2E.2E.2E.html) (1 message, latest: Nov 12 2022 at 14:07)
• PR #6418: feat(algebra/group_with_zero): add lemmas about… (3 messages, latest: Nov 11 2022 at 14:09)
• PR #5719: feat(meta): Assignable datatypes and expression… (4 messages, latest: Nov 10 2022 at 14:16)
• PR #15760: feat(number_theory/prime_counting): Tochiori l… (2 messages, latest: Nov 09 2022 at 14:12)
• [PR #16454: feat(data/finsupp/defs, algebra/big_operators/…](topic/PR.20.2316454.3A.20feat(data.2Ffinsupp.2Fdefs.2C.20algebra.2Fbig_operators.2F.2E.2E.2E.html) (1 message, latest: Nov 06 2022 at 14:17)
• PR #8737: feat(combinatorics/simple_graph): connectivity (1 message, latest: Nov 05 2022 at 14:16)
• PR #11352: feat(data/sum/interval): The lexicographic sum… (2 messages, latest: Nov 04 2022 at 14:17)
• PR #13917: feat(set_theory/game/basic): Golf using `antis… (1 message, latest: Nov 03 2022 at 14:22)
• PR #8475: feat(order/compactly_generated): For any b, t… (1 message, latest: Nov 02 2022 at 14:26)
• [PR #11985: feat(): add additive versions of `is_central_…](topic/PR.20.2311985.3A.20feat().3A.20add.20additive.20versions.20of.20.60is_central_.2E.2E.2E.html) (1 message, latest: Nov 01 2022 at 14:26)
• PR #6954: feat(archive/imo): add 2014 Q1 (2 messages, latest: Oct 30 2022 at 14:18)
• PR #15915: refactor(linear_algebra/smodeq): Relax smodeq … (2 messages, latest: Oct 29 2022 at 14:19)
• PR #15927: feat(order/order_iso_nat): value is accessible… (1 message, latest: Oct 28 2022 at 14:27)
• issue #161: Change list.prod from foldl to foldr (9 messages, latest: Oct 28 2022 at 14:27)
• PR #15547: feat(set_theory/zfc/basic): intersection of fa… (1 message, latest: Oct 27 2022 at 14:29)
• PR #14809: feat(order/has_involution): Types with antiton… (2 messages, latest: Oct 26 2022 at 14:26)
• PR #16965: feat(data/{finset,set}/basic): A nonempty set … (2 messages, latest: Oct 24 2022 at 15:16)
• [PR #7904: feat(order/basic, algebra/ordered_monoid_lemmas…](topic/PR.20.237904.3A.20feat(order.2Fbasic.2C.20algebra.2Fordered_monoid_lemmas.2E.2E.2E.html) (2 messages, latest: Oct 22 2022 at 18:20)
• PR #8979: Modular forms (4 messages, latest: Oct 21 2022 at 19:50)
• issue #2880: integrate noncomm_ring and ring (2 messages, latest: Oct 20 2022 at 14:38)
• PR #11046: Complexity Theory (1 message, latest: Oct 19 2022 at 14:36)
• PR #15990: feat(set_theory/ordinal/arithmetic): miscellan… (1 message, latest: Oct 18 2022 at 14:35)
• PR #15949: feat(ring_theory/finiteness): A morphism is fi… (5 messages, latest: Oct 16 2022 at 14:43)
• PR #16087: feat(topology/covering): Define covering spaces (2 messages, latest: Oct 15 2022 at 15:55)
• issue #5518: "simp normal form" should be documented (9 messages, latest: Oct 13 2022 at 14:29)
• PR #5569: feat(algebra/module/submodule): merge smul_mem … (2 messages, latest: Oct 12 2022 at 14:39)
• PR #4059: feat(category_theory/monoidal): Strong functor (2 messages, latest: Oct 09 2022 at 14:21)
• PR #6244: feat(data/fin/tuple): lemmas about append (1 message, latest: Oct 08 2022 at 14:23)
• PR #3770: feat(group/perm/sign): swap_adj_induction_on (8 messages, latest: Oct 07 2022 at 14:36)
• issue #4336: ext on structures should use `subsingleton… (8 messages, latest: Oct 06 2022 at 14:37)
• PR #11716: feat(topology/lindelof): define Lindelöf space (3 messages, latest: Oct 04 2022 at 14:39)
• PR #13566: feat(analysis/normed_space/multilinear): parti… (1 message, latest: Oct 03 2022 at 14:38)
• issue #15669: Connected components are open, under suitab… (3 messages, latest: Oct 02 2022 at 14:27)
• PR #8103: feat(geometry/manifold/curves): smooth curves (3 messages, latest: Oct 01 2022 at 14:21)
• issue #2601: Linear programming (12 messages, latest: Oct 01 2022 at 14:21)
• PR #15141: feat(probability/subgaussian): define sub-Gaus… (1 message, latest: Sep 30 2022 at 14:36)
• issue #10802: Stars and bars (10 messages, latest: Sep 29 2022 at 14:29)
• [PR #11677: feat(order/category/): Lattice categories](topic/PR.20.2311677.3A.20feat(order.2Fcategory.2F).3A.20Lattice.20categories.html) (1 message, latest: Sep 27 2022 at 14:34)
• PR #4406: feat(data/tuple): homogeneous tuples based on `… (4 messages, latest: Sep 26 2022 at 14:33)
• issue #2553: Quadratic forms over Q_p (14 messages, latest: Sep 26 2022 at 14:33)
• [PR #15491: feat(combinatorics/set_family/compression/basi…](topic/PR.20.2315491.3A.20feat(combinatorics.2Fset_family.2Fcompression.2Fbasi.2E.2E.2E.html) (2 messages, latest: Sep 25 2022 at 16:06)
• issue #408: transporting definitions and theorems along i… (43 messages, latest: Sep 25 2022 at 14:18)
• PR #16525: chore(algebra/order/monoid_lemmas_zero_lt): re… (1 message, latest: Sep 24 2022 at 14:17)
• PR #15552: feat(set_theory/zfc/ordinal): basic results on… (1 message, latest: Sep 21 2022 at 14:29)
• issue #5504: to_additive should raise an error if the ori… (2 messages, latest: Sep 19 2022 at 14:35)
• PR #10409: feat(data/list/basic): add filter/remove_all l… (2 messages, latest: Sep 19 2022 at 14:25)
• PR #16437: feat(group_theory/commutator): Add `commutator… (2 messages, latest: Sep 18 2022 at 15:26)
• issue #1654: clean up usages of ext (11 messages, latest: Sep 18 2022 at 14:14)
• PR #16267: feat(order/bounded_order): The lattice of comp… (1 message, latest: Sep 16 2022 at 14:25)
• PR #15532: chore(set_theory/ordinal/arithmetic): move the… (1 message, latest: Sep 14 2022 at 14:24)
• PR #4579: feat(tactic/chain_trans): prove inequalities by… (5 messages, latest: Sep 13 2022 at 14:23)
• PR #6259: chore(data/subtype): add heq_of_coe_eq ext lemma (4 messages, latest: Sep 12 2022 at 14:22)
• PR #16276: feat(algebraic_topology/simplex_category): str… (1 message, latest: Sep 11 2022 at 14:14)
• PR #14399: feat(ring_theory/ideal/basic): define right id… (1 message, latest: Sep 10 2022 at 14:14)
• PR #7065: feat(analysis/special_functions/integrals): int… (5 messages, latest: Sep 09 2022 at 14:22)
• PR #7436: feat(category_theory/concrete): representably c… (3 messages, latest: Sep 06 2022 at 14:18)
• PR #15041: refactor(set_theory/cardinal/basic): constrain… (1 message, latest: Sep 05 2022 at 14:17)
• PR #16168: feat(data/set/intervals/unordered_interval): I… (2 messages, latest: Sep 04 2022 at 14:28)
• PR #3638: feat(data/qpf): extend the theory of qpfs to su… (4 messages, latest: Sep 03 2022 at 14:14)
• PR #15996: feat(algebraic_geometry): `exists_pow_mul_eq_… (1 message, latest: Sep 01 2022 at 14:14)
• [PR #9623: feat(analysis/normed_space/conformal_linear_map…](topic/PR.20.239623.3A.20feat(analysis.2Fnormed_space.2Fconformal_linear_map.2E.2E.2E.html) (3 messages, latest: Aug 29 2022 at 14:15)
• PR #12842: feat(algebra/order/floor): Generalize floor le… (2 messages, latest: Aug 28 2022 at 16:21)
• PR #15464: feat(group_theory): Groups of order p^2 are ab… (4 messages, latest: Aug 28 2022 at 08:11)
• PR #15408: feat(set_theory/game/nim): recursors for left/… (1 message, latest: Aug 27 2022 at 14:13)
• PR #16074: feat(number_theory/padics/padic_norm): add int… (1 message, latest: Aug 25 2022 at 14:14)
• issue #16021: Lean is unable to infer ordered_smul inst… (2 messages, latest: Aug 24 2022 at 14:25)
• PR #14769: feat(probability/tail_prob): the tail probabil… (1 message, latest: Aug 24 2022 at 14:13)
• PR #11444: chore(analysis/calculus/fderiv_symmetric): spl… (1 message, latest: Aug 20 2022 at 14:13)
• PR #14659: feat(set_theory/game/pgame): notation and basi… (1 message, latest: Aug 19 2022 at 14:14)
• [PR #11759: refactor(): remove duplicate subobject instances](topic/PR.20.2311759.3A.20refactor().3A.20remove.20duplicate.20subobject.20instances.html) (1 message, latest: Aug 18 2022 at 14:16)
• PR #9843: feat(algebra/group/conj): conjugacy class as fi… (1 message, latest: Aug 17 2022 at 14:19)
• PR #12587: feat(algebra/ring/basic): lemmas about oddness… (2 messages, latest: Aug 16 2022 at 17:55)
• PR #14734: refactor(algebra/module/dedekind_domain): elim… (1 message, latest: Aug 15 2022 at 14:16)
• [PR #15206: chore(): golf and tidy some proofs](topic/PR.20.2315206.3A.20chore().3A.20golf.20and.20tidy.20some.20proofs.html) (1 message, latest: Aug 14 2022 at 14:13)
• PR #11376: feat(ring_theory/dedekind_finite): add materia… (1 message, latest: Aug 13 2022 at 14:13)
• PR #5179: feat(linear_algebra/multilinear-tensor): Add `m… (5 messages, latest: Aug 12 2022 at 14:14)
• [PR #15159: feat(number_theory/modular_forms/congruence_su…](topic/PR.20.2315159.3A.20feat(number_theory.2Fmodular_forms.2Fcongruence_su.2E.2E.2E.html) (1 message, latest: Aug 09 2022 at 14:18)
• [PR #14534: feat(topology/uniform_space/uniform_convergenc…](topic/PR.20.2314534.3A.20feat(topology.2Funiform_space.2Funiform_convergenc.2E.2E.2E.html) (2 messages, latest: Aug 08 2022 at 14:42)
• PR #8399: feat(archive): mccune axiom defines groups (4 messages, latest: Aug 07 2022 at 14:13)
• PR #15071: refactor(order/well_founded): ditch `well_foun… (2 messages, latest: Aug 06 2022 at 16:46)
• issue #14902: Composition of convex functions (2 messages, latest: Aug 06 2022 at 14:43)
• PR #10830: feat(algebraic_geometry): descent theorem (1 message, latest: Aug 05 2022 at 14:15)
• PR #13240: feat(data/polynomial/zcoeff): define zcoeff + API (2 messages, latest: Aug 04 2022 at 14:23)
• PR #15644: feat(algebra/order/with_zero): Add eq_one_of_m… (1 message, latest: Aug 02 2022 at 14:14)
• PR #14382: feat(analysis/analytic/isolated_zeros): princi… (1 message, latest: Aug 01 2022 at 14:16)
• PR #15233: refactor(set_theory/cardinal/basic): `enat.car… (2 messages, latest: Jul 31 2022 at 17:56)
• issue #1046: Expand the surreals library (7 messages, latest: Jul 30 2022 at 21:22)
• PR #12312: feat(analysis/inner_product_space/sqrt): `is_s… (2 messages, latest: Jul 29 2022 at 14:13)
• PR #15550: feat(set_theory/zfc/basic): pSet with empty … (4 messages, latest: Jul 29 2022 at 06:56)
• PR #14335: feat(data/sign): Allocating signs (1 message, latest: Jul 27 2022 at 14:15)
• PR #10643: feat(data/set_like/basic): add a congr lemma (1 message, latest: Jul 25 2022 at 14:15)
• PR #11468: feat(linear_algebra/clifford_algebra): the cli… (1 message, latest: Jul 24 2022 at 14:12)
• PR #14807: feat(order/interval): Order intervals (1 message, latest: Jul 21 2022 at 14:14)
• PR #9056: feat(group_theory/nilpotent): add lemma on quot… (4 messages, latest: Jul 20 2022 at 14:15)
• PR #11553: feat(algebra/jordan/triple): Introduce Jordan … (2 messages, latest: Jul 19 2022 at 14:14)
• PR #12900: feat(order/hom/lattice): Map lattice homs alon… (1 message, latest: Jul 18 2022 at 14:22)
• [PR #13200: feat(ring_theory/polynomial/special_coefficien…](topic/PR.20.2313200.3A.20feat(ring_theory.2Fpolynomial.2Fspecial_coefficien.2E.2E.2E.html) (1 message, latest: Jul 17 2022 at 14:13)
• PR #10346: feat(data/fin/tuple): rename fin.append to `… (2 messages, latest: Jul 16 2022 at 14:13)
• PR #11932: feat(order/sup_indep): More lemmas (2 messages, latest: Jul 14 2022 at 14:18)
• PR #14923: fix(algebra/group/units): splitting out `mul_o… (1 message, latest: Jul 12 2022 at 14:23)
• issue #14275: Create library note explaining seemingly re… (1 message, latest: Jun 30 2022 at 14:19)
• PR #12497: refactor(analysis/inner_product_space/pi_L2): … (2 messages, latest: Jun 29 2022 at 14:18)
• PR #13726: definition of triangle_free_far in terms of ed… (2 messages, latest: Jun 28 2022 at 14:19)
• issue #11682: command to unpack an existential with `clas… (2 messages, latest: Jun 28 2022 at 14:19)
• PR #9121: feat(algebra/big_operators/finprod): assorted l… (1 message, latest: Jun 27 2022 at 14:22)
• issue #2109: nonneg_of_mul_nonpos_right and `nonneg_of_… (8 messages, latest: Jun 26 2022 at 23:56)
• PR #10562: feat(data/bool): bnot_ne (3 messages, latest: Jun 26 2022 at 14:18)
• PR #12812: feat(ring_theory/integrally_closed): if x is i… (2 messages, latest: Jun 24 2022 at 14:18)
• PR #14072: feat(set_theory/ordinal/notation): fast growin… (5 messages, latest: Jun 22 2022 at 18:56)
• PR #10865: feat(order/atoms): A set/finset/multiset is an… (1 message, latest: Jun 20 2022 at 14:19)
• [PR #7020: feat(geometry/manifold/): transferring geometr…](topic/PR.20.237020.3A.20feat(geometry.2Fmanifold.2F).3A.20transferring.20geometr.2E.2E.2E.html) (5 messages, latest: Jun 12 2022 at 14:18)
• PR #12254: feat(number_theory/miller_rabin): adding lemma… (2 messages, latest: Jun 11 2022 at 14:18)
• issue #1462: Why are sheaves, sheaves? (5 messages, latest: Jun 11 2022 at 14:18)
• PR #11656: feat(algebra/incidence): Incidence algebras (3 messages, latest: Jun 08 2022 at 18:03)
• issue #4985: Avoid restating multiplicatively many `foo_h… (8 messages, latest: Jun 07 2022 at 14:20)
• PR #14044: feat(algebraic_topology/dold_kan): technical l… (1 message, latest: Jun 06 2022 at 14:18)
• PR #10345: feat(linear_algebra/tensor_product): Generalis… (1 message, latest: Jun 05 2022 at 14:18)
• PR #1083: feat(tactic/vampire): interface with Vampire (7 messages, latest: Jun 03 2022 at 14:18)
• PR #5924: chore(data/dfinsupp): Add sum_hom (5 messages, latest: Jun 02 2022 at 14:24)
• PR #12301: refactor(data/nat/factorization): Change defin… (2 messages, latest: May 30 2022 at 14:21)
• PR #3748: WIP: new datatype compiler (5 messages, latest: May 29 2022 at 14:20)
• PR #14030: feat(category_theory/limits): the image of a c… (1 message, latest: May 25 2022 at 14:32)
• [PR #8919: refactor(field_theory/): generalize subfields …](topic/PR.20.238919.3A.20refactor(field_theory.2F).3A.20generalize.20subfields.20.2E.2E.2E.html) (2 messages, latest: May 21 2022 at 15:16)
• PR #12253: refactor(analysis/inner_product_space/pi_L2): … (1 message, latest: May 20 2022 at 14:20)
• issue #1117: RFC: turn mul_action into a structure (12 messages, latest: May 20 2022 at 14:20)
• PR #12964: feat(topology/bornology/order): complete latti… (1 message, latest: May 18 2022 at 14:24)
• PR #2819: feat(number_theory/geometry_of_numbers): Minkow… (2 messages, latest: May 17 2022 at 14:32)
• PR #13480: feat(analysis/convex/uniform): Uniformly conve… (2 messages, latest: May 16 2022 at 14:33)
• issue #1097: transport a monoidal structure across an equ… (3 messages, latest: May 15 2022 at 23:18)
• PR #8632: feat(group_theory/p_group): Groups of order p^2… (11 messages, latest: May 15 2022 at 16:07)
• PR #8054: chore(linear_algebra): make linear_map extend d… (3 messages, latest: May 13 2022 at 16:08)
• issue #3532: tfae with named statements (4 messages, latest: May 12 2022 at 14:22)
• PR #4716: chore(category_theory/limits/preserves): preser… (15 messages, latest: May 09 2022 at 14:20)
• issue #2273: Infix notation for is_O / is_o (3 messages, latest: May 08 2022 at 14:20)
• issue #1924: New linters (8 messages, latest: May 06 2022 at 15:56)
• PR #11303: refactor(order/well_founded_set): golf, review… (3 messages, latest: May 06 2022 at 12:22)
• PR #11782: feat(algebra/order/monoid_lemmas_pos): use `co… (4 messages, latest: May 05 2022 at 17:10)
• issue #12666: Integrability on intervals via exhausting t… (1 message, latest: May 03 2022 at 14:18)
• [PR #12009: feat(data/{polynomial, mv_polynomial}/schwartz…](topic/PR.20.2312009.3A.20feat(data.2F.7Bpolynomial.2C.20mv_polynomial.7D.2Fschwartz.2E.2E.2E.html) (1 message, latest: May 02 2022 at 14:20)
• PR #12118: feat(topology/algebra/module/locally_convex): … (1 message, latest: Apr 30 2022 at 14:19)
• PR #11073: feat(algebra/jordan): Introduce Jordan rings (1 message, latest: Apr 29 2022 at 14:20)
• PR #7891: feat(algebra/ordered_{field, group}): lemmas ab… (10 messages, latest: Apr 26 2022 at 13:13)
• PR #12310: feat(group_theory/torsion): Q/Z and Fq[X] are … (3 messages, latest: Apr 23 2022 at 15:28)
• PR #13067: feat(ring_theory/dedekind_domain): Chinese rem… (1 message, latest: Apr 21 2022 at 14:20)
• [PR #11545: WIP feat(): define subobject classes up to `s…](topic/PR.20.2311545.3A.20WIP.20feat().3A.20define.20subobject.20classes.20up.20to.20.60s.2E.2E.2E.html) (1 message, latest: Apr 18 2022 at 14:13)
• PR #12895: feat(algebra/module): add injective module and… (1 message, latest: Apr 15 2022 at 14:14)
• PR #11606: feat(tactic/lint): adding a new linter for iff's (13 messages, latest: Apr 12 2022 at 12:12)
• [PR #8837: feat(algebra/add_torsor, linear_algebra/affine_…](topic/PR.20.238837.3A.20feat(algebra.2Fadd_torsor.2C.20linear_algebra.2Faffine_.2E.2E.2E.html) (3 messages, latest: Apr 10 2022 at 14:13)
• PR #10348: Add whilecc.lean (6 messages, latest: Apr 07 2022 at 14:13)
• PR #10131: feat(list/prod_monoid): add list.prod_map* lemmas (2 messages, latest: Apr 06 2022 at 14:13)
• PR #12478: feat(algebra/algebra/basic): Introduce non-uni… (1 message, latest: Apr 04 2022 at 14:14)
• PR #8781: feat(linear_algebra/{tensor,exterior,clifford})… (1 message, latest: Apr 03 2022 at 14:12)
• PR #11649: feat(algebraic_geometry): Intersection of affi… (1 message, latest: Apr 02 2022 at 14:13)
• [PR #5923: feat(group_theory/perm/sign): Add lemma about (…](topic/PR.20.235923.3A.20feat(group_theory.2Fperm.2Fsign).3A.20Add.20lemma.20about.20(.2E.2E.2E.html) (6 messages, latest: Mar 31 2022 at 14:13)
• PR #3292: feat(field_theory/complete_ordered): conditiona… (2 messages, latest: Mar 30 2022 at 14:28)
• PR #9573: refactor(topology/order): redefine `topological… (3 messages, latest: Mar 29 2022 at 14:13)
• PR #10539: refactor(order): uninstance pi.has_le (2 messages, latest: Mar 27 2022 at 14:17)
• [PR #12186: feat(algebraic_geometry/) : presheaf of modules](topic/PR.20.2312186.3A.20feat(algebraic_geometry.2F).20.3A.20presheaf.20of.20modules.html) (1 message, latest: Mar 25 2022 at 14:13)
• PR #9387: feat(probability_theory/independence): if a fam… (1 message, latest: Mar 24 2022 at 14:13)
• PR #8559: feat(analysis/complex/isometry): Homomorphism f… (1 message, latest: Mar 22 2022 at 14:13)
• PR #6476: feat(algebra/ring/boolean_ring): boolean_algebr… (5 messages, latest: Mar 20 2022 at 14:20)
• PR #5527: feat(order/heyting_algebra): Heyting algebras (3 messages, latest: Mar 19 2022 at 14:21)
• issue #6025: Convert subsingleton lemmas to instances (1 message, latest: Mar 15 2022 at 14:14)
• [PR #11282: feat(): has_repr instances for option-lik…](topic/PR.20.2311282.3A.20feat().3A.20.60has_repr.60.20instances.20for.20.60option.60-lik.2E.2E.2E.html) (3 messages, latest: Mar 14 2022 at 16:40)
• PR #9123: feat(algebra/smul_with_zero): `distrib_mul_acti… (3 messages, latest: Mar 14 2022 at 14:15)
• PR #4956: feat(archive/imo): formalise 1979 Q1 (5 messages, latest: Mar 13 2022 at 15:18)
• [PR #9943: feat(measure_theory/measure/finite_measure_weak…](topic/PR.20.239943.3A.20feat(measure_theory.2Fmeasure.2Ffinite_measure_weak.2E.2E.2E.html) (1 message, latest: Mar 11 2022 at 14:13)
• PR #12046: feat(topology/bornology/hom): Bounded maps (1 message, latest: Mar 10 2022 at 14:12)
• PR #11458: feat(analysis/convex/topology): Separating by … (1 message, latest: Mar 09 2022 at 14:12)
• issue #1068: category instances for all the 'standard' al… (2 messages, latest: Mar 07 2022 at 21:37)
• PR #9525: fix(algebra/ring): fix diamonds in nat- and int… (1 message, latest: Mar 03 2022 at 14:13)
• PR #3332: feat(data/qpf/indexed): indexed families of dat… (7 messages, latest: Mar 03 2022 at 00:58)
• PR #8280: feat(group_theory/quotient_group): the Zassenha… (3 messages, latest: Feb 27 2022 at 14:12)
• PR #11642: doc(algebra,data/fun_like): small morphism doc… (2 messages, latest: Feb 24 2022 at 14:47)
• PR #11229: feat(topology/continuous_function/compact): co… (1 message, latest: Feb 22 2022 at 14:12)
• PR #10235: refactor(algebra/opposites): use `mul_opposite… (1 message, latest: Feb 20 2022 at 14:12)
• PR #6152: feat(linear_algebra/multilinear): add notation (2 messages, latest: Feb 19 2022 at 14:12)
• PR #5574: feat(archive/100-theorems-list): Ballot Problem (14 messages, latest: Feb 16 2022 at 16:27)
• PR #9925: feat(data/nat/choose): add facts about the mult… (1 message, latest: Feb 13 2022 at 14:16)
• PR #11231: feat(measure_theory/function/lp_space): genera… (2 messages, latest: Feb 12 2022 at 14:20)
• issue #2871: unique factorisation of polynomials over a UFD (22 messages, latest: Feb 11 2022 at 18:27)
• PR #10641: refactor(algebra/direct_sum): unbundle `direct… (1 message, latest: Feb 11 2022 at 14:16)
• PRs #6606, #6427, #6428, #6429, #6421 (5 messages, latest: Feb 10 2022 at 05:34)
• PR #10693: feat(data/equiv/basic): lemmas about compositi… (1 message, latest: Feb 09 2022 at 14:16)
• PR #11109: split(data/finsupp/multiset): Split off `data…. (1 message, latest: Feb 08 2022 at 14:17)
• PR #6642: refactor(module/submodule): allow submodules to… (5 messages, latest: Feb 07 2022 at 14:17)
• [PR #8889: feat(algebra/ordered_monoid): sub_neg_monoid (w…](topic/PR.20.238889.3A.20feat(algebra.2Fordered_monoid).3A.20sub_neg_monoid.20(w.2E.2E.2E.html) (1 message, latest: Feb 05 2022 at 14:14)
• issue #2882: apply_congr with h (9 messages, latest: Feb 05 2022 at 01:35)
• PR #10867: feat(combinatorics/simple_graph/inc_matrix): I… (1 message, latest: Feb 02 2022 at 14:16)
• PR #4259: feat(archive/100-theorems-list): Partition theorem (3 messages, latest: Jan 30 2022 at 14:15)
• issue #2891: support multiple targets in equiv_rw (8 messages, latest: Jan 29 2022 at 21:22)
• PR #11347: refactor(data/equiv/basic): Deduce variants of… (1 message, latest: Jan 28 2022 at 14:16)
• issue #7564: Define the Gamma function (1 message, latest: Jan 26 2022 at 14:16)
• PR #8295: feat(geometry/manifold/tangent_bundle): the `ta… (2 messages, latest: Jan 25 2022 at 14:16)
• PR #8289: feat(data/matrix/basic): miscellaneous defs and… (3 messages, latest: Jan 24 2022 at 14:17)
• issue #3097: squeeze_simp produces invalid result (19 messages, latest: Jan 24 2022 at 14:17)
• PR #2508: feat(topology/local_homeomorph): define `local_… (3 messages, latest: Jan 23 2022 at 14:16)
• PR #10140: chore(linear_algebra/multilinear): remove the … (2 messages, latest: Jan 21 2022 at 14:17)
• PR #11095: feat(combinatorics/simple_graph/connectivity):… (1 message, latest: Jan 19 2022 at 14:16)
• PR #9370: feat(field_theory/is_alg_closed/classification)… (2 messages, latest: Jan 15 2022 at 14:17)
• PR #7833: feat(measure_theory/arithmetic): add instances … (1 message, latest: Jan 14 2022 at 14:18)
• issue #5863: Make linters emit messages in a way that's u… (3 messages, latest: Jan 10 2022 at 17:21)
• PR #7980: feat(order/directed): Add codirected_order clas… (2 messages, latest: Jan 08 2022 at 15:41)
• issue #3428: library_search and negation (9 messages, latest: Jan 08 2022 at 14:16)
• PR #4678: feat(tactic/congr): use reducible transparency (3 messages, latest: Jan 07 2022 at 14:17)
• issue #694: We don't have Cauchy's integral formula (12 messages, latest: Jan 06 2022 at 14:49)
• PR #9145: feat(data/mv_polynomial/derivation): derivation… (1 message, latest: Jan 05 2022 at 14:15)
• PR #5521: feat(analysis/calculus/deriv): let simp compute… (7 messages, latest: Jan 03 2022 at 14:17)
• PR #2578: feat(group_theory/free_monoid_product): define … (1 message, latest: Dec 31 2021 at 14:17)
• issue #1093: basic theory of Lie algebras (6 messages, latest: Dec 28 2021 at 12:58)
• issue #10213: Lax-Milgram theorem (1 message, latest: Dec 25 2021 at 14:17)
• PR #10372: feat(linear_algebra/trace): dual_tensor_hom i… (1 message, latest: Dec 22 2021 at 14:18)
• PR #9733: feat(data/set/basic): decidable_mem (2 messages, latest: Dec 21 2021 at 14:17)
• issue #2376: omega is slow with nonstandard 7 (29 messages, latest: Dec 19 2021 at 16:00)
• PR #9490: feat(group_theory/double_cosets): definition of… (1 message, latest: Dec 19 2021 at 14:17)
• issue #687: Linting tools (6 messages, latest: Dec 18 2021 at 14:51)
• PR #10221: doc(algebra/algebra/basic): expand the docstring (5 messages, latest: Dec 15 2021 at 20:16)
• PR #6448: feat(tactic/set): added set_taut to prove set e… (2 messages, latest: Dec 11 2021 at 14:18)
• PR #1822: [WIP] feat(ring_theory/dedekind_finite) some ba… (4 messages, latest: Dec 06 2021 at 14:48)
• PR #7498: feat(combinatorics/simple_graph/inc_matrix): ad… (1 message, latest: Dec 04 2021 at 14:19)
• PR #9545: feat(group_theory/commensurable): Definition an… (1 message, latest: Dec 03 2021 at 14:20)
• PR #8903: feat(analysis): Cauchy integral formula (WIP) (1 message, latest: Dec 02 2021 at 14:19)
• PR #10439: Define compact convergence topology on contino… (2 messages, latest: Dec 01 2021 at 16:40)
• issue #2890: equiv_rw fails with metavariables (1 message, latest: Dec 01 2021 at 14:20)
• issue #1098: examples of (symmetric) monoidal categories (4 messages, latest: Nov 25 2021 at 18:06)
• PR #4787: refactor(analysis/convex): redefine convex fo… (5 messages, latest: Nov 25 2021 at 14:19)
• PR #4273: feat(data/set/intervals/with_bot_top): lemmas a… (34 messages, latest: Nov 24 2021 at 14:19)
• PR #8242: feat(category_theory/adjunctions): adjust simp set (2 messages, latest: Nov 22 2021 at 14:19)
• PR #6441: fix(data/list/defs): remove chunking hack (2 messages, latest: Nov 19 2021 at 14:19)
• PR #7274: feat(archive/100-theorems-list): add proof of t… (5 messages, latest: Nov 17 2021 at 14:19)
• PR #2770: feat(combinatorics): Kruskal-Katona theorem and… (2 messages, latest: Nov 11 2021 at 14:19)
• issue #1866: Move module below group_power in the `im… (5 messages, latest: Nov 10 2021 at 14:20)
• issue #1639: to_additive should copy simps and `exten… (13 messages, latest: Nov 08 2021 at 18:01)
• PR #9606: feat(ring_theory/euclidean_domain): generalize … (3 messages, latest: Nov 08 2021 at 11:44)
• PR #8915: feat(number_theory/basic): lifting the exponent… (1 message, latest: Nov 06 2021 at 14:18)
• [PR #8901: refactor(field_theory/): generalize subfields …](topic/PR.20.238901.3A.20refactor(field_theory.2F).3A.20generalize.20subfields.20.2E.2E.2E.html) (1 message, latest: Nov 05 2021 at 14:19)
• PR #6295: feat(topology/homeomorph): Add homeomorph_of_co… (2 messages, latest: Nov 02 2021 at 14:19)
• [PR #7645: refactor(algebra/linear_ordered_comm_group_with…](topic/PR.20.237645.3A.20refactor(algebra.2Flinear_ordered_comm_group_with.2E.2E.2E.html) (2 messages, latest: Oct 31 2021 at 14:18)
• PR #2492: refactor(data/polynomial): use `monoid_algebra…. (3 messages, latest: Oct 30 2021 at 14:18)
• issue #946: data.nat.cast.cast is too general to be an in… (17 messages, latest: Oct 30 2021 at 14:18)
• PR #8082: feat(order/succ_pred): define the typeclass `su… (1 message, latest: Oct 29 2021 at 14:19)
• issue #1044: bundling morphisms (16 messages, latest: Oct 28 2021 at 14:39)
• PR #6955: feat(computability/tm_to_partrec): prove finite… (2 messages, latest: Oct 28 2021 at 14:23)
• issue #9805: convert proves 1=0 (1 message, latest: Oct 27 2021 at 14:19)
• PR #8981: add file containing the Weierstrass M-test (1 message, latest: Oct 25 2021 at 14:19)
• PR #8154: feat(topology/vector_bundle): `topological_vect… (1 message, latest: Oct 23 2021 at 14:18)
• PR #2784: feat(number_theory/bertrand): Bertrand's postulate (4 messages, latest: Oct 19 2021 at 14:19)
• PR #7539: feat (order/modular_lattice): modular_lattice a… (1 message, latest: Oct 15 2021 at 14:18)
• PR #7206: chore(data/mv_polynomial/basic): make monomial … (1 message, latest: Oct 14 2021 at 14:19)
• issue #4413: document op_induction (2 messages, latest: Oct 11 2021 at 01:20)
• issue #9421: Use has_star.star instead of complex.conj (2 messages, latest: Oct 09 2021 at 23:23)
• PR #7138: feat(combinatorics/simple_graph/basic): add lem… (1 message, latest: Oct 08 2021 at 14:18)
• PR #6307: feat(algebra/big_operators/order): some variants (2 messages, latest: Oct 05 2021 at 15:03)
• PR #7813: feat(data/nat/digits): Add lemmas (1 message, latest: Oct 04 2021 at 14:18)
• workflow failure (8 messages, latest: May 20 2021 at 06:11)
• [PR #6606: feat(linear_algebra/bilinear_form, linear_algeb…](topic/PR.20.236606.3A.20feat(linear_algebra.2Fbilinear_form.2C.20linear_algeb.2E.2E.2E.html) (1 message, latest: Apr 27 2021 at 14:25)
• issue #2551: Quadratic forms over R — Sylvester's law of … (8 messages, latest: Apr 24 2021 at 14:24)
• [PR #5823: chore() clean up file imports by removing tran…](topic/PR.20.235823.3A.20chore().20clean.20up.20file.20imports.20by.20removing.20tran.2E.2E.2E.html) (10 messages, latest: Apr 22 2021 at 14:24)
• issue #5258: Abel-Ruffini theorem (3 messages, latest: Apr 21 2021 at 15:20)
• PR #4913: feat(analysis/normed_space/box_subadditive): de… (1 message, latest: Apr 21 2021 at 14:27)
• PR #6244: feat(data/fin): lemmas about append (1 message, latest: Apr 20 2021 at 14:24)
• PR #5927: feat(category_theory/sites): Sheaves of structures (1 message, latest: Apr 17 2021 at 14:22)
• [PR #6741: feat(): Add is_scalar_tower instances for tens…](topic/PR.20.236741.3A.20feat().3A.20Add.20is_scalar_tower.20instances.20for.20tens.2E.2E.2E.html) (2 messages, latest: Apr 16 2021 at 14:24)
• PR #6923: feat(analysis/complex/isometry): add linear_iso… (1 message, latest: Apr 15 2021 at 14:23)
• issue #2176: Define preadditive categories (16 messages, latest: Apr 12 2021 at 03:01)
• PR #3083: refactor(data/finset): use lattice operations (4 messages, latest: Apr 10 2021 at 14:22)
• PR #5539: feat(algebra/field): define division semirings … (2 messages, latest: Apr 08 2021 at 14:24)
• issue #3837: @\[simps\] does not consider projections of … (4 messages, latest: Apr 08 2021 at 14:24)
• [PR #6773: chore(): redefine {nat,int} mul based on a lef…](topic/PR.20.236773.3A.20chore().3A.20redefine.20.7Bnat.2Cint.7D.20mul.20based.20on.20a.20lef.2E.2E.2E.html) (10 messages, latest: Apr 07 2021 at 21:24)
• issue #1608: catch leftover set_option commands (1 message, latest: Apr 07 2021 at 14:25)
• issue #1850: Fundamental theorem of calculus (2 messages, latest: Apr 03 2021 at 14:22)
• PR #6258: feat(ring_theory/laurent_series): introduce rin… (1 message, latest: Apr 02 2021 at 14:23)
• PR #5783: feat(multiset/basic): add lemma exists_minimal_… (2 messages, latest: Mar 28 2021 at 14:23)
• PR #4321: feat(algebra/free_algebra): Define a grading (26 messages, latest: Mar 23 2021 at 08:38)
• PR #6061: feat(tactic/lint): linter for @[class] def (4 messages, latest: Mar 23 2021 at 01:26)
• [PR #5851: chore(/pi): rename *_hom.apply to pi.apply_hom](topic/PR.20.235851.3A.20chore(*.2Fpi).3A.20rename.20*_hom.2Eapply.20to.20pi.2Eapply*_hom.html) (2 messages, latest: Mar 18 2021 at 14:28)
• PR #4301: feat(liouville_theorem): lemmas of Liouville th… (14 messages, latest: Mar 17 2021 at 08:17)
• issue #1922: Intuitionistic versions of finish use clas… (15 messages, latest: Mar 15 2021 at 14:28)
• PR #6291: feat(topology/category/profinite): Initial work… (1 message, latest: Mar 14 2021 at 14:21)
• issue #4763: topology/sheaves/sheaf_condition/pairwise_in… (4 messages, latest: Mar 14 2021 at 14:21)
• PR #2292: refactor(algebra/group): make multiplicative … (53 messages, latest: Mar 13 2021 at 16:05)
• PR #3169: feat(ring_theory/polynomial): homogeneous and s… (2 messages, latest: Mar 13 2021 at 14:21)
• PR #2311: Poincaré recurrence theorem (5 messages, latest: Mar 12 2021 at 14:27)
• PR #4615: feat(tactic/converter): Add an exact tactic, to… (8 messages, latest: Mar 11 2021 at 14:26)
• PR #4885: feat(category_theory/adjunction): general adjoi… (4 messages, latest: Mar 08 2021 at 14:44)
• PR #5975: feat(nat/digits): Natural basis representation … (3 messages, latest: Mar 06 2021 at 14:20)
• PR #5487: feat(tactic/to_additive): Allow to_additive aft… (1 message, latest: Mar 01 2021 at 14:20)
• PR #4707: feat(data/polynomial/reverse.lean): show traili… (5 messages, latest: Feb 28 2021 at 14:40)
• PR #2819: [WIP] feat(number_theory/geometry_of_numbers): … (6 messages, latest: Feb 27 2021 at 14:19)
• PR #5152: feat(category_theory): Global Left Kan extension (1 message, latest: Feb 24 2021 at 14:25)
• PR #5966: feat(combinatorics/simple_graph): degree lemmas (1 message, latest: Feb 22 2021 at 14:19)
• PR #4930: feat(category_theory/closed): Exponential ideals (4 messages, latest: Feb 20 2021 at 14:19)
• PR #2300: feat(tactic): tactic block caching (2 messages, latest: Feb 19 2021 at 14:20)
• PR #4069: added statements for trailing_degree, nat_trail… (2 messages, latest: Feb 15 2021 at 14:35)
• PR #5893: doc(data/finset): rewrite finset doc-strings (1 message, latest: Feb 14 2021 at 14:19)
• PR #5104: feat(order/antichain): introduce antichain (2 messages, latest: Feb 13 2021 at 14:19)
• issue #2706: rename squeeze_simp to simp? and have it… (4 messages, latest: Feb 12 2021 at 15:51)
• [PR #4619: refactor(algebra/): Attempt to generalize the …](topic/PR.20.234619.3A.20refactor(algebra.2F).3A.20Attempt.20to.20generalize.20the.20.2E.2E.2E.html) (3 messages, latest: Feb 12 2021 at 14:20)
• PR #5672: feat(algebra/subalgebra): Trivial subalgebra ha… (1 message, latest: Feb 08 2021 at 14:19)
• PR #3635: WIP: Remove the requirement from ideal that t… (4 messages, latest: Feb 07 2021 at 18:50)
• issue #4674: Roots in alg closed fields (3 messages, latest: Feb 06 2021 at 14:19)
• PR #4731: feat(archive/imo): formalize 1987Q1 (1 message, latest: Feb 05 2021 at 14:20)
• issue #1481: ext? should print a trace message (3 messages, latest: Jan 30 2021 at 14:27)
• issue #5525: Unify (or at least connect) preorder_hom a… (1 message, latest: Jan 29 2021 at 14:23)
• PR #5591: feat(geometry/manifold/instances): sphere is a … (6 messages, latest: Jan 28 2021 at 17:08)
• PR #3980: feat(group_theory/group_action): add Cayley's t… (1 message, latest: Jan 27 2021 at 14:23)
• PR #4832: chore(topology/sheaves/sheaf_condition): first … (2 messages, latest: Jan 25 2021 at 14:46)
• issue #1563: order of element (8 messages, latest: Jan 23 2021 at 16:23)
• issue #1853: Define Bochner integrals over subsets and me… (2 messages, latest: Jan 22 2021 at 14:56)
• PR #4949: chore(linear_algebra/basis): make more args exp… (1 message, latest: Jan 21 2021 at 14:44)
• issue #1093: definition of Lie algebras (11 messages, latest: Jan 16 2021 at 16:01)
• PR #5462: feat(data/buffer/parser/numeral): numeral parse… (2 messages, latest: Jan 15 2021 at 20:10)
• PR #4756: feat(algebra/category/Module): direct limit is … (3 messages, latest: Jan 13 2021 at 14:45)
• issue #2672: Bug in ring tactic (3 messages, latest: Jan 12 2021 at 16:38)
• PR #2630: refactor(computability/reduce): define many-one… (5 messages, latest: Jan 11 2021 at 15:48)
• issue #3326: non-idempotence of ring (when following zify) (3 messages, latest: Jan 09 2021 at 14:36)
• PR #5010: feat(data/fin): identities in add and mul monoids (2 messages, latest: Jan 08 2021 at 14:50)
• PR #5361: feat(analysis/real/polynomial): preparations fo… (2 messages, latest: Jan 04 2021 at 14:43)
• issue #2889: missing instance equiv_functor unique (1 message, latest: Dec 30 2020 at 14:29)
• PR #4812: feat(algebra/graded_algebra): Define a dependen… (6 messages, latest: Dec 28 2020 at 14:54)
• PR #5282: feat(category_theory/sites): closed sieves (2 messages, latest: Dec 27 2020 at 14:37)
• PR #5269: feat(linear_algebra/alternating): Add dom_coprod (2 messages, latest: Dec 25 2020 at 14:34)
• issue #2872: ideal.is_coprime is about elements not ideal… (4 messages, latest: Dec 18 2020 at 18:30)
• PR #5000: feat(measure_theory/measure_space): add theorem… (1 message, latest: Dec 17 2020 at 14:26)
• PR #4458: feat(analysis/calculus): define a smooth bump f… (3 messages, latest: Dec 15 2020 at 19:05)
• issue #1535: have library_search call symmetry before… (4 messages, latest: Dec 14 2020 at 15:53)
• PR #4773: feat(ring_theory/tensor_product): the base chan… (1 message, latest: Dec 13 2020 at 14:24)
• PR #4658: feat(topology/vector_bundle): definition of top… (4 messages, latest: Dec 10 2020 at 14:24)
• PR #4867: feat(algebra/continued_fractions): add terminat… (1 message, latest: Dec 08 2020 at 14:24)
• PR #2843: refactor(algebra/group/basic): minimal axioms f… (2 messages, latest: Dec 06 2020 at 18:55)
• PR #4843: feat(dynamics): (semi-)flows, omega limits (5 messages, latest: Dec 03 2020 at 14:45)
• PR #4406: feat(data/finvec): homogeneous vectors based on… (2 messages, latest: Dec 02 2020 at 14:24)
• PR #3770: feat(linear_algebra): algebra multilinear maps (11 messages, latest: Dec 01 2020 at 09:22)
• [PR #4817: chore(): Test leanprover-community/lean#495](topic/PR.20.234817.3A.20chore().3A.20Test.20leanprover-community.2Flean.23495.html) (1 message, latest: Nov 28 2020 at 14:19)
• issue #4449: Migrate is_Z_bilin to the general theory (1 message, latest: Nov 27 2020 at 14:20)
• issue #1534: add variations of nat.mod_add_div (1 message, latest: Nov 24 2020 at 14:20)
• issue #4210: to_additive fails for integer literals (1 message, latest: Nov 22 2020 at 14:18)
• PR #4718: feat(tactic/explode): display exploded proofs a… (6 messages, latest: Nov 21 2020 at 06:14)
• PR #4841: feat(tactic/rewrite_search): Automatically sear… (3 messages, latest: Nov 16 2020 at 14:29)
• issue #930: feat(algebra): add additive versions for free… (4 messages, latest: Nov 13 2020 at 18:02)
• PR #4608: feat(category_theory/sites): sheaves on a groth… (7 messages, latest: Nov 13 2020 at 17:36)
• issue #4660: Library note for when implicit arguments are… (3 messages, latest: Nov 11 2020 at 12:16)
• PR #4369: feat(archive/imo): formalize IMO 1964 problem 1 (6 messages, latest: Nov 07 2020 at 21:14)
• random PR: [WIP] feat(number_theory/geometry_of_numbers):… (8 messages, latest: Nov 01 2020 at 22:28)
• random issue: #2726 (7 messages, latest: Nov 01 2020 at 18:44)
• random issue: simpa accepts non-existing lemmas (#2061) (3 messages, latest: Nov 01 2020 at 16:55)
• random issue: transporting definitions and theorems along… (16 messages, latest: Nov 01 2020 at 12:16)
• random PR: #773 (5 messages, latest: Oct 30 2020 at 20:44)
• stream events (4 messages, latest: Oct 30 2020 at 20:34)

---

Last updated: Dec 20 2023 at 11:08 UTC