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

Commits on Mar 2, 2026

• chore: bump toolchain to v4.29.0-rc3 (#35942)

  Show description for 9b1001c
  

  3 peoplecommitted
  9b1001c

  Copy full SHA for 9b1001c

Commits on Mar 1, 2026

• chore(*): reduce defeq abuse about `Set` (#35795)

  Show description for f08eb80
  urkud

  committed
  f08eb80

  Copy full SHA for f08eb80

Commits on Feb 27, 2026

• chore: mark `Encodable.ofCountable` as `no_expose` (#35838)

  Show description for 6cbbebb
  vihdzp

  committed
  6cbbebb

  Copy full SHA for 6cbbebb

• feat: classical "decidability" instances on sets and ideals (#33757)

  Show description for a5a17eb
  fpvandoorn

  committed
  a5a17eb

  Copy full SHA for a5a17eb

Commits on Feb 25, 2026

• chore(*): reduce defeq abuse around `Set` (#35752)

  urkud

  committed
  6dc81b8

  Copy full SHA for 6dc81b8

Commits on Feb 23, 2026

• feat: add (m)differentiableAt_of_(m)fderiv_injective (#35284)

  Show description for 8b62eaa
  grunweg

  committed
  8b62eaa

  Copy full SHA for 8b62eaa

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

• chore(Order/Defs/Unbundled): deprecate `def Irreflexive` in favor of `class Std.Irrefl` (#35191)

  SnirBroshi

  committed
  41228da

  Copy full SHA for 41228da

Commits on Feb 13, 2026

• chore(Logic/IsEmpty): split file into `Defs` and `Basic` (#35137)

  Show description for d5bbce8
  JovanGerb

  committed
  d5bbce8

  Copy full SHA for d5bbce8

• chore: don't expose `Shrink` (#34387)

  Show description for 67144fe
  plp127

  committed
  67144fe

  Copy full SHA for 67144fe

• chore: deduplicate `attribute [simp]`s (#35202)

  Show description for 468d523
  Komyyy

  committed
  468d523

  Copy full SHA for 468d523

• chore: deprecate aliases of Classical lemmas (#34625)

  Show description for ecba541
  Ruben-VandeVelde

  committed
  ecba541

  Copy full SHA for ecba541

Commits on Feb 6, 2026

• chore: rename `CompRel` to `Relation.SymmGen` (#34428)

  Show description for cb53e58
  

  chenson2018

  and

  Ruben-VandeVelde

  committed
  cb53e58

  Copy full SHA for cb53e58

Commits on Jan 30, 2026

• chore: import Tactic.Attr.Register privately (#32541)

  Show description for 933e89d
  YaelDillies

  committed
  933e89d

  Copy full SHA for 933e89d

Commits on Jan 29, 2026

• feat(Logic/IsEmpty): add theorems relating surjectivity and emptiness (#33475)

  Show description for 9881197
  BoltonBailey

  committed
  9881197

  Copy full SHA for 9881197

• chore: golf using `grind` (#33119)

  euprunin

  committed
  2ca69d3

  Copy full SHA for 2ca69d3

Commits on Jan 28, 2026

• chore(Logic): generalise universes for relator and relation (#34391)

  Show description for 7c54188
  b-mehta

  committed
  7c54188

  Copy full SHA for 7c54188

Commits on Jan 26, 2026

• feat(Logic/Relation): transitive closure of symmetric relation is symmetric (#34382)

  Show description for 9baf873
  b-mehta

  committed
  9baf873

  Copy full SHA for 9baf873

Commits on Jan 25, 2026

• chore: golf using `grind` (#33286)

  Show description for be60ca1
  euprunin

  committed
  be60ca1

  Copy full SHA for be60ca1

Commits on Jan 20, 2026

• chore(Order/Defs/Unbundled): deprecate `IsTotal` in favor of core's `Std.Total` (#33797)

  SnirBroshi

  committed
  edec8f5

  Copy full SHA for edec8f5

Commits on Jan 18, 2026

• fix: add missing deprecations (#34087)

  Show description for 7048ffa
  Ruben-VandeVelde

  committed
  7048ffa

  Copy full SHA for 7048ffa

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

• chore: golf using `grind`, reduce compilation time and imports (#33912)

  euprunin

  committed
  ae275c9

  Copy full SHA for ae275c9

Commits on Jan 12, 2026

• chore: remove outdated `library_note2` usage (#33868)

  Show description for 77ff30a
  Vierkantor

  committed
  77ff30a

  Copy full SHA for 77ff30a

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

• chore: annotate manual alignment (#33789)

  Show description for 3c32718
  grunweg

  committed
  3c32718

  Copy full SHA for 3c32718

• chore(Order/Defs/Unbundled): deprecate `IsRefl` in favor of core's `Std.Refl` (#33755)

  SnirBroshi

  committed
  eed70c4

  Copy full SHA for eed70c4

• chore: fix whitespace (#33747)

  Show description for b294104
  harahu

  committed
  b294104

  Copy full SHA for b294104

Commits on Jan 8, 2026

• chore(Order/Defs/Unbundled): deprecate `IsIrrefl` in favor of core's `Std.Irrefl` (#33717)

  SnirBroshi

  committed
  98379c7

  Copy full SHA for 98379c7

Commits on Jan 7, 2026

• chore(Order/Defs/Unbundled): deprecate `IsAntisymm` in favor of core's `Std.Antisymm` (#33685)

  SnirBroshi

  committed
  cb3ccde

  Copy full SHA for cb3ccde

Commits on Jan 6, 2026

• chore: golf proofs (#33549)

  euprunin

  committed
  9afc927

  Copy full SHA for 9afc927

• chore(Data/Option): deprecate `Option.iget` (#33583)

  Show description for b79634a
  kim-em

  committed
  b79634a

  Copy full SHA for b79634a

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 Jan 3, 2026

• feat(ToIntervalMod): add missing lemmas (#33442)

  Show description for 96123a3
  urkud

  committed
  96123a3

  Copy full SHA for 96123a3

Pagination

Previous

Next