Commits

Breadcrumbs

History for

onmaster

User selector

All users

All time

Commit History

Commits on Feb 13, 2026

• 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 Jan 21, 2026

• chore(SetTheory/Cardinal): remove explicit argument to `nat_lt_aleph0` (#33990)

  Show description for d630389
  YaelDillies

  committed
  d630389

  Copy full SHA for d630389

• chore(SetTheory/Cardinal/Arithmetic): switch `lift.{max u w} x = lift.{max v w} y` to `lift.{u} x = lift.{v} y` (#33657)

  vihdzp

  committed
  fdd5760

  Copy full SHA for fdd5760

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

• feat(SetTheory/Cardinal): formulas for `sum (fun n : ℕ ↦ x ^ n)` (#32645)

  vihdzp

  committed
  c96081d

  Copy full SHA for c96081d

Commits on Dec 17, 2025

• doc: fix file references (#32855)

  Show description for 1035fd0
  harahu

  committed
  1035fd0

  Copy full SHA for 1035fd0

Commits on Dec 15, 2025

• chore(SetTheory): fix whitespace (#32899)

  Show description for f385661
  harahu

  committed
  f385661

  Copy full SHA for f385661

Commits on Dec 5, 2025

• feat(push_neg): `push_neg +distrib` syntax (#31406)

  Show description for 06bb38c
  JovanGerb

  committed
  06bb38c

  Copy full SHA for 06bb38c

Commits on Nov 29, 2025

• chore: golf using `contrapose` for `↔` (#32193)

  Show description for 63af23d
  JovanGerb

  committed
  63af23d

  Copy full SHA for 63af23d

Commits on Nov 22, 2025

• chore: rename `mul_le_mul_right'` to `mul_le_mul_left` (#30242)

  YaelDillies

  committed
  b07a584

  Copy full SHA for b07a584

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

• chore: remove use of `erw` in `SetTheory.Cardinal.Arithmetic` (#31774)

  euprunin

  committed
  58e94a9

  Copy full SHA for 58e94a9

• chore: bump toolchain to v4.26.0-rc1 (#31763)

  Show description for 1988a78
  

  6 peoplecommitted
  1988a78

  Copy full SHA for 1988a78

Commits on Oct 22, 2025

• feat(SetTheory/Cardinal): generalize and rename theorems on `Cardinal.sum` (#29351)

  Show description for df375c2
  staroperator

  committed
  df375c2

  Copy full SHA for df375c2

Commits on Oct 17, 2025

• chore: use `grw`, `gcongr` more (#30508)

  Show description for 108140a
  YaelDillies

  committed
  108140a

  Copy full SHA for 108140a

Commits on Aug 26, 2025

• chore: golf using `grw` (#26981)

  Show description for da5290c
  JovanGerb

  committed
  da5290c

  Copy full SHA for da5290c

Commits on Jul 11, 2025

• refactor(SetTheory/Ordinal/Arithmetic): `Ordinal.IsLimit` → `Order.IsSuccLimit` (#26643)

  Show description for d6f4a82
  vihdzp

  committed
  d6f4a82

  Copy full SHA for d6f4a82

Commits on Jun 27, 2025

• chore: remove unused simp arguments (#26430)

  Show description for cf17ac4
  

  nomeata

  and

  YaelDillies

  committed
  cf17ac4

  Copy full SHA for cf17ac4

Commits on Jun 7, 2025

• chore: deprime `induction` in `Archive` and `SetTheory` (#25512)

  Show description for cb99f5a
  Parcly-Taxel

  committed
  cb99f5a

  Copy full SHA for cb99f5a

• chore(Order): use new ge/gt naming convention - Part 2 (#25560)

  Show description for 6c6e018
  JovanGerb

  committed
  6c6e018

  Copy full SHA for 6c6e018

• chore(Order): use new `ge`/`gt` naming convention - Part 1 (#24775)

  Show description for 827b149
  JovanGerb

  committed
  827b149

  Copy full SHA for 827b149

Commits on Mar 18, 2025

• chore(SetTheory): split `Cardinal/Basic.lean` (#23014)

  Show description for a80159d
  Vierkantor

  committed
  a80159d

  Copy full SHA for a80159d

Commits on Mar 17, 2025

• refactor(SetTheory/Cardinal/Ordinal): move results (#21857)

  Show description for 53b17b6
  vihdzp

  committed
  53b17b6

  Copy full SHA for 53b17b6

Commits on Feb 19, 2025

• chore: replace single-subgoal `cases'` (#21976)

  Show description for f5362da
  Parcly-Taxel

  committed
  f5362da

  Copy full SHA for f5362da

Commits on Feb 15, 2025

• chore: automatically replace `cases'` used to split `Or` (#16526)

  Show description for 0e2ee7f
  Parcly-Taxel

  committed
  0e2ee7f

  Copy full SHA for 0e2ee7f

Commits on Jan 26, 2025

• feat(SetTheory/Cardinal/Arithmetic): omega ordinals are additively/multiplicatively principal (#18778)

  vihdzp

  committed
  c774a9c

  Copy full SHA for c774a9c

• feat: `a ^ b ≤ ℵ₀` if `a ≤ ℵ₀` and `b < ℵ₀` (#21060)

  Show description for 1844f02
  YaelDillies

  committed
  1844f02

  Copy full SHA for 1844f02

Commits on Jan 24, 2025

• chore(SetTheory/Cardinal/Arithmetic): remove unneeded import (#21013)

  vihdzp

  committed
  8f355f5

  Copy full SHA for 8f355f5

Commits on Jan 12, 2025

• feat: allow several identifiers in assert_not_exists (#15994)

  Show description for 0634717
  

  adomani

  and

  joneugster

  committed
  0634717

  Copy full SHA for 0634717

Commits on Jan 6, 2025

• chore: remove >9 month old deprecations (#20505)

  kim-em

  committed
  886b340

  Copy full SHA for 886b340

Commits on Jan 5, 2025

• feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933)

  vihdzp

  committed
  3c12551

  Copy full SHA for 3c12551

Commits on Dec 16, 2024

• feat(SetTheory/Cardinal/Arithmetic): cardinality of ordinal exponential (#17813)

  Show description for 9e10768
  vihdzp

  committed
  9e10768

  Copy full SHA for 9e10768

Commits on Dec 12, 2024

• chore(SetTheory/Cardinal/Arithmetic): generalize `card_iSup_Iio_le_sum_card` (#19727)

  Show description for d554797
  vihdzp

  committed
  d554797

  Copy full SHA for d554797

Commits on Dec 5, 2024

• refactor(SetTheory/Ordinal/Arithmetic): redefine `IsLimit` to `IsSuccLimit` (#19054)

  Show description for 6a9d0fe
  vihdzp

  committed
  6a9d0fe

  Copy full SHA for 6a9d0fe

Commits on Nov 14, 2024

• chore(SetTheory/Ordinal/Basic): `Ordinal.lt_iSup` → `Ordinal.lt_iSup_iff` (#18903)

  Show description for a5a981b
  vihdzp

  committed
  a5a981b

  Copy full SHA for a5a981b

Pagination

Previous

Next