Commits

Breadcrumbs

History for

onmaster

User selector

All users

All time

Commit History

Commits on Mar 5, 2026

• refactor: nicer definition for ordinal logarithm (#35850)

  Show description for 7b60111
  vihdzp

  committed
  7b60111

  Copy full SHA for 7b60111

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

  Show description for 237efa9
  urkud

  committed
  237efa9

  Copy full SHA for 237efa9

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 Mar 2, 2026

• chore: golf using `simp` (#35726)

  Show description for 827d134
  euprunin

  committed
  827d134

  Copy full SHA for 827d134

• feat(SetTheory/Ordinal/CantorNormalForm): Evaluate a Finsupp as a CNF (#33840)

  Show description for d7da6fe
  

  vihdzp

  and

  vihdzp

  committed
  d7da6fe

  Copy full SHA for d7da6fe

• chore(SetTheory/Ordinal/Basic): deprecate `Ordinal.induction` → `WellFoundedLT.induction` (#35855)

  Show description for f5110b6
  vihdzp

  committed
  f5110b6

  Copy full SHA for f5110b6

• chore: mark Submodule.toAddSubgroup @[reducible] (#35761)

  Show description for 02398f3
  kim-em

  committed
  02398f3

  Copy full SHA for 02398f3

• 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

• chore: fix whitespace (#35909)

  Show description for 338973d
  grunweg

  committed
  338973d

  Copy full SHA for 338973d

Commits on Feb 28, 2026

• chore(SetTheory/Ordinal/Arithmetic): avoid terminal `simp only` (#35854)

  Show description for 24cb29a
  vihdzp

  committed
  24cb29a

  Copy full SHA for 24cb29a

Commits on Feb 27, 2026

• chore(SetTheory/Ordinal/FixedPointApproximations): fix `unusedVariables` warnings (#35859)

  vihdzp

  committed
  7b7d66d

  Copy full SHA for 7b7d66d

• refactor: nicer definition for ordinal division (#35849)

  Show description for 3d58818
  vihdzp

  committed
  3d58818

  Copy full SHA for 3d58818

• chore(SetTheory/Ordinal/Basic): deprecate `succ_eq_add_one` and `succ_zero` (#35844)

  Show description for fc17c68
  vihdzp

  committed
  fc17c68

  Copy full SHA for fc17c68

• refactor: make `Order.succ_eq_add_one` a `simp` lemma (#35741)

  Show description for bce6de5
  vihdzp

  committed
  bce6de5

  Copy full SHA for bce6de5

Commits on Feb 25, 2026

• feat(SetTheory/Cardinal): generalize infinite pigeonhole principle (#34091)

  Show description for 450920a
  staroperator

  committed
  450920a

  Copy full SHA for 450920a

Commits on Feb 24, 2026

• feat: more lemmas on `Ordinal.type` (#35519)

  Show description for 900da3d
  vihdzp

  committed
  900da3d

  Copy full SHA for 900da3d

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

  kim-em

  committed
  0c08ce9

  Copy full SHA for 0c08ce9

Commits on Feb 23, 2026

• chore: remove `simp` from `Ordinal.add_one_eq_succ` (#35553)

  Show description for 5ba5966
  vihdzp

  committed
  5ba5966

  Copy full SHA for 5ba5966

• feat(SetTheory/Cardinal): more lemmas about `ENat` (#33909)

  Show description for abd0739
  YaelDillies

  committed
  abd0739

  Copy full SHA for abd0739

• feat(SetTheory/Ordinal/Arithmetic): prove `isSuccPrelimit_iff_omega0_dvd` (#34664)

  Show description for cfc99f1
  GrigorenkoPV

  committed
  cfc99f1

  Copy full SHA for cfc99f1

Commits on Feb 20, 2026

• chore: remove deprecated material from CGT (#35550)

  Show description for 08657ed
  vihdzp

  committed
  08657ed

  Copy full SHA for 08657ed

Commits on Feb 19, 2026

• chore: `toType_empty_iff_eq_zero` → `isEmpty_toType_iff` (#35517)

  Show description for b9076d1
  vihdzp

  committed
  b9076d1

  Copy full SHA for b9076d1

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(Logic/IsEmpty): split file into `Defs` and `Basic` (#35137)

  Show description for d5bbce8
  JovanGerb

  committed
  d5bbce8

  Copy full SHA for d5bbce8

• feat(SetTheory/Cardinal/Arithmetic): `Cardinal.mk` is strictly monotone on finite sets (#34695)

  SnirBroshi

  committed
  cb597d7

  Copy full SHA for cb597d7

• feat: order topologies of successor orders (#32455)

  Show description for 80dbc51
  

  vihdzp

  and

  j-loreaux

  committed
  80dbc51

  Copy full SHA for 80dbc51

• feat(SetTheory/Cardinal): helpers for Konig's theorem on bipartite graphs (#32552)

  Show description for 6c1d14f
  

  ksenono

  and

  danils@mit.edu

  committed
  6c1d14f

  Copy full SHA for 6c1d14f

Commits on Feb 9, 2026

• refactor(SetTheory/Ordinal): introduce `natCast_pow` (#34662)

  Show description for efc0e39
  vihdzp

  committed
  efc0e39

  Copy full SHA for efc0e39

Commits on Feb 8, 2026

• chore(SetTheory/Ordinal/Veblen): add `recommended_spelling` for epsilon and gamma functions (#34732)

  Show description for a022ca4
  vihdzp

  committed
  a022ca4

  Copy full SHA for a022ca4

Commits on Feb 6, 2026

• feat(gcongr): beef up `@[gcongr]` tag to accept `↔` & any argument order (#33025)

  Show description for c01b1d7
  

  JovanGerb

  and

  joneugster

  committed
  c01b1d7

  Copy full SHA for c01b1d7

• chore(Order/Defs/Unbundled): deprecate `IsTrichotomous` in favor of core's `Std.Trichotomous` (#34349)

  SnirBroshi

  committed
  d50d677

  Copy full SHA for d50d677

Commits on Feb 5, 2026

• feat: set has cardinality one iff singleton (#28680)

  vihdzp

  committed
  b7a750a

  Copy full SHA for b7a750a

• chore(*): add `-- shake: keep-all` to all deprecated modules (#34864)

  Show description for 1626c4b
  urkud

  committed
  1626c4b

  Copy full SHA for 1626c4b

Pagination

Previous

Next