Commits

Breadcrumbs

History for

onmaster

User selector

All users

All time

Commit History

Commits on Mar 3, 2026

• chore: remove `set_option backward.isDefEq.respectTransparency false` (#36021)

  Show description for 33a07fa
  kim-em

  committed
  33a07fa

  Copy full SHA for 33a07fa

• chore: add/remove `set_option backward` after moving to `v4.29.0-rc3` (#35952)

  Show description for 6fcaafd
  kim-em

  committed
  6fcaafd

  Copy full SHA for 6fcaafd

Commits on Feb 24, 2026

• chore: bump toolchain to v4.29.0-rc2 (#35708)

  kim-em

  committed
  0c08ce9

  Copy full SHA for 0c08ce9

Commits on Feb 18, 2026

• fix(Dynamics/BirkhoffSum): birkhoffAverage_of_comp_eq only needs AddCommMonoid (#35307)

  samueloettl

  committed
  2c5d229

  Copy full SHA for 2c5d229

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 13, 2026

• chore: run `lake shake --add-public --keep-implied --keep-prefix --fix` (#34511)

  kim-em

  committed
  af5e2dd

  Copy full SHA for af5e2dd

Commits on Jan 30, 2026

• chore: golf using fun_prop (#34441)

  Show description for 409fcdc
  grunweg

  committed
  409fcdc

  Copy full SHA for 409fcdc

Commits on Jan 27, 2026

• chore: remove superfluous 'by fun_prop' parameters (#34446)

  Show description for 23d606e
  grunweg

  committed
  23d606e

  Copy full SHA for 23d606e

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

  grunweg

  committed
  6ab7b9e

  Copy full SHA for 6ab7b9e

Commits on Jan 14, 2026

• chore: annotate locations using manual alignment (#33976)

  Show description for aeabced
  grunweg

  committed
  aeabced

  Copy full SHA for aeabced

Commits on Jan 9, 2026

• chore: run the new `shake` tool (#32731)

  Show description for b8e3880
  

  Kha

  and

  kim-em

  committed
  b8e3880

  Copy full SHA for b8e3880

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 29, 2025

• chore: remove May 2025 deprecated declarations (#33014)

  Show description for 1448aee
  Parcly-Taxel

  committed
  1448aee

  Copy full SHA for 1448aee

Commits on Dec 19, 2025

• refactor(Dynamics): use `SetRel` notions of separation and cover (#31259)

  Show description for 87f5366
  YaelDillies

  committed
  87f5366

  Copy full SHA for 87f5366

Commits on Dec 17, 2025

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

  Show description for 0a79887
  harahu

  committed
  0a79887

  Copy full SHA for 0a79887

• chore: remove March and April 2025 deprecated declarations (#32990)

  Show description for d24b8b3
  Parcly-Taxel

  committed
  d24b8b3

  Copy full SHA for d24b8b3

• feat(Topology/UniformSpace): add `isRefl_of_mem_uniformity` (#32850)

  Show description for 25fee2c
  gasparattila

  committed
  25fee2c

  Copy full SHA for 25fee2c

Commits on Dec 15, 2025

• chore(Dynamics): fix whitespace (#32902)

  Show description for 607429b
  harahu

  committed
  607429b

  Copy full SHA for 607429b

Commits on Dec 8, 2025

• chore: re-enable the flexible linter (#32577)

  Show description for 789a309
  grunweg

  committed
  789a309

  Copy full SHA for 789a309

Commits on Dec 7, 2025

• feat(Dynamics/PeriodicPts): some theorems for `Pi.map` in `Dynamics/PeriodicPts` analogous to those for `Prod.map` (#29530)

  Show description for 466925b
  ShreckYe

  committed
  466925b

  Copy full SHA for 466925b

Commits on Dec 5, 2025

• chore: remove finiteness from Order.Filter.Lift (#23411)

  Show description for 5a54f93
  

  PatrickMassot

  and

  ADedecker

  committed
  5a54f93

  Copy full SHA for 5a54f93

Commits on Dec 4, 2025

• feat(Tactic): add `lia` as an alias for `cutsat` and use it throughout (#32376)

  Show description for 8101f86
  

  kim-em

  and

  Ruben-VandeVelde

  committed
  8101f86

  Copy full SHA for 8101f86

Commits on Dec 1, 2025

• feat(by_contra!): allow `rintro` patterns in `by_contra!` (#32230)

  Show description for 28ba29b
  JovanGerb

  committed
  28ba29b

  Copy full SHA for 28ba29b

• feat(Order/Basic): change the type of `Eq.trans_ge` and `LE.le.trans_eq'` (#32246)

  Show description for b6b88ca
  JovanGerb

  committed
  b6b88ca

  Copy full SHA for b6b88ca

Commits on Nov 28, 2025

• chore: enable the flexible linter in mathlib (#28962)

  Show description for 3b77237
  grunweg

  committed
  3b77237

  Copy full SHA for 3b77237

Commits on Nov 26, 2025

• chore: use generic `map_X` lemmas where possible (#31244)

  Show description for 0ceb38e
  kim-em

  committed
  0ceb38e

  Copy full SHA for 0ceb38e

Commits on Nov 24, 2025

• doc(Dynamics): polish docstrings (#31441)

  Show description for 1530991
  harahu

  committed
  1530991

  Copy full SHA for 1530991

Commits on Nov 19, 2025

• feat(Dynamics/Ergodic): add `ergodic_of_ergodic_semiconj` (#31793)

  Show description for 3f3cd98
  lua-vr

  committed
  3f3cd98

  Copy full SHA for 3f3cd98

• feat(push_neg): tag `not_frequently` and `not_eventually` (#31403)

  Show description for 66b2a65
  JovanGerb

  committed
  66b2a65

  Copy full SHA for 66b2a65

• 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 17, 2025

• doc: ensure only a single H1 header per file (#31741)

  harahu

  committed
  0e528d8

  Copy full SHA for 0e528d8

Commits on Nov 16, 2025

• doc: tidy backticks in misc. subdirectories (#31699)

  Show description for bd39cb5
  harahu

  committed
  bd39cb5

  Copy full SHA for bd39cb5

Commits on Nov 11, 2025

• chore(Analysis/SpecificLimits/Basic): generalize lemmas (#28475)

  astrainfinita

  committed
  11acf7c

  Copy full SHA for 11acf7c

Commits on Nov 7, 2025

• refactor(Logic/Equiv): rename `image_eq_preimage` to `image_symm_eq_preimage`/`image_eq_preimage_symm` (#31130)

  Show description for 3ec545d
  YaelDillies

  committed
  3ec545d

  Copy full SHA for 3ec545d

Commits on Nov 6, 2025

• chore: golf using finiteness (#31005)

  Show description for ec86c6c
  grunweg

  committed
  ec86c6c

  Copy full SHA for ec86c6c

Pagination

Previous

Next