Commits

Breadcrumbs

History for

onmaster

User selector

All users

Datepicker

All time

Commit History

Commits on Sep 4, 2025

• chore: add `-v` flag to `lake update` in CI (#29338)

  Show description for 75b9e12
  kim-em

  committed
  75b9e12

  Copy full SHA for 75b9e12

Commits on Sep 3, 2025

• feat: deprecated module automation (#24917)

  Show description for afb3068
  

  adomani

  and

  grunweg

  committed
  afb3068

  Copy full SHA for afb3068

Commits on Sep 1, 2025

• feat: rational approximations for square roots of natural numbers (#29193)

  kim-em

  committed
  1c58764

  Copy full SHA for 1c58764

• feat: statement only of Chudnovsky's formula for pi (#29170)

  Show description for 3fd1d01
  kim-em

  committed
  3fd1d01

  Copy full SHA for 3fd1d01

Commits on Aug 31, 2025

• doc: hyphenize "well-defined" where applicable (#29140)

  Show description for a155dd5
  harahu

  committed
  a155dd5

  Copy full SHA for a155dd5

• chore(scripts): update nolints.json (#29152)

  Show description for c73d160
  

  leanprover-community-bot-assistant

  and

  leanprover-community-bot

  committed
  c73d160

  Copy full SHA for c73d160

Commits on Aug 30, 2025

• feat(Algebra/Order/Group/Pointwise/Interval): rename `Set.mapsTo'` to `Set.mapsTo_iff_image_subset` (#27551)

  Show description for c20f6c5
  Paul-Lez

  committed
  c20f6c5

  Copy full SHA for c20f6c5

Commits on Aug 29, 2025

• chore: minimize `fun_prop` imports (#29078)

  Show description for 7f2eaff
  grunweg

  committed
  7f2eaff

  Copy full SHA for 7f2eaff

Commits on Aug 28, 2025

• chore(Matroid): move to `Combinatorics` (#29008)

  Show description for b60d321
  YaelDillies

  committed
  b60d321

  Copy full SHA for b60d321

• feat(NormNum): add extension for `Nat.ModEq`, `Int.ModEq` (#29044)

  Show description for 37187ea
  yury-harmonic

  committed
  37187ea

  Copy full SHA for 37187ea

• feat: `measurable_from_prod_countable_right` (#28547)

  YaelDillies

  committed
  4ee73c0

  Copy full SHA for 4ee73c0

• feat: `mon_tauto`, a simp set to prove tautologies about a monoid object (#26057)

  Show description for 41c7044
  

  YaelDillies

  and

  erdOne

  committed
  41c7044

  Copy full SHA for 41c7044

• feat(Tactic/FieldSimp): rewrite for performance and robustness (#28658)

  Show description for d60062a
  

  hrmacbeth

  and

  grunweg

  committed
  d60062a

  Copy full SHA for d60062a

Commits on Aug 27, 2025

• chore: move most of Data/Matrix to LinearAlgebra (#28966)

  Show description for 1cd593f
  grunweg

  committed
  1cd593f

  Copy full SHA for 1cd593f

• feat(Topology): R1 spaces are quasisober (#26358)

  Show description for 50de20e
  plp127

  committed
  50de20e

  Copy full SHA for 50de20e

Commits on Aug 24, 2025

• chore(scripts): update nolints.json (#28827)

  Show description for f02623d
  leanprover-community-bot

  committed
  f02623d

  Copy full SHA for f02623d

Commits on Aug 22, 2025

• chore(downstream_dashboard.py): Allow empty workflow list (#28366)

  Show description for 5dc0648
  BoltonBailey

  committed
  5dc0648

  Copy full SHA for 5dc0648

• CI: list the projects I maintain (#28655)

  Show description for a3660d1
  YaelDillies

  committed
  a3660d1

  Copy full SHA for a3660d1

Commits on Aug 21, 2025

• chore: bench report documentation (#28734)

  Show description for ea5d04e
  Kha

  committed
  ea5d04e

  Copy full SHA for ea5d04e

Commits on Aug 20, 2025

• chore: prune branches in fork not used in PRs (#28657)

  Show description for fe53a10
  Garmelon

  committed
  fe53a10

  Copy full SHA for fe53a10

• refactor(Tactic/NormNum): expose the derive API for known expressions directly (#28621)

  Show description for 4cb1b3c
  eric-wieser

  committed
  4cb1b3c

  Copy full SHA for 4cb1b3c

Commits on Aug 19, 2025

• chore: upload bench outputs (#28634)

  Show description for fec9776
  Kha

  committed
  fec9776

  Copy full SHA for fec9776

• chore: include only master branch when migrating to fork (#28643)

  Show description for 9b71cdc
  Garmelon

  committed
  9b71cdc

  Copy full SHA for 9b71cdc

• chore: deprecate `Std.HashMap.mapVal` and `Std.Data.HashMap` module (#28611)

  Show description for 763501d
  thorimur

  committed
  763501d

  Copy full SHA for 763501d

Commits on Aug 18, 2025

• doc: some missing docstrings (#28585)

  YaelDillies

  committed
  55affb0

  Copy full SHA for 55affb0

Commits on Aug 17, 2025

• refactor: deprecate all the material in the CGT repo (#28063)

  Show description for 8939bd7
  vihdzp

  committed
  8939bd7

  Copy full SHA for 8939bd7

• chore: remove Cardinal imports from GroupTheory.GroupAction.Quotient (#28529)

  Ruben-VandeVelde

  committed
  26a0305

  Copy full SHA for 26a0305

• chore(scripts): update nolints.json (#28535)

  Show description for 98731b9
  leanprover-community-bot

  committed
  98731b9

  Copy full SHA for 98731b9

Commits on Aug 15, 2025

• chore: add the Brownian motion project to downstream_repos.yml (#28459)

  RemyDegenne

  committed
  797fe7f

  Copy full SHA for 797fe7f

• chore: bump toolchain to v4.23.0-rc2 (#28454)

  kim-em

  authored
  90c0e18

  Copy full SHA for 90c0e18

Commits on Aug 13, 2025

• fix: update bench config to not use make (#28348)

  Show description for 20320fa
  bryangingechen

  committed
  20320fa

  Copy full SHA for 20320fa

• refactor: Add norm_num machinery for NNRat (#9915)

  Show description for 69035af
  

  plp127

  and

  eric-wieser

  committed
  69035af

  Copy full SHA for 69035af

• script: Add downstream project dashboard (#26048)

  Show description for 4f8e2e1
  Vierkantor

  committed
  4f8e2e1

  Copy full SHA for 4f8e2e1

Commits on Aug 12, 2025

• chore: fix spelling mistakes (#28273)

  euprunin

  committed
  03b550a

  Copy full SHA for 03b550a

Commits on Aug 11, 2025

• chore(scripts): update nolints.json (#28214)

  Show description for 0025b4a
  leanprover-community-bot

  committed
  0025b4a

  Copy full SHA for 0025b4a

Pagination

Previous

Next