Commits

Breadcrumbs

History for

onmaster

User selector

All users

All time

Commit History

Commits on Feb 17, 2026

• chore: bump toolchain to v4.29.0-rc1 (#35459)

  Show description for 33a7291
  

  6 peoplecommitted
  33a7291

  Copy full SHA for 33a7291

Commits on Feb 6, 2026

• refactor(CategoryTheory): remove `HasForget` (#34741)

  dagurtomas

  committed
  045ac40

  Copy full SHA for 045ac40

Commits on Jan 30, 2026

• feat(Condensed): the functor from light profinite sets preserves effective epimorphisms (#32627)

  Show description for 76befbe
  

  3 peoplecommitted
  76befbe

  Copy full SHA for 76befbe

Commits on Jan 29, 2026

• chore(*): use `apply +allowSynthFailures` syntax (#34525)

  Show description for ad65e18
  Vierkantor

  committed
  ad65e18

  Copy full SHA for ad65e18

Commits on Jan 27, 2026

• chore: misc `fun_prop` golfs (#34448)

  grunweg

  committed
  6ab7b9e

  Copy full SHA for 6ab7b9e

Commits on Jan 19, 2026

• chore: remove some `backward.proofsInPublic` (#33595)

  Show description for e0bd51b
  JovanGerb

  committed
  e0bd51b

  Copy full SHA for e0bd51b

Commits on Jan 5, 2026

• chore: remove unnecessary @[expose] from public sections (#33581)

  Show description for 959c852
  kim-em

  committed
  959c852

  Copy full SHA for 959c852

Commits on Dec 26, 2025

• doc(Condensed): fix file refs (#33263)

  Show description for e126ddc
  harahu

  committed
  e126ddc

  Copy full SHA for e126ddc

Commits on Dec 23, 2025

• chore(CategoryTheory): deprecate cartesian closed categories API (#33228)

  dagurtomas

  committed
  9c7dee5

  Copy full SHA for 9c7dee5

Commits on Dec 19, 2025

• chore: remove backward.privateInPublic from lakefile (#33034)

  Show description for 03dd195
  

  3 peoplecommitted
  03dd195

  Copy full SHA for 03dd195

Commits on Dec 18, 2025

• refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure (#26446)

  Show description for a2089ae
  

  joelriou

  and

  pre-commit-ci-lite[bot]

  committed
  a2089ae

  Copy full SHA for a2089ae

Commits on Dec 17, 2025

• chore(misc): fix whitespace (#33004)

  Show description for 0a79887
  harahu

  committed
  0a79887

  Copy full SHA for 0a79887

Commits on Dec 16, 2025

• chore: move `set_option backward.proofsInPublic` to where it is needed (#32934)

  Show description for fcad271
  kim-em

  committed
  fcad271

  Copy full SHA for fcad271

Commits on Dec 15, 2025

• chore(Condensed): fix whitespace (#32905)

  Show description for bfbfe1f
  harahu

  committed
  bfbfe1f

  Copy full SHA for bfbfe1f

Commits on Dec 13, 2025

• chore: use `Category*` everywhere (#32842)

  Show description for dd97bd1
  robin-carlier

  committed
  dd97bd1

  Copy full SHA for dd97bd1

Commits on Dec 9, 2025

• chore: remove "non-breaking spaces" (#32587)

  Show description for 790901a
  loefflerd

  committed
  790901a

  Copy full SHA for 790901a

Commits on Dec 5, 2025

• fix(Condensed/Explicit): typo in docstring (#32478)

  dagurtomas

  committed
  ae8e527

  Copy full SHA for ae8e527

Commits on Dec 1, 2025

• doc(Condensed): make ASCII art diagrams align more nicely in docs (#32221)

  Show description for 934dbd5
  dagurtomas

  committed
  934dbd5

  Copy full SHA for 934dbd5

Commits on Nov 30, 2025

• doc: use file refs when referencing files (#32025)

  Show description for e7d2a0c
  harahu

  committed
  e7d2a0c

  Copy full SHA for e7d2a0c

Commits on Nov 28, 2025

• chore(CategoryTheory): generalize `EqualizerCondition.bijective_mapToEqualizer_pullback` to abstract pullback cones (#31906)

  dagurtomas

  committed
  f8c8067

  Copy full SHA for f8c8067

• chore(CategoryTheory): move `Closed` directory into `Monoidal` (#30771)

  dagurtomas

  committed
  e4f6915

  Copy full SHA for e4f6915

Commits on Nov 25, 2025

• feat(Condensed): characterize internal projectivity (#31368)

  dagurtomas

  committed
  e2b0176

  Copy full SHA for e2b0176

Commits on Nov 24, 2025

• feat(Condensed): closed symmetric monoidal structure on light condensed modules (#25797)

  dagurtomas

  committed
  7d9368d

  Copy full SHA for 7d9368d

• feat(Condensed): cartesian monoidal functor LightProfinite -> LightCondSet (#30800)

  dagurtomas

  committed
  d1de275

  Copy full SHA for d1de275

• feat(Condensed): constructions for light condensed objects can be done in an equivalent small category (#30827)

  dagurtomas

  committed
  5e87abc

  Copy full SHA for 5e87abc

Commits on Nov 19, 2025

• chore: move Mathlib to the module system (#31786)

  Show description for 6a54a80
  

  kim-em

  and

  Kha

  committed
  6a54a80

  Copy full SHA for 6a54a80

Commits on Nov 6, 2025

• chore(*): use autoparams and `fun_prop` (#31317)

  urkud

  committed
  efdba04

  Copy full SHA for efdba04

Commits on Oct 28, 2025

• chore(CategoryTheory/EssentiallySmall): adding an instance (#30534)

  Show description for 807c884
  joelriou

  committed
  807c884

  Copy full SHA for 807c884

Commits on Oct 26, 2025

• chore(Condensed): fix typo (#30846)

  Show description for 2108383
  

  yonggyuchoimath

  and

  pre-commit-ci-lite[bot]

  committed
  2108383

  Copy full SHA for 2108383

Commits on Oct 23, 2025

• doc: Cartesian-closed -> Cartesian closed (#30777)

  dagurtomas

  committed
  c03073a

  Copy full SHA for c03073a

Commits on Oct 21, 2025

• doc: fix recurring instances of "this files" (#30719)

  Show description for 24c5360
  harahu

  committed
  24c5360

  Copy full SHA for 24c5360

Commits on Oct 13, 2025

• doc: fix repeated words in documentation (#30479)

  harahu

  committed
  c7448d4

  Copy full SHA for c7448d4

Commits on Sep 27, 2025

• doc: hyphenate attributive compound adjectives ending in "preserving" (#29301)

  Show description for 2a54fc0
  harahu

  committed
  2a54fc0

  Copy full SHA for 2a54fc0

Commits on Sep 16, 2025

• chore: remove redundant `have`:s in `Computability/`, `Combinatorics/`, `Condensed/`, `Data/Nat/` and `Data/PNat/` (#28996)

  euprunin

  committed
  360066c

  Copy full SHA for 360066c

Commits on Sep 15, 2025

• chore(Condensed): introduce an abbrev for the equivalence of light condensed sets with a category of sheaves on a small site (#25795)

  dagurtomas

  committed
  5d58cf7

  Copy full SHA for 5d58cf7

Pagination

Previous

Next