Zulip Chat Archive

Stream: triage

---

Topics:

• PR !4#18646: feat(RingTheory): isotypic components (1 message, latest: Apr 15 2025 at 14:14)
• issue !4#6509: Add Trans instances for morphisms (4 messages, latest: Apr 15 2025 at 14:14)
• PR !4#15906: feat: define singular manifolds (2 messages, latest: Apr 14 2025 at 14:15)
• issue !4#12737: Tracking: explicit universes can improve … (2 messages, latest: Apr 14 2025 at 14:13)
• issue !4#2032: refactor: redefine metrizable and Polish s… (9 messages, latest: Apr 14 2025 at 08:46)
• PR !4#20652: feat: categorical description of center of a… (1 message, latest: Apr 13 2025 at 14:13)
• issue !4#21324: Lightweight variant of group (1 message, latest: Apr 13 2025 at 14:13)
• [PR !4#8977: testing for leanprover/lean4#2940 (`extends f…](topic/PR.20!4.238977.3A.20testing.20for.20leanprover.2Flean4.232940.20(.60extends.20f.2E.2E.2E.html) (2 messages, latest: Apr 12 2025 at 14:12)
• PR !4#14009: chore: replace continuity -> fun_prop in rem… (1 message, latest: Apr 11 2025 at 14:13)
• issue !4#10752: Porting note: added dsimp only (4 messages, latest: Apr 11 2025 at 14:13)
• issue !4#5025: simp does not try applying @\[refl\] lem… (9 messages, latest: Apr 10 2025 at 18:52)
• PR !4#18679: DO NOT MERGE! test: latest import script (3 messages, latest: Apr 10 2025 at 15:04)
• PR !4#21450: feat: improve trace nodes for positivity (1 message, latest: Apr 09 2025 at 14:15)
• issue !4#11031: Doc bug: "Using mathlib4 as a dependency"… (4 messages, latest: Apr 09 2025 at 14:15)
• PR !4#22828: feat(CategoryTheory): parametrized adjunctions (1 message, latest: Apr 08 2025 at 14:13)
• issue !4#13732: bibtool not available in provided dev c… (5 messages, latest: Apr 08 2025 at 14:13)
• PR !4#21948: feat(ModelTheory): Formula.iSup and iInf (1 message, latest: Apr 07 2025 at 14:14)
• issue !4#10906: Diamonds at reducible_and_instances tra… (2 messages, latest: Apr 07 2025 at 14:14)
• PR !4#23396: chore: split LocallyFinite results out of Co… (4 messages, latest: Apr 06 2025 at 15:50)
• issue !4#6646: Make use of loopy instances for implicatio… (4 messages, latest: Apr 06 2025 at 14:12)
• PR !4#16303: feat(CI): check for badly formatted titles o… (1 message, latest: Apr 05 2025 at 14:12)
• issue !4#10675: Porting note: dsimp cannot prove this (2 messages, latest: Apr 05 2025 at 14:12)
• PR !4#7713: feat: add_left/right_inj for measures (3 messages, latest: Apr 04 2025 at 14:14)
• issue !4#2029: refactor: generalize `LocallyFinite.exists… (2 messages, latest: Apr 04 2025 at 14:14)
• PR !4#10129: fix(Topology/MetricSpace/InfSep): Make `infs… (3 messages, latest: Apr 03 2025 at 14:14)
• issue !4#6645: have? can't find mul_left_cancel₀ (5 messages, latest: Apr 03 2025 at 14:14)
• PR !4#7427: Mohanad ahmed/sort eigenvalues abs (2 messages, latest: Apr 02 2025 at 14:13)
• issue !4#17887: Support of partial derivative (1 message, latest: Apr 02 2025 at 14:13)
• PR !4#15679: test: refactor in CI (2 messages, latest: Apr 01 2025 at 14:14)
• issue !4#5560: Rename neg_nsmul to nsmul_neg (4 messages, latest: Apr 01 2025 at 14:14)
• PR !4#18914: fix(Tactic/Linter): the minImports linter … (1 message, latest: Mar 31 2025 at 14:13)
• issue !4#5539: Orthogonality for affine subspaces (2 messages, latest: Mar 31 2025 at 14:13)
• PR !4#20967: tracking(CategoryTheory/Enriched/Limits): ad… (1 message, latest: Mar 30 2025 at 14:12)
• issue !4#10539: Follow up from #9697: generalize nilpoten… (2 messages, latest: Mar 30 2025 at 14:12)
• PR !4#16311: feat(Computability): regular languages are c… (2 messages, latest: Mar 29 2025 at 14:12)
• issue !4#22219: Turn compute_degree into a simproc (1 message, latest: Mar 29 2025 at 14:12)
• PR !4#7994: chore: generalize `LieSubalgebra.mem_map_subm… (2 messages, latest: Mar 28 2025 at 14:14)
• issue !4#11911: IsMatching is only defined on subgraphs o… (2 messages, latest: Mar 28 2025 at 14:14)
• issue !4#11678: Typo in Mathlib.Condensed.Explicit doc (2 messages, latest: Mar 27 2025 at 15:38)
• PR !4#23057: doc: library note about argument order in in… (1 message, latest: Mar 27 2025 at 14:13)
• issue !4#19341: Sharpness in linear_combination (3 messages, latest: Mar 27 2025 at 11:10)
• PR !4#4871: feat: define the additive submonoid of positi… (1 message, latest: Mar 26 2025 at 14:14)
• issue !4#15486: Tracking issue for slow field_simp call… (4 messages, latest: Mar 25 2025 at 14:29)
• PR !4#22579: doc(Topology/Defs/Induced): fix comments on … (1 message, latest: Mar 25 2025 at 14:13)
• PR !4#15115: feat: Generalize assumptions in liminf and l… (1 message, latest: Mar 24 2025 at 14:14)
• issue !4#10424: Create BilinearMap abbreviation (2 messages, latest: Mar 24 2025 at 14:14)
• PR !4#15895: feat(Computability/ContextFreeGrammar): mapp… (1 message, latest: Mar 23 2025 at 14:13)
• issue !4#11647: tracking issue for change in behaviour in… (2 messages, latest: Mar 23 2025 at 14:13)
• PR !4#8616: feat(Algebra/FreeAlgebra): add right action a… (2 messages, latest: Mar 22 2025 at 14:12)
• issue !4#7930: simps should dsimp the type of the new arg… (3 messages, latest: Mar 22 2025 at 14:12)
• issue !4#11757: Carve out Algebra, Data and Order sublibr… (4 messages, latest: Mar 21 2025 at 14:13)
• PR !4#21903: feat: add from/toList between `FreeSemigroup… (1 message, latest: Mar 21 2025 at 14:13)
• PR !4#21336: feat(Algebra/Category): finitely presented a… (2 messages, latest: Mar 20 2025 at 14:44)
• issue !4#2417: Typeclass search doesn't find Fintype fo… (5 messages, latest: Mar 20 2025 at 14:14)
• PR !4#12493: chore: split Data.DFinsupp.Basic (1 message, latest: Mar 19 2025 at 14:13)
• PR !4#22253: feat(Set): lemmas about set difference (1 message, latest: Mar 18 2025 at 14:13)
• issue !4#19288: Generalise Asymptotics API to drop commut… (2 messages, latest: Mar 18 2025 at 14:13)
• PR !4#10476: feat(Topology/UniformSpace): define uniform … (2 messages, latest: Mar 17 2025 at 14:14)
• issue !4#404: should clear_ tactic also clear inaccessi… (3 messages, latest: Mar 17 2025 at 14:14)
• issue !4#994: decide regression (5 messages, latest: Mar 17 2025 at 08:49)
• PR !4#21514: test: find label comment (2 messages, latest: Mar 16 2025 at 21:27)
• issue !4#5343: notation3 doesn't work with scoped (4 messages, latest: Mar 16 2025 at 21:16)
• [PR !4#6777: chore(CovariantClass): replace eta-expanded …](topic/PR.20!4.236777.3A.20chore(CovariantClass).3A.20replace.20eta-expanded.20.2E.2E.2E.html) (3 messages, latest: Mar 15 2025 at 14:12)
• PR !4#12143: feat: generic linter, absorbing cdot linte… (1 message, latest: Mar 14 2025 at 14:12)
• issue !4#12035: Tracking issue for Hurwitz and Dirichlet … (1 message, latest: Mar 14 2025 at 14:12)
• PR !4#8740: fix: improve recall impl / error reporting (1 message, latest: Mar 13 2025 at 14:12)
• issue !4#4326: Redefine real powers of NNReal numbers (3 messages, latest: Mar 13 2025 at 14:12)
• PR !4#21038: feat(Computability/Language): add Arden's lemma (1 message, latest: Mar 12 2025 at 14:13)
• issue !4#2202: Redesign bundled morphisms and sets (5 messages, latest: Mar 12 2025 at 14:13)
• PR !4#18206: chore(SetTheory/Ordinal/Basic): golf/clean u… (2 messages, latest: Mar 11 2025 at 15:07)
• issue !4#8052: After leanprover/lean4#2734, norm_cast o… (3 messages, latest: Mar 11 2025 at 14:14)
• PR !4#7835: feat(LinearAlgebra/Matrix): lift for projec… (1 message, latest: Mar 10 2025 at 14:14)
• issue !4#740: add protected after the fact? (2 messages, latest: Mar 10 2025 at 14:14)
• PR !4#15943: feat: add ProdQuotientMapSpace (2 messages, latest: Mar 09 2025 at 14:12)
• issue !4#2505: [refl] tag depends on order of instance ar… (4 messages, latest: Mar 09 2025 at 14:12)
• PR !4#15400: feat: "confusing variables" linter (1 message, latest: Mar 08 2025 at 14:11)
• issue !4#5379: Extend basic API about DomMulAct (2 messages, latest: Mar 08 2025 at 14:11)
• issue !4#11039: Porting note: broken proof was (5 messages, latest: Mar 08 2025 at 10:55)
• PR !4#20838: feat(Combinatorics/SimpleGraph): API for bip… (2 messages, latest: Mar 07 2025 at 18:02)
• PR !4#13573: feat: add multivariate polynomial modules (2 messages, latest: Mar 07 2025 at 14:12)
• issue !4#11215: Porting note: TODO (2 messages, latest: Mar 07 2025 at 14:12)
• issue !4#8075: refactor: switch to IsAdjoinRoot (3 messages, latest: Mar 06 2025 at 14:13)
• PR !4#22116: feat: Fin.castPred_ne_zero and `Pairwise.f… (1 message, latest: Mar 05 2025 at 14:13)
• issue !4#7657: simps sometimes gets types confused (3 messages, latest: Mar 05 2025 at 14:13)
• PR !4#21099: chore(RingTheory/Generators): use unificatio… (1 message, latest: Mar 04 2025 at 14:13)
• issue !4#741: zify incorrectly uses eq.refl (3 messages, latest: Mar 04 2025 at 14:13)
• PR !4#11393: feat(Analysis/Distribution/SchwartzSpace): T… (2 messages, latest: Mar 03 2025 at 14:14)
• issue !4#19934: Cartan matrices and their myriad generali… (1 message, latest: Mar 03 2025 at 14:14)
• [PR !4#8195: Feat (GroupTheory.SpecificGroups.PresentedDih…](topic/PR.20!4.238195.3A.20Feat.20(GroupTheory.2ESpecificGroups.2EPresentedDih.2E.2E.2E.html) (2 messages, latest: Mar 02 2025 at 14:11)
• PR !4#4979: doc(Data/Nat/Bitblast): initial commit (1 message, latest: Mar 01 2025 at 14:12)
• issue !4#2682: Miscellaneous tactic attempts (4 messages, latest: Mar 01 2025 at 14:12)
• PR !4#15254: feat(CategoryTheory/Monoidal): redefine `Mon… (5 messages, latest: Feb 28 2025 at 14:17)
• issue !4#13291: Reflection representations of a Coxeter g… (1 message, latest: Feb 28 2025 at 14:13)
• PR !4#8503: feat: meta utils for refine? (2 messages, latest: Feb 27 2025 at 14:13)
• issue !4#21333: Documentation error on comp_linearmap (1 message, latest: Feb 27 2025 at 14:13)
• PR !4#9935: feat(AlgebraicTopology): add constructors for… (1 message, latest: Feb 26 2025 at 14:13)
• issue !4#12096: Porting note: unimplemented instance_prio… (1 message, latest: Feb 26 2025 at 14:13)
• PR !4#21127: feat(Combinatorics/SimpleGraph): the Andrásf… (1 message, latest: Feb 25 2025 at 14:13)
• issue !4#5870: Sync DifferentiableAt.inv and `Different… (4 messages, latest: Feb 25 2025 at 14:13)
• [PR !4#5912: feat(Analysis.Distribution.ContDiffMapSupport…](topic/PR.20!4.235912.3A.20feat(Analysis.2EDistribution.2EContDiffMapSupport.2E.2E.2E.html) (3 messages, latest: Feb 24 2025 at 14:13)
• issue !4#5049: Tracking issue for troubles with the `simp… (3 messages, latest: Feb 24 2025 at 14:12)
• PR !4#18236: feat(Algebra/Category/ModuleCat/Presheaf): t… (1 message, latest: Feb 23 2025 at 14:13)
• issue !4#8135: Autogenerate lemmas about OfNat.ofNat (3 messages, latest: Feb 23 2025 at 14:13)
• PR !4#19066: feat(SetTheory/Ordinal/Nimber/Field): Nimber… (2 messages, latest: Feb 22 2025 at 21:37)
• issue !4#6091: My 100 theorems (2 messages, latest: Feb 22 2025 at 14:11)
• PR !4#18252: feat(Bicategory/Oplax): Fix simp lemmas and … (2 messages, latest: Feb 21 2025 at 14:11)
• issue !4#802: register_simp_attr with (2 messages, latest: Feb 21 2025 at 14:11)
• issue !4#15415: wrong link for Complex.abs in documentation (5 messages, latest: Feb 20 2025 at 15:03)
• PR !4#3251: feat: deriving LinearOrder for simple enoug… (2 messages, latest: Feb 20 2025 at 14:12)
• PR !4#21375: WIP: generalise lemmas to ENorm (2 messages, latest: Feb 19 2025 at 14:30)
• issue !4#10754: Porting note: added instance (1 message, latest: Feb 19 2025 at 14:13)
• PR !4#14704: feat(FieldTheory): define typeclass for simp… (1 message, latest: Feb 18 2025 at 14:12)
• issue !4#2437: Interface with SMT solvers (4 messages, latest: Feb 18 2025 at 14:12)
• PR !4#15989: feat(SetTheory/Ordinal/Principal): simplify … (3 messages, latest: Feb 18 2025 at 05:03)
• issue !4#1458: apply_rules in the symm + only confi… (26 messages, latest: Feb 17 2025 at 14:12)
• ✔ PR !4#21008: feat(Order/WellQuasiOrder): `WellQuasiOrde… (7 messages, latest: Feb 17 2025 at 05:35)
• PR !4#18474: perf: lower the priority of *WithOne.to* i… (1 message, latest: Feb 16 2025 at 14:12)
• issue !4#15871: Performance regressions using rintro ge… (1 message, latest: Feb 16 2025 at 14:12)
• PR !4#17071: feat : (LinearAlgebra/RootSystem) : Separati… (2 messages, latest: Feb 15 2025 at 20:19)
• issue !4#2030: refactor: add TC cycles (2 messages, latest: Feb 15 2025 at 14:11)
• PR !4#17672: refactor: turn IsTorsionFree into a typeclass (1 message, latest: Feb 14 2025 at 14:11)
• issue !4#16670: general theory of Galois categories (3 messages, latest: Feb 14 2025 at 14:11)
• PR !4#18629: feat(Computability.Timed): Formalization of … (1 message, latest: Feb 13 2025 at 14:13)
• issue !4#5752: Sometimes #synth X works, but `example :… (2 messages, latest: Feb 13 2025 at 14:13)
• PR !4#19337: feat(Data/Finsupp): generalise Finsupp to … (1 message, latest: Feb 12 2025 at 14:13)
• issue !4#9866: Use standard names for topological spaces (2 messages, latest: Feb 11 2025 at 14:12)
• PR !4#19563: feat(Probability): two kernels are a.e. equa… (1 message, latest: Feb 10 2025 at 14:12)
• issue !4#10959: Porting note: simp cannot prove this (4 messages, latest: Feb 10 2025 at 14:12)
• PR !4#8832: feat: add norm_num extensions for factorials (1 message, latest: Feb 09 2025 at 14:11)
• issue !4#694: performance regression in ring (1 message, latest: Feb 09 2025 at 14:11)
• PR !4#16532: feat: rewrite the linter for spaces before s… (1 message, latest: Feb 08 2025 at 14:11)
• PR !4#7890: feat(Mathlib/Tactic/Setm): implement setm tactic (1 message, latest: Feb 07 2025 at 14:12)
• issue !4#6679: Unify APIs and naming for codRestrict (5 messages, latest: Feb 07 2025 at 14:12)
• issue !4#5690: calculating in ZMod 4 is terrible (4 messages, latest: Feb 07 2025 at 06:52)
• [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) (4 messages, latest: Feb 06 2025 at 14:12)
• issue !4#394: Make by_contra accept binderIdent (2 messages, latest: Feb 06 2025 at 14:12)
• PR !4#14160: feat(Algebra/Group/Action/Defs): Redefine `F… (1 message, latest: Feb 04 2025 at 14:12)
• issue !4#12946: restore gh-problem-matcher-wrap in CI (3 messages, latest: Feb 04 2025 at 14:12)
• PR !4#13442: feat: mabel tactic for multiplicative abelia… (1 message, latest: Feb 03 2025 at 14:13)
• issue !4#19895: simps: allow specifying configuration opt… (1 message, latest: Feb 03 2025 at 14:13)
• PR !4#19693: feat(SetTheory/Cardinal/Cofinality): define … (2 messages, latest: Feb 03 2025 at 05:41)
• issue !4#2136: norm_num functionality tracking issue (4 messages, latest: Feb 02 2025 at 14:11)
• PR !4#19632: WIP CI (6 messages, latest: Feb 02 2025 at 09:59)
• issue !4#14484: Explode is incorrectly spaced when namesp… (1 message, latest: Feb 01 2025 at 14:11)
• PR !4#16626: test: print speed of rfl (2 messages, latest: Jan 31 2025 at 14:21)
• issue !4#6108: Consequences of Hölder inequality for cont… (2 messages, latest: Jan 31 2025 at 14:11)
• PR !4#7739: feat(LinearAlgebra/LinearPMap): difference of… (2 messages, latest: Jan 30 2025 at 14:12)
• issue !4#20232: possible bug revealed by failure to apply… (1 message, latest: Jan 30 2025 at 14:12)
• PR !4#7962: feat: DualNumber (Quaternion R) as a `Cliff… (1 message, latest: Jan 29 2025 at 14:12)
• issue !4#10745: Porting note: was simp (1 message, latest: Jan 29 2025 at 14:12)
• issue !4#13544: Rename zpow_le_zpow and rpow_le_rpow (2 messages, latest: Jan 28 2025 at 17:52)
• PR !4#16570: chore(Tactic/CategoryTheory): change `TermEl… (2 messages, latest: Jan 28 2025 at 14:13)
• PR !4#15277: feat(CStarAlgebra): matrices with entries in… (2 messages, latest: Jan 27 2025 at 16:57)
• issue !4#13864: Tracking issue: try replacing `measurabil… (1 message, latest: Jan 27 2025 at 14:12)
• PR !4#7601: feat: ring hom support in ring (2 messages, latest: Jan 26 2025 at 14:11)
• PR !4#20319: feat(Logic/IsEmpty/Relator): empty on sides (2 messages, latest: Jan 25 2025 at 14:48)
• issue !4#7083: local simp for simpsets (3 messages, latest: Jan 25 2025 at 14:11)
• PR !4#12353: feat: conv% (1 message, latest: Jan 24 2025 at 14:11)
• issue !4#15509: Proposal to add new attributes (2 messages, latest: Jan 24 2025 at 14:11)
• PR !4#11500: refactor(Topology/Algebra/Module/WeakDual): … (2 messages, latest: Jan 23 2025 at 14:13)
• issue !4#5463: Review all names with ' (9 messages, latest: Jan 22 2025 at 23:47)
• issue !4#11224: Porting note: change rw to erw (3 messages, latest: Jan 22 2025 at 23:45)
• PR !4#19721: feat (WIP): formalize Moreira's version of S… (2 messages, latest: Jan 22 2025 at 14:54)
• issue !4#214: Check notation precedences (1 message, latest: Jan 22 2025 at 14:12)
• PR !4#10190: feat(AlgebraicTopology): add Augmented Simp… (1 message, latest: Jan 21 2025 at 14:11)
• PR !4#20670: feat(CategoryTheory/Localization): HasLocali… (1 message, latest: Jan 20 2025 at 14:12)
• issue !4#11292: Using github releases (7 messages, latest: Jan 20 2025 at 00:14)
• PR !4#15906: feat: define singular n-manifolds (2 messages, latest: Jan 19 2025 at 19:09)
• PR !4#14563: feat: if-then-else of exclusive or statement (1 message, latest: Jan 19 2025 at 14:12)
• PR !4#7903: feat: define UnboundedSpace (2 messages, latest: Jan 18 2025 at 14:11)
• issue !4#11041: Porting note: broken ext (2 messages, latest: Jan 18 2025 at 14:11)
• issue !4#18237: Refactor field theory using IsConjRoot (1 message, latest: Jan 17 2025 at 14:11)
• PR !4#12006: feat: the suffa tactic (3 messages, latest: Jan 16 2025 at 14:16)
• issue !4#6038: Missing positivity extensions (5 messages, latest: Jan 16 2025 at 14:11)
• PR !4#19556: perf: disable the unused tactic linter (78 messages, latest: Jan 15 2025 at 22:14)
• ✔ PR !4#15874: doc(Order/InitialSeg): Improve documentation (3 messages, latest: Jan 14 2025 at 17:54)
• PR !4#7322: feat: Default list (1 message, latest: Jan 14 2025 at 14:12)
• PR !4#16810: feat: define (a : ENat) ^ (b : ENat) (1 message, latest: Jan 13 2025 at 14:12)
• issue !4#11227: Porting note: added simp (3 messages, latest: Jan 13 2025 at 14:12)
• PR !4#12251: refactor(RingTheory/HahnSeries) : several ge… (2 messages, latest: Jan 12 2025 at 10:49)
• issue !4#6105: Reorganize Analysis.Calculus.ContDiff[Def] (4 messages, latest: Jan 11 2025 at 14:11)
• [PR !4#17757: refactor(): generalize typeclass assumption…](topic/PR.20!4.2317757.3A.20refactor().3A.20generalize.20typeclass.20assumption.2E.2E.2E.html) (3 messages, latest: Jan 10 2025 at 20:13)
• issue !4#19588: Tracking issue: game order relations cleanup (2 messages, latest: Jan 09 2025 at 17:27)
• PR !4#5897: feat: add a MonadError instance for ContT (1 message, latest: Jan 08 2025 at 14:12)
• issue !4#3722: Redefine Matrix.UnitaryGroup.toGL etc (3 messages, latest: Jan 08 2025 at 14:12)
• PR !4#19164: Add toWithTop, ofWithTop (1 message, latest: Jan 07 2025 at 15:04)
• issue !4#2427: positivity enhancement (6 messages, latest: Jan 07 2025 at 15:04)
• PR !4#16120: feat(ModelTheory/Algebra/Ring/Basic): Ring h… (1 message, latest: Jan 06 2025 at 14:12)
• issue !4#3426: apply?/exact?/have?/rw? issues (3 messages, latest: Jan 06 2025 at 14:12)
• PR !4#17675: perf: do not search algebraic hierarchy when… (1 message, latest: Jan 05 2025 at 14:12)
• issue !4#13328: Broken link in mathlib4_docs (3 messages, latest: Jan 04 2025 at 17:37)
• PR !4#12192: feat: generalize isLittleO_const_id_atTop/atBot (1 message, latest: Jan 04 2025 at 14:11)
• issue !4#10068: A semisimple Lie algebra has non-degenera… (7 messages, latest: Jan 03 2025 at 18:35)
• issue !4#10971: Porting note: need dsimp only (2 messages, latest: Jan 03 2025 at 14:11)
• PR !4#6210: feat(Data/IsROrC/Basic): add a `StarOrderedRi… (1 message, latest: Jan 02 2025 at 14:11)
• issue !4#18548: Hermite functions (1 message, latest: Jan 02 2025 at 14:11)
• issue !4#9410: RewriteSearch.lean flaky tests? (7 messages, latest: Jan 02 2025 at 10:53)
• issue !4#10059: Docs mention non-existent Finset.univ' (5 messages, latest: Jan 02 2025 at 10:11)
• PR !4#12438: feat: some APIs for flat modules (2 messages, latest: Jan 02 2025 at 10:00)
• PR !4#10717: feat(Algebra/Homology): the total complex of… (1 message, latest: Jan 01 2025 at 14:12)
• PR !4#19973: feat(SetTheory/Order/Defs): not_lt_iff_not_l… (1 message, latest: Dec 31 2024 at 14:12)
• issue !4#2184: Use Pairwise in Set.iUnionLift and `Se… (1 message, latest: Dec 30 2024 at 14:11)
• PR !4#14007: test: papercut linter working on all mathlib (1 message, latest: Dec 29 2024 at 14:12)
• PR !4#9598: feat(Analysis/Complex): HasPrimitives on disc (2 messages, latest: Dec 28 2024 at 14:11)
• PR !4#8767: refactor(Cache): tidy lake-manifest parsing i… (1 message, latest: Dec 27 2024 at 14:11)
• issue !4#10395: Dot-notation for theorems that don't have… (1 message, latest: Dec 27 2024 at 14:11)
• issue !4#10067: Root system theory (10 messages, latest: Dec 27 2024 at 07:48)
• issue !4#5265: Improve positivity extension for norm (10 messages, latest: Dec 26 2024 at 14:14)
• PR !4#11633: refactor: Lighten finiteness dependencies (1 message, latest: Dec 26 2024 at 14:11)
• PR !4#10998: feat(Logic): Arithmetization of partial recu… (1 message, latest: Dec 25 2024 at 14:11)
• PR !4#19299: feat(Algebra/CategoryTheory): Add CommAlgebr… (1 message, latest: Dec 24 2024 at 14:11)
• issue !4#7781: use and ! incorrect parsing (1 message, latest: Dec 24 2024 at 14:11)
• PR !4#12581: feat: (Probability/SubProbabilityMassFunction) (1 message, latest: Dec 23 2024 at 14:11)
• issue !4#5617: Add typeclasses for smooth (· • ·) (1 message, latest: Dec 23 2024 at 14:11)
• PR !4#19551: perf: TRY disabling ALL syntax style linters… (1 message, latest: Dec 22 2024 at 14:12)
• PR !4#12310: feat: add Tropically bound polynomials (1 message, latest: Dec 21 2024 at 14:11)
• PR !4#14669: feat(Data/Nat/PartENat): add lemmas for Part… (1 message, latest: Dec 20 2024 at 14:12)
• PR !4#19198: feat(Algebra/Homology/Embedding): the homolo… (1 message, latest: Dec 19 2024 at 14:12)
• PR !4#19516: refactor(CategoryTheory/Sites): define Funct… (1 message, latest: Dec 18 2024 at 14:26)
• issue !4#12564: simps: generate all lemmas but one (3 messages, latest: Dec 18 2024 at 14:26)
• issue !4#2061: port and enhance tfae tactics (5 messages, latest: Dec 17 2024 at 17:46)
• PR !4#16656: feat(Data/Fintype/List): generalize `fintype… (1 message, latest: Dec 17 2024 at 14:12)
• PR !4#10026: Linear programming according to Antoine Cham… (1 message, latest: Dec 16 2024 at 14:13)
• issue !4#11081: Porting note: cannot automatically derive (1 message, latest: Dec 16 2024 at 14:13)
• PR !4#15822: feat: greedy colorings of finite graphs (1 message, latest: Dec 15 2024 at 14:11)
• PR !4#9040: feat: to_snoc an attribute for generating l… (3 messages, latest: Dec 15 2024 at 13:27)
• PR !4#15355: feat: MiM PR report (1 message, latest: Dec 14 2024 at 14:11)
• issue #11678: Typo in Mathlib.Condensed.Explicit doc (5 messages, latest: Dec 14 2024 at 01:27)
• PR !4#9510: feat(Analysis/Calculus/DualNumber): Extending… (1 message, latest: Dec 13 2024 at 14:12)
• PR !4#16984: feat: extend module tactic to handle multi… (1 message, latest: Dec 12 2024 at 14:12)
• issue !4#18942: @\[simps\] is sometimes used to generate … (3 messages, latest: Dec 12 2024 at 11:30)
• PR !4#11519: feat: syntax_rules (1 message, latest: Dec 10 2024 at 14:12)
• issue !4#8372: Merge exp, Real.exp, and Complex.exp (1 message, latest: Dec 09 2024 at 14:12)
• issue !4#5473: Redefine Trivialization (4 messages, latest: Dec 08 2024 at 14:11)
• issue !4#4862: Split file Analysis.BoundedVariation (3 messages, latest: Dec 07 2024 at 23:40)
• PR !4#17366: feat(Algebra/Category/ModuleCat): pullback o… (2 messages, latest: Dec 07 2024 at 14:14)
• PR !4#19547: perf: merge several style syntax linters (2 messages, latest: Dec 06 2024 at 22:55)
• issue !4#11573: Int.cast_negSucc makes norm_cast introduc… (5 messages, latest: Dec 06 2024 at 16:47)
• PR !4#8118: feat(CategoryTheory): add dinatural transform… (1 message, latest: Dec 05 2024 at 14:11)
• issue !4#12129: Porting notes: additional beta_reduction … (1 message, latest: Dec 05 2024 at 14:11)
• PR !4#18397: chore: Rename RestrictGenTopology to `Topo… (2 messages, latest: Dec 04 2024 at 14:54)
• PR !4#7875: chore: make SMulCommClass A A B and `SMulCo… (2 messages, latest: Dec 03 2024 at 14:11)
• issue !4#11036: Porting note: broken dot notation (1 message, latest: Dec 03 2024 at 14:11)
• PR !4#17513: perf: do not search algebraic hierarchies wh… (2 messages, latest: Dec 02 2024 at 14:12)
• issue !4#6335: Generalize Submodule.ofLe and its friend… (3 messages, latest: Dec 02 2024 at 14:12)
• PR !4#16925: feat(SetTheory/Cardinal/Cofinality): aleph i… (3 messages, latest: Dec 02 2024 at 06:11)
• PR !4#18667: feat(LinearAlgebra/Goursat): Goursat's lemma… (1 message, latest: Dec 01 2024 at 14:11)
• issue !4#10685: Porting note: dsimp can prove this (1 message, latest: Dec 01 2024 at 14:11)
• PR !4#14731: feat: the repeated typeclass assumption linter (2 messages, latest: Nov 30 2024 at 14:26)
• issue !4#7152: Algebras should imply both left and right … (1 message, latest: Nov 30 2024 at 14:11)
• issue !4#18720: Linter for unused variable declarations (2 messages, latest: Nov 29 2024 at 14:55)
• PR !4#7831: testing: lean4#2728 (1 message, latest: Nov 28 2024 at 14:12)
• PR !4#14943: test:flag imports (2 messages, latest: Nov 26 2024 at 14:47)
• PR !4#12778: perf: decouple algebraic and order hierarchi… (1 message, latest: Nov 25 2024 at 14:11)
• issue !4#6440: pp.unicode.fun=true is not turned on dur… (1 message, latest: Nov 25 2024 at 14:11)
• PR !4#7225: some random stuff (2 messages, latest: Nov 24 2024 at 14:11)
• PR !4#16054: chore(SetTheory/Game/Impartial): remove `Imp… (2 messages, latest: Nov 23 2024 at 19:55)
• issue !4#8275: Special-case Prop-valued fields in simps (5 messages, latest: Nov 23 2024 at 14:12)
• PR !4#5919: feat: implement orthogonality for AffineSubspace (2 messages, latest: Nov 22 2024 at 14:11)
• PR !4#11212: feat(GroupTheory/GroupAction): instance `Mul… (3 messages, latest: Nov 21 2024 at 14:11)
• issue !4#15410: norm_num for Nat.factors (1 message, latest: Nov 21 2024 at 14:11)
• PR !4#14727: feat(RingTheory/Flat/CategoryTheory): a flat… (1 message, latest: Nov 20 2024 at 14:12)
• issue !4#10830: to_additive doesn't always translate pr… (1 message, latest: Nov 20 2024 at 14:12)
• PR !4#7014: chore: cleanup of trans tactic (1 message, latest: Nov 19 2024 at 14:12)
• issue !4#10688: Porting note: added to ease automation (1 message, latest: Nov 19 2024 at 14:12)
• PR !4#14401: feat: add Stream'.pmap & Seq'.pmap (1 message, latest: Nov 18 2024 at 14:12)
• issue !4#3028: push_cast doesn't run rfl after operation (4 messages, latest: Nov 18 2024 at 14:12)
• issue !4#5073: rwa yields a confusing error when rw s… (2 messages, latest: Nov 17 2024 at 14:10)
• PR !4#16658: add tips file (2 messages, latest: Nov 16 2024 at 15:40)
• issue !4#10968: Porting library notes - tracking issue (1 message, latest: Nov 16 2024 at 14:11)
• issue !4#7839: Generalize `MeasureTheory.tendsto_measure_… (2 messages, latest: Nov 15 2024 at 14:11)
• PR !4#5952: feat: add Qq wrappers for ToExpr (1 message, latest: Nov 14 2024 at 14:11)
• issue !4#10888: Porting note: added proof (4 messages, latest: Nov 14 2024 at 14:11)
• issue !4#12717: Porting note: simp doesn't apply simp… (2 messages, latest: Nov 13 2024 at 14:26)
• PR !4#3757: feat: config options for fail_if_no_progress (1 message, latest: Nov 12 2024 at 14:12)
• PR !4#9256: chore: use Pairwise (_ on _) where possible (3 messages, latest: Nov 11 2024 at 17:25)
• issue !4#5030: continuity tactic is not as capable as i… (3 messages, latest: Nov 11 2024 at 14:12)
• PR !4#12429: feat: toND – auto-generating natDegree (5 messages, latest: Nov 10 2024 at 14:11)
• PR !4#8900: feat: Incidence algebras (3 messages, latest: Nov 09 2024 at 16:28)
• issue !4#11445: Porting note: added definition (1 message, latest: Nov 09 2024 at 14:11)
• PR !4#18294: perf: make Mul.toSMul higher priority (1 message, latest: Nov 08 2024 at 14:11)
• issue !4#11043: Porting note: was decide! (2 messages, latest: Nov 07 2024 at 17:40)
• PR !4#17069: chore(CategoryTheory/Functor/Basic): put `si… (1 message, latest: Nov 05 2024 at 14:12)
• PR !4#17580: feat: lint declarations which contain a doub… (1 message, latest: Nov 04 2024 at 14:12)
• issue !4#10066: Cartan subalgebras are conjugate (2 messages, latest: Nov 04 2024 at 14:12)
• PR !4#17889: chore(SetTheory/Ordinal/Notation): use `NatC… (2 messages, latest: Nov 03 2024 at 14:31)
• issue !4#5395: Define the setoid that glues a set into a pt (1 message, latest: Nov 03 2024 at 14:11)
• issue !4#14202: clean up completely normal results to use… (1 message, latest: Nov 02 2024 at 14:11)
• PR !4#17699: feat(Algebra/Group): forward difference oper… (1 message, latest: Oct 31 2024 at 14:10)
• issue !4#5171: Porting note: Missing has nonempty instanc… (4 messages, latest: Oct 31 2024 at 14:10)
• PR !4#9605: feat(Data/Finset & List): Add Lemmas for Sort… (3 messages, latest: Oct 30 2024 at 21:15)
• PR !4#15640: feat: add status of file names (2 messages, latest: Oct 29 2024 at 14:16)
• PR !4#5604: fix: make divisibility semireducible (2 messages, latest: Oct 28 2024 at 14:23)
• PR !4#8960: feat(Fin/Parity): add Fin.even_iff (1 message, latest: Oct 27 2024 at 14:10)
• issue !4#7631: Zero ℕ instance breaks acyclic tactic (1 message, latest: Oct 27 2024 at 14:10)
• PR !4#17338: feat(Matrix): characteristic polynomial of u… (2 messages, latest: Oct 26 2024 at 15:01)
• PR !4#17739: feat(Topology/Order/DenselyOrdered): prove N… (2 messages, latest: Oct 25 2024 at 17:31)
• [PR !4#15786: feat(AlgebraicGeometry/EllipticCurve/NumberF…](topic/PR.20!4.2315786.3A.20feat(AlgebraicGeometry.2FEllipticCurve.2FNumberF.2E.2E.2E.html) (1 message, latest: Oct 24 2024 at 14:10)
• PR !4#15253: test: check commits (2 messages, latest: Oct 23 2024 at 14:34)
• PR !4#9344: feat: Add AddGroup.FG -> Module.Finite ℤ … (1 message, latest: Oct 22 2024 at 14:10)
• issue !4#660: to_additive unable to translate `toOneHom… (2 messages, latest: Oct 21 2024 at 17:47)
• PR !4#15212: feat: Add fundamental theorem of calculus-2 … (2 messages, latest: Oct 21 2024 at 14:10)
• PR !4#14379: feat: the no-whitespace linter (1 message, latest: Oct 20 2024 at 14:10)
• PR !4#5364: feat: wlog ... replacing (1 message, latest: Oct 19 2024 at 14:10)
• PR !4#15578: feat(Function): Fixed points of function f… (1 message, latest: Oct 18 2024 at 14:10)
• issue !4#15785: abel_nf: PANIC at Lean.isLevelMVarAssigna… (1 message, latest: Oct 18 2024 at 14:10)
• PR !4#12473: first translations (4 messages, latest: Oct 17 2024 at 14:12)
• issue !4#10670: Porting note: instance was not necessary … (3 messages, latest: Oct 16 2024 at 14:40)
• PR !4#17360: feat(RingTheory/PowerSeries/WellKnown): chan… (2 messages, latest: Oct 16 2024 at 14:13)
• issue !4#12094: Porting note: unimplemented `dangerous_in… (9 messages, latest: Oct 16 2024 at 03:46)
• PR !4#17499: feat: more lemmas about Fin-indexed produc… (2 messages, latest: Oct 15 2024 at 14:10)
• PR !4#13970: feat: a linter to flag unnecessary uses of `… (5 messages, latest: Oct 14 2024 at 20:39)
• PR !4#17254: chore: prodAssoc as an additive/multiplic… (1 message, latest: Oct 13 2024 at 14:09)
• issue !4#5788: Possible issue in Mathlib.Data.List.Basic (1 message, latest: Oct 13 2024 at 14:09)
• PR !4#13685: feat(Combinatorics): add definitions for net… (1 message, latest: Oct 12 2024 at 14:09)
• issue !4#3844: apply_rules with discharger (2 messages, latest: Oct 12 2024 at 14:09)
• PR !4#15937: test: add autolabelling of PRs in Lean (2 messages, latest: Oct 11 2024 at 15:35)
• issue !4#10759: Porting note: removed @\[simp\] to avoid … (4 messages, latest: Oct 11 2024 at 13:13)
• PR !4#14898: feat: extend the linter against broad imports (2 messages, latest: Oct 10 2024 at 15:41)
• PR !4#17185: feat(CategoryTheory/Monoidal): add `Mon_Clas… (1 message, latest: Oct 09 2024 at 14:10)
• issue !4#10741: simp[LE.le] causes Lean server to crash (3 messages, latest: Oct 08 2024 at 19:10)
• PR !4#14739: feat(Measure): add gcongr lemmas (1 message, latest: Oct 07 2024 at 14:10)
• issue !4#4807: Split MeasureTheory.Integral.FundThmCalculus (1 message, latest: Oct 07 2024 at 14:10)
• PR !4#16305: feat: #guard_exceptions – like `#guard_ms… (2 messages, latest: Oct 06 2024 at 16:26)
• issue !4#7103: Spikes in compilation + maximum resident s… (1 message, latest: Oct 06 2024 at 14:10)
• PR !4#13994: chore(Topology): replace continuity -> fun_prop (1 message, latest: Oct 05 2024 at 14:10)
• PR !4#15294: feat: two Finset lemmas (2 messages, latest: Oct 04 2024 at 14:10)
• PR !4#13207: Lean pr testing 4277 (1 message, latest: Oct 03 2024 at 14:10)
• issue !4#1101: "basic" extensions for positivity tactic (4 messages, latest: Oct 03 2024 at 14:10)
• PR !4#16675: feat(Analysis/BoxIntegral): Add BoxPartition… (1 message, latest: Oct 01 2024 at 14:10)
• issue !4#15865: lift tactic does not respect abbreviations (1 message, latest: Oct 01 2024 at 14:10)
• PR !4#16267: chore(Order/RelIso/Basic): \[s : Setoid α\] … (1 message, latest: Sep 30 2024 at 14:10)
• issue !4#4837: field tactic (1 message, latest: Sep 30 2024 at 14:10)
• issue !4#14652: fin_cases breaks on intervals of Fin (2 messages, latest: Sep 29 2024 at 14:09)
• PR !4#13372: dev: generic replacement (1 message, latest: Sep 28 2024 at 14:10)
• issue !4#172: Automate coercion setup (3 messages, latest: Sep 28 2024 at 14:10)
• PR !4#13256: feat(Analysis/Convex): define half-spaces (1 message, latest: Sep 27 2024 at 14:10)
• issue !4#7178: Lindelöf and paracompact spaces (1 message, latest: Sep 26 2024 at 14:09)
• PR !4#16061: feat(Data/Finsupp/Defs): induction_on_max (4 messages, latest: Sep 25 2024 at 14:50)
• issue !4#1840: #find gives bogus results (3 messages, latest: Sep 25 2024 at 14:10)
• PR !4#13847: feat(EllipticCurve): the universal elliptic … (1 message, latest: Sep 24 2024 at 14:10)
• PR !4#7850: chore(logic): adds aliases for pi instances (2 messages, latest: Sep 23 2024 at 19:04)
• issue !4#7987: Small TODOs to do! (4 messages, latest: Sep 23 2024 at 14:09)
• issue !4#12532: tracking issue for `set_option backward.s… (3 messages, latest: Sep 23 2024 at 07:46)
• [PR !4#13155: feat(NumberTheory/EllipticDivisibilitySequen…](topic/PR.20!4.2313155.3A.20feat(NumberTheory.2FEllipticDivisibilitySequen.2E.2E.2E.html) (1 message, latest: Sep 22 2024 at 14:09)
• PR !4#16250: chore: deprime induction, cases in `Combin… (1 message, latest: Sep 21 2024 at 14:09)
• PR !4#14308: feat(Algebra/Category): Direct construction … (1 message, latest: Sep 20 2024 at 14:10)
• PR !4#12416: chore: remove some cdots (1 message, latest: Sep 19 2024 at 14:09)
• PR !4#10084: feat: the homotopy lifting property for cove… (2 messages, latest: Sep 18 2024 at 14:10)
• issue !4#11554: Shake telling me to replace import that i… (1 message, latest: Sep 18 2024 at 14:10)
• issue !4#7825: Basic topological properties of manifolds (4 messages, latest: Sep 18 2024 at 09:49)
• PR !4#12673: feat: add ContDiff.lipschitzOnWith (2 messages, latest: Sep 18 2024 at 09:49)
• PR !4#7447: feat: reverse for fin tuples (1 message, latest: Sep 16 2024 at 14:10)
• issue !4#7729: simp_arith reification stage should not be… (1 message, latest: Sep 16 2024 at 14:10)
• PR !4#11800: feat : Define KappaLindelöf spaces (4 messages, latest: Sep 16 2024 at 04:52)
• PR !4#15082: refactor(AlgebraicGeometry): Introduce `Sche… (1 message, latest: Sep 14 2024 at 14:09)
• issue !4#3000: lift duplicating a hypothesis (5 messages, latest: Sep 14 2024 at 14:09)
• PR !4#12068: chore: deprecate Ordering.orElse for .then (1 message, latest: Sep 13 2024 at 14:09)
• PR !4#14981: feat(MvPowerSeries.LexOrder): lexicographic … (1 message, latest: Sep 12 2024 at 14:10)
• PR !4#15407: feat(Topology): Set of generic points of gen… (1 message, latest: Sep 11 2024 at 14:09)
• issue !4#10941: Diamond for CompleteBooleanAlgebra of `… (1 message, latest: Sep 11 2024 at 14:09)
• issue !4#10750: Porting note: added to clean up types (3 messages, latest: Sep 10 2024 at 14:09)
• PR !4#14127: feat(CategoryTheory): monoidal structure on … (1 message, latest: Sep 09 2024 at 14:10)
• issue !4#430: tactic porting tracking issue (8 messages, latest: Sep 09 2024 at 10:22)
• PR !4#15129: chore: remove or tweak outdated comments abo… (1 message, latest: Sep 08 2024 at 14:09)
• PR !4#11989: feat: finpartition decomposition of a graph'… (1 message, latest: Sep 07 2024 at 14:09)
• PR !4#5934: feat: port Data.Rat.MetaDefs (1 message, latest: Sep 06 2024 at 14:10)
• issue !4#2018: casesm changed behaviour, does not decon… (4 messages, latest: Sep 06 2024 at 14:10)
• PR !4#12556: tests with presimps (2 messages, latest: Sep 05 2024 at 14:09)
• issue !4#4955: Make inhabit use simp \[nontriviality\] … (3 messages, latest: Sep 01 2024 at 14:09)
• PR !4#13570: Lean pr testing 4379 (1 message, latest: Aug 20 2024 at 14:09)
• issue !4#5026: Tracking issue for unknown simp regressions (2 messages, latest: Aug 20 2024 at 14:09)
• PR !4#10200: feat(GroupTheory/Submonoid/Operations): defi… (1 message, latest: Aug 19 2024 at 14:09)
• issue !4#10611: Todo list for SetTheory/Game (2 messages, latest: Aug 19 2024 at 14:09)
• PR !4#11991: draft: syntax data linter (1 message, latest: Aug 17 2024 at 14:09)
• PR !4#13149: feat: multiple universe polymorphism for the… (1 message, latest: Aug 16 2024 at 14:09)
• PR !4#14266: feat(AlgebraicGeometry): define a pretopolog… (1 message, latest: Aug 15 2024 at 14:09)
• issue !4#9129: mk_iff and ext add too many explicit a… (7 messages, latest: Aug 14 2024 at 23:52)
• PR !4#13543: test: automatically undeprecate (1 message, latest: Aug 11 2024 at 14:09)
• issue !4#11462: to_additive should translate the names … (2 messages, latest: Aug 11 2024 at 14:09)
• PR !4#14270: feat(FermatLastTheorem): Generalize FLT stat… (2 messages, latest: Aug 09 2024 at 17:43)
• PR !4#7649: wip: instead of suppress_compilation, use `… (1 message, latest: Aug 08 2024 at 14:08)
• PR !4#6403: chore: change instance priorities of `Ordered… (1 message, latest: Aug 07 2024 at 14:09)
• PR !4#13755: Test separate addzero mulone (1 message, latest: Aug 06 2024 at 14:09)
• PR !4#13191: Lean pr testing 4272 (1 message, latest: Aug 05 2024 at 14:09)
• PR !4#13079: Lean pr testing 4152 (4 messages, latest: Aug 04 2024 at 14:16)
• PR !4#13891: chore: bump Aesop to enable precompilation (1 message, latest: Aug 03 2024 at 14:09)
• PR !4#13646: Lean pr testing 4223 (1 message, latest: Aug 01 2024 at 14:09)
• ✔ issue !4#754: Set theory notation (4 messages, latest: Jul 31 2024 at 23:18)
• PR !4#13852: perf: skip some typeclasses in TC search (1 message, latest: Jul 31 2024 at 14:09)
• PR !4#12329: feat: algebraic operations on `SeparationQuo… (1 message, latest: Jul 30 2024 at 14:09)
• PR !4#6002: feat(Analysis.SpecialFunctions.Gaussian): add… (1 message, latest: Jul 29 2024 at 14:09)
• issue !4#11622: simps generates lemmas for propositions (1 message, latest: Jul 29 2024 at 14:09)
• issue !4#11299: Slow unification of `ContinuousLinearMap…. (3 messages, latest: Jul 29 2024 at 04:35)
• PR !4#14799: feat(Analysis/MeanInequalities): Weighted QM… (1 message, latest: Jul 28 2024 at 14:08)
• issue !4#9303: apply_fun: "internal exception: postpone" (1 message, latest: Jul 28 2024 at 14:08)
• PR !4#13092: chore: drop order dependency from Data.Nat.Defs (3 messages, latest: Jul 27 2024 at 16:55)
• PR !4#10524: chore(Data/IsROrC): make proper_isROrC an … (1 message, latest: Jul 26 2024 at 14:09)
• PR !4#6079: fix: deduplicate variables (1 message, latest: Jul 25 2024 at 14:09)
• issue !4#4836: linear_combination for inequalities (3 messages, latest: Jul 25 2024 at 14:09)
• PR !4#9146: feat(Data/ZMod/Defs): Topological structure o… (2 messages, latest: Jul 24 2024 at 14:14)
• PR !4#11100: feat(CategoryTheory/Limits): add `Functor.ma… (1 message, latest: Jul 23 2024 at 14:08)
• issue !4#1074: to_additive feature requests / issues (2 messages, latest: Jul 23 2024 at 14:08)
• issue !4#5028: Tracking issue for mysterious slowdowns (2 messages, latest: Jul 22 2024 at 14:09)
• PR !4#14495: feat(LegendreSymbol/AddCharacter): std add c… (1 message, latest: Jul 19 2024 at 14:09)
• PR !4#11415: chore(Init/Logic): remove Commutative and … (1 message, latest: Jul 18 2024 at 14:08)
• PR !4#14034: feat(Order/WellFounded): well-founded of str… (1 message, latest: Jul 17 2024 at 14:09)
• PR !4#13899: feat: The diagonal of a finset (2 messages, latest: Jul 16 2024 at 14:10)
• PR !4#4197: feat/refactor: redefinition of homology + der… (1 message, latest: Jul 15 2024 at 14:08)
• PR !4#13010: feat: relax universe constraint is stoneCech… (3 messages, latest: Jul 14 2024 at 15:33)
• issue !4#5164: sometimes rw worked in mathlib3 but we h… (3 messages, latest: Jul 14 2024 at 14:15)
• PR !4#10345: feat(Algebra.Module.Zlattice): Add Voronoi D… (2 messages, latest: Jul 13 2024 at 14:08)
• PR !4#10332: feat(Topology/Sets): define regular open set… (1 message, latest: Jul 12 2024 at 14:09)
• PR !4#12313: feat: "outer product" of functions that tend… (1 message, latest: Jul 11 2024 at 14:09)
• issue !4#6336: Add SubringClass.toNonUnitalSubringClass… (2 messages, latest: Jul 11 2024 at 14:09)
• PR !4#10796: feat(Tactic/Positivity): non-negativity of f… (1 message, latest: Jul 10 2024 at 14:09)
• [PR !4#12290: feat(MeasureTheory/Integral/linearRieszMarko…](topic/PR.20!4.2312290.3A.20feat(MeasureTheory.2FIntegral.2FlinearRieszMarko.2E.2E.2E.html) (1 message, latest: Jul 08 2024 at 14:09)
• PR !4#10594: feat: fun_trans function transformation ta… (1 message, latest: Jul 07 2024 at 14:09)
• issue !4#13998: duplicated definition of the pullback fun… (1 message, latest: Jul 07 2024 at 14:09)
• PR !4#12010: feat: the category of Hopf algebras (1 message, latest: Jul 06 2024 at 14:08)
• PR !4#8585: chore: bench lean4#2944 (1 message, latest: Jul 05 2024 at 14:08)
• PR !4#11103: chore(ModelTheory): rename BoundedFormula … (1 message, latest: Jul 04 2024 at 14:09)
• PR !4#6307: refactor(CategoryTheory/Monoidal): add whiske… (1 message, latest: Jul 03 2024 at 14:09)
• PR !4#9111: feat(LinearAlgebra/CliffordAlgebra): port Spi… (10 messages, latest: Jul 02 2024 at 14:17)
• PR !4#7849: testing: bench nightly testing for lean4#2712 (2 messages, latest: Jul 01 2024 at 14:08)
• PR !4#13627: chore(Data/Num): migrate from bit0/bit1 (1 message, latest: Jun 30 2024 at 14:08)
• PR !4#13428: feat (RingTheory/Binomial) : Multichoose lem… (3 messages, latest: Jun 29 2024 at 22:45)
• PR !4#7632: chore (GroupTheory.Perm.Basic): remove uneces… (1 message, latest: Jun 28 2024 at 14:09)
• PR !4#13817: chore: correct CompletelyNormalSpace API t… (1 message, latest: Jun 27 2024 at 14:08)
• PR !4#13810: feat(Combinatorics/SimpleGraph): add `Fintyp… (1 message, latest: Jun 26 2024 at 14:08)
• PR !4#7991: feat(Topology/Algebra/Group): Normal open nei… (2 messages, latest: Jun 25 2024 at 14:08)
• PR !4#11968: feat: RefinedDiscrTree (1 message, latest: Jun 24 2024 at 14:08)
• PR !4#7892: New Tactic: differentiability (1 message, latest: Jun 23 2024 at 14:08)
• PR !4#4771: feat: Backtrack minimize (1 message, latest: Jun 22 2024 at 14:08)
• PR !4#6195: chore(RingTheory/TensorProduct): golf the `mu… (1 message, latest: Jun 21 2024 at 14:08)
• PR !4#13507: feat(LightProfinite): a sequential limit of … (1 message, latest: Jun 20 2024 at 14:08)
• PR !4#12679: perf(NumberTheory/RamificationInertia): spee… (1 message, latest: Jun 18 2024 at 14:08)
• PR !4#12181: lint also let vs have (2 messages, latest: Jun 17 2024 at 15:24)
• issue !4#11229: Porting note: deprecated (1 message, latest: Jun 17 2024 at 14:09)
• [PR !4#9820: feat(RingTheory/GradedAlgebra/HomogeneousIdea…](topic/PR.20!4.239820.3A.20feat(RingTheory.2FGradedAlgebra.2FHomogeneousIdea.2E.2E.2E.html) (1 message, latest: Jun 16 2024 at 14:40)
• issue !4#11692: Manual priority changes for performance (1 message, latest: Jun 16 2024 at 14:40)
• PR !4#12748: feat(Probability/Distributions): add result … (1 message, latest: Jun 15 2024 at 14:08)
• [issue !4#9168: second countable spaces are Lindelöf (this…](topic/issue.20!4.239168.3A.20second.20countable.20spaces.20are.20Lindel.C3.B6f.20(this.2E.2E.2E.html) (2 messages, latest: Jun 15 2024 at 14:08)
• PR !4#7516: perf: use abbrev to prevent unifying useles… (2 messages, latest: Jun 14 2024 at 14:10)
• [PR !4#8793: feat(RepresentationTheory/GroupCohomology/Hil…](topic/PR.20!4.238793.3A.20feat(RepresentationTheory.2FGroupCohomology.2FHil.2E.2E.2E.html) (2 messages, latest: Jun 13 2024 at 14:08)
• issue !4#9258: Investigate a potential "filter-indexed" v… (2 messages, latest: Jun 13 2024 at 14:08)
• issue !4#11180: Porting note: removed @\[pp_nodot\] (2 messages, latest: Jun 12 2024 at 17:46)
• PR !4#9398: feat: port itauto from lean 3 (1 message, latest: Jun 12 2024 at 14:08)
• PR !4#6042: feat(LinearAlgebra/Matrix/SVD): Singular Valu… (2 messages, latest: Jun 11 2024 at 14:09)
• PR !4#4960: chore: use open scoped (1 message, latest: Jun 10 2024 at 14:09)
• issue !4#13362: cc tactic can't unify def-eq instances … (1 message, latest: Jun 10 2024 at 14:09)
• PR !4#13278: chore(GradedAlgebra.HomogeneousLocalization)… (1 message, latest: Jun 09 2024 at 14:09)
• PR !4#13311: feat: Add lemmas about finite products of me… (1 message, latest: Jun 08 2024 at 14:09)
• PR !4#10609: feat: SmallSet.{u} α - sets with u-small… (2 messages, latest: Jun 07 2024 at 15:18)
• PR !4#8362: feat(Asymptotics): define ReflectsGrowth (2 messages, latest: Jun 06 2024 at 15:21)
• issue !4#7082: should Nat.odd_iff_not_even be a simp? (3 messages, latest: Jun 06 2024 at 14:09)
• PR !4#12093: feat: tweak the definition of semicontinuity… (1 message, latest: Jun 05 2024 at 14:09)
• issue !4#12228: slow typeclass synthesis: takes 19000 hea… (5 messages, latest: Jun 05 2024 at 10:00)
• PR !4#12629: feat(Topology/ContinuousFunction/Bounded): a… (1 message, latest: Jun 04 2024 at 14:09)
• PR !4#12728: feat(CategoryTheory): the localized category… (1 message, latest: Jun 03 2024 at 14:09)
• PR !4#10159: Linear programming according to Antoine Cham… (1 message, latest: Jun 02 2024 at 14:08)
• PR !4#11820: feat(Algebra/Star/Unitary): add unitarySubgroup (1 message, latest: Jun 01 2024 at 14:09)
• PR !4#10444: doc(IsROrC): expand the docstring (1 message, latest: May 31 2024 at 14:09)
• PR !4#11283: (feat:ModelTheory/Satisfiability): Define th… (1 message, latest: May 29 2024 at 14:08)
• issue !4#6937: exact? doesn't close the goal (2 messages, latest: May 29 2024 at 14:08)
• PR !4#11243: feat: Density of a finset (1 message, latest: May 28 2024 at 14:09)
• issue !4#6814: allow Cache use alternative mirror URL v… (2 messages, latest: May 28 2024 at 14:09)
• PR !4#10436: feat: Modular Character of a locally compact… (1 message, latest: May 27 2024 at 14:09)
• PR !4#7351: feat(Topology/Algebra/Order): extend function… (3 messages, latest: May 26 2024 at 14:08)
• PR !4#5133: feat: IntermediateField adjoin syntax for set… (1 message, latest: May 23 2024 at 14:08)
• PR !4#8100: feat: add support for other types in norm_num (1 message, latest: May 22 2024 at 14:08)
• issue !4#10064: The roots of a Lie algebra are a root sys… (1 message, latest: May 22 2024 at 14:08)
• PR !4#12769: feat: Fourier transform of iterated derivatives (1 message, latest: May 21 2024 at 14:09)
• PR !4#7883: chore (Order.Ring.Defs): rings comes before o… (1 message, latest: May 20 2024 at 14:08)
• PR !4#12768: feat: two equiv involving Associates and `… (3 messages, latest: May 19 2024 at 14:39)
• issue !4#10694: Porting note: added to speed up elaboration (1 message, latest: May 19 2024 at 14:09)
• PR !4#7534: feat: Add `measurableEquiv_nat_bool_of_counta… (2 messages, latest: May 17 2024 at 14:09)
• PR !4#11175: feat(ModelTheory/Substructures): define equi… (1 message, latest: May 16 2024 at 14:08)
• PR !4#9726: feat: define AddConstEquiv (3 messages, latest: May 15 2024 at 14:10)
• issue !4#11119: Porting note: @\[simp\] removed (1 message, latest: May 15 2024 at 14:09)
• [PR !4#9433: feat(AlgebraicGeometry/EllipticCurve/Jacobian…](topic/PR.20!4.239433.3A.20feat(AlgebraicGeometry.2FEllipticCurve.2FJacobian.2E.2E.2E.html) (1 message, latest: May 14 2024 at 14:08)
• Topic names (6 messages, latest: May 13 2024 at 17:10)
• PR !4#11195: chore: showcase deprecation tool (8 messages, latest: May 13 2024 at 14:34)
• PR !4#10428: feat: add simp_digits tactic (1 message, latest: May 12 2024 at 14:09)
• PR !4#9572: chore: adaptations for leanprover/lean4#3151 (1 message, latest: May 11 2024 at 14:08)
• PR !4#10230: chore: Delete some orphaned porting notes an… (4 messages, latest: May 09 2024 at 14:39)
• PR !4#6317: refactor(Data/Finsupp/Defs): make Finsupp.sin… (1 message, latest: May 07 2024 at 14:08)
• PR !4#10844: feat(UniformConvergenceTopology): prove `Com… (2 messages, latest: May 05 2024 at 15:14)
• PR !4#12111: feat: exhibit lower adjoint for smallSets, u… (1 message, latest: May 04 2024 at 14:08)
• PR !4#10179: feat(Data/Nat/BitVec/Lemmas) toFin_intCast… (1 message, latest: May 03 2024 at 14:08)
• issue !4#12231: slow typeclass synthesis: takes 15000 hea… (1 message, latest: May 03 2024 at 14:08)
• PR !4#7076: feat: define measure zero subsets of a manifold (1 message, latest: May 02 2024 at 14:08)
• issue !4#10691: Porting note: was rw (1 message, latest: May 02 2024 at 14:08)
• PR !4#9734: feat: Binary entropy (2 messages, latest: May 01 2024 at 15:12)
• issue !4#8875: linarith can no longer solve a simple problem (1 message, latest: May 01 2024 at 14:08)
• PR !4#9460: Update lean-toolchain for testing https://git… (1 message, latest: Apr 30 2024 at 14:09)
• issue !4#7217: Linter / Formatter Wishlist (1 message, latest: Apr 30 2024 at 14:09)
• PR !4#3808: feat: #formalize, backed by a choice of LLMs (1 message, latest: Apr 28 2024 at 14:08)
• PR !4#12065: Update lean-toolchain for testing https://gi… (1 message, latest: Apr 26 2024 at 14:08)
• PR !4#4775: feat: SubExpr utilities (1 message, latest: Apr 25 2024 at 14:09)
• PR !4#7445: perf: improve some instances in MonoidAlgebra (1 message, latest: Apr 24 2024 at 14:08)
• PR !4#9819: fg graded ring (1 message, latest: Apr 21 2024 at 14:08)
• is the bot dead (8 messages, latest: Apr 20 2024 at 23:57)
• [PR !4#9367: feat(SuccPred): {succ,pred}{min,max}](topic/PR.20!4.239367.3A.20feat(SuccPred).3A.20.7Bsucc.2Cpred.7D.7Bmin.2Cmax.7D.html) (1 message, latest: Mar 08 2024 at 14:07)
• PR !4#10661: feat: Positivity extension for Bochner integral (1 message, latest: Mar 06 2024 at 14:06)
• PR !4#10985: refactor(Order): rename cInf -> csInf and cS… (1 message, latest: Mar 05 2024 at 14:06)
• PR !4#9320: chore: Golf terminal simp calls (1 message, latest: Mar 04 2024 at 14:07)
• PR !4#4109: feat: run library_search when the cursor is a… (1 message, latest: Mar 03 2024 at 14:06)
• PR !4#10836: feat: Jensen's inequality for the entropy (2 messages, latest: Mar 02 2024 at 14:34)
• PR !4#6548: refactor: make charP_to_charZero an instance (1 message, latest: Mar 01 2024 at 14:06)
• issue !4#5127: ∃ x ∈ s, P x parses differently (3 messages, latest: Feb 28 2024 at 18:28)
• PR !4#7569: refactor(LinearAlgebra/QuadraticForm) : Gener… (1 message, latest: Feb 28 2024 at 14:06)
• PR !4#10004: feat: interval version of parametric integra… (1 message, latest: Feb 26 2024 at 14:06)
• PR !4#6590: feat: composition of LinearPMaps (1 message, latest: Feb 25 2024 at 14:06)
• PR !4#10283: feat(Data/Fin/OrderHom): Extend lemmas to si… (1 message, latest: Feb 24 2024 at 14:05)
• issue !4#554: set as a TermElab (1 message, latest: Feb 24 2024 at 14:05)
• PR !4#6135: feat(AlgebraicGeometry/Morphisms): closed imm… (1 message, latest: Feb 22 2024 at 14:06)
• PR !4#6617: feat(ModelTheory): Lefschetz principle for Al… (1 message, latest: Feb 21 2024 at 14:06)
• PR !4#9101: chore: More golfing (1 message, latest: Feb 20 2024 at 14:06)
• PR !4#8298: feat: LocallyConstant as a condensed set (1 message, latest: Feb 19 2024 at 14:06)
• issue !4#10071: The Chevalley-Serre relations define simp… (1 message, latest: Feb 19 2024 at 14:06)
• PR !4#7596: feat: covering maps from properly discontinuo… (2 messages, latest: Feb 18 2024 at 14:05)
• PR !4#2533: feat: port initial/principal segment lemmas (1 message, latest: Feb 17 2024 at 14:05)
• PR !4#9978: chore(FieldTheory/KummerExtension): move some… (1 message, latest: Feb 16 2024 at 14:06)
• issue !4#7752: irreducible_def incorrectly jump-to-defi… (1 message, latest: Feb 16 2024 at 14:06)
• PR !4#7087: fix: remove a heartbeat bump (2 messages, latest: Feb 15 2024 at 20:35)
• PR !4#9872: feat: version of the extreme value theorem wi… (1 message, latest: Feb 15 2024 at 14:05)
• issue !4#1212: filename Clear!.lean contains illegal char… (4 messages, latest: Feb 15 2024 at 03:16)
• PR !4#7907: feat: introduce NthRoot notation class (1 message, latest: Feb 13 2024 at 14:06)
• issue !4#10267: Drop DecidableEq in Module.DualBases (1 message, latest: Feb 12 2024 at 14:05)
• PR !4#8568: refactor(RingTheory/Ideal/Operation): prime a… (1 message, latest: Feb 11 2024 at 14:06)
• PR !4#9251: feat(cone/caratheodory): add caratheodory the… (1 message, latest: Feb 10 2024 at 14:05)
• PR !4#2605: chore: better error message in linarith (1 message, latest: Feb 08 2024 at 14:05)
• issue !4#7450: zify! tactic (1 message, latest: Feb 08 2024 at 14:05)
• PR !4#7873: perf: reorder extends and remove some `with… (3 messages, latest: Feb 06 2024 at 13:50)
• PR !4#8885: feat: use @[csimp] to use exponentiation by r… (1 message, latest: Feb 04 2024 at 14:05)
• PR !4#7478: feat(Topology/MetricSpace/Congruence): define… (2 messages, latest: Feb 03 2024 at 16:58)
• PR !4#7520: perf: build up more instances before Polynomi… (1 message, latest: Feb 02 2024 at 14:05)
• PR !4#9923: chore: split CategoryTheory.FinCategory (1 message, latest: Feb 01 2024 at 14:05)
• PR !4#7165: feat: golf using the set_like tactic (1 message, latest: Jan 31 2024 at 14:05)
• issue !4#3722: Redefine Matrix.unitaryGroup.toGL etc (1 message, latest: Jan 31 2024 at 14:05)
• PR !4#6330: chore: make some instance about Sub...Class… (2 messages, latest: Jan 30 2024 at 14:05)
• issue !4#5464: Generalize manifold structure on a vector … (2 messages, latest: Jan 30 2024 at 14:05)
• PR !4#9837: feat: Generalize results of `CanonicalEmbeddi… (1 message, latest: Jan 29 2024 at 14:05)
• issue !4#5499: Introduce a typeclass for a `ModelWithCorn… (1 message, latest: Jan 28 2024 at 14:05)
• PR !4#8661: feat(CategoryTheory/Sites): descent of sheaves (1 message, latest: Jan 27 2024 at 14:05)
• issue !4#4998: anonymous constructor notation does not ma… (1 message, latest: Jan 26 2024 at 14:05)
• PR !4#7560: perf (GroupTheory.SubMonoid): direct inherita… (1 message, latest: Jan 25 2024 at 14:05)
• PR !4#8420: fix: improvements I noticed when teaching (1 message, latest: Jan 23 2024 at 14:05)
• PR !4#6262: refactor: do not allow nsmul and zsmul to… (1 message, latest: Jan 22 2024 at 14:05)
• PR !4#8218: feat: Unfold widget (2 messages, latest: Jan 21 2024 at 16:02)
• PR !4#5593: Update lakefile with scripts for import gener… (1 message, latest: Jan 20 2024 at 14:05)
• issue !4#7339: Error on non-Debian Linux distros and VS C… (1 message, latest: Jan 20 2024 at 14:05)
• PR !4#8612: feat(Data/Nat/Choose): add Choose.lucas (1 message, latest: Jan 19 2024 at 14:05)
• PR !4#7791: feat(LinearAlgebra/Matrix): define projective… (5 messages, latest: Jan 19 2024 at 12:32)
• PR !4#7851: Definition and basic properties of closed fun… (1 message, latest: Jan 18 2024 at 14:05)
• issue !4#8828: Implement norm_num for rpow (2 messages, latest: Jan 17 2024 at 14:05)
• PR !4#6692: Disjoint indexed union of local homeomorphisms (1 message, latest: Jan 16 2024 at 14:05)
• PR !4#9490: feat(GroupTheory/GroupAction): define MulActi… (2 messages, latest: Jan 15 2024 at 14:25)
• PR !4#8961: refactor: use the coinduced topology on ULift (1 message, latest: Jan 14 2024 at 14:05)
• issue !4#5878: Normed rings with summable geometric series (1 message, latest: Jan 13 2024 at 14:05)
• PR !4#8638: refactor: noncommutative tensor product (1 message, latest: Jan 12 2024 at 14:05)
• issue !4#380: delta-derive handler (1 message, latest: Jan 11 2024 at 14:05)
• PR !4#5995: feat: add APIs about Quotient.choice (1 message, latest: Jan 10 2024 at 14:05)
• PR !4#6183: chore: remove normalizeScaleRoots (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)
• 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)
• PR !4#290: feat: profunctor optics (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)
• 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)
• PR !4#7101: feat: self_le_pow (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)
• PR !4#6268: Fixups to #3838 (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#6859: TryLean4Bundle: Windows Bundle Creator (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)
• PR !4#5383: feat: define Bitvec constants for -1, INT_MIN… (1 message, latest: Sep 13 2023 at 14:03)
• PR !4#282: feat: deriving optics (1 message, latest: Sep 12 2023 at 14:04)
• PR !4#6808: feat: vertex replacement (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)
• PR !4#5745: feat: a tactic to consume type annotations, a… (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)
• 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: May 02 2025 at 03:31 UTC