Commits

Breadcrumbs

History for

on7c54188

User selector

All users

All time

Commit History

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

Commits on Jan 2, 2026

• chore(Order/Defs/Unbundled): deprecate `IsSymm` in favor of core's `Std.Symm` (#33325)

  SnirBroshi

  committed
  7d40891

  Copy full SHA for 7d40891

Commits on Jan 1, 2026

• chore: remove June 2025 deprecated declarations (#33429)

  Show description for a7e757e
  Parcly-Taxel

  committed
  a7e757e

  Copy full SHA for a7e757e

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

• doc(Logic): fix file refs (#33277)

  Show description for 48f5874
  harahu

  committed
  48f5874

  Copy full SHA for 48f5874

Commits on Dec 22, 2025

• feat(RingTheory/MvPolynomial/IrrQuadratic): irreducibility of sum X_i Y_i (#31161)

  Show description for 839af0c
  

  3 peoplecommitted
  839af0c

  Copy full SHA for 839af0c

Commits on Dec 19, 2025

• chore: golf proofs (#32996)

  euprunin

  committed
  a702d1f

  Copy full SHA for a702d1f

• chore: remove backward.privateInPublic from lakefile (#33034)

  Show description for 03dd195
  

  3 peoplecommitted
  03dd195

  Copy full SHA for 03dd195

• chore(LinearAlgebra/Multilinear/Basic.lean): remove `erw`s in `restr` (#32526)

  Show description for 55fdf80
  

  3 peoplecommitted
  55fdf80

  Copy full SHA for 55fdf80

Commits on Dec 17, 2025

• chore: `grind` tags for `Logic/Relation` (#32791)

  Show description for e318f81
  luisacicolini

  committed
  e318f81

  Copy full SHA for e318f81

Commits on Dec 16, 2025

• chore: fix whitespace (#32903)

  Show description for bedee4c
  harahu

  committed
  bedee4c

  Copy full SHA for bedee4c

• chore: move `set_option backward.proofsInPublic` to where it is needed (#32934)

  Show description for fcad271
  kim-em

  committed
  fcad271

  Copy full SHA for fcad271

Commits on Dec 15, 2025

• feat(Logic/Equiv): `Option α × β ≃ β ⊕ α × β` (#32712)

  erdOne

  committed
  0c63deb

  Copy full SHA for 0c63deb

Commits on Dec 14, 2025

• chore: bump toolchain to v4.27.0-rc1 (#32874)

  Show description for 5e9b6b9
  

  6 peoplecommitted
  5e9b6b9

  Copy full SHA for 5e9b6b9

Commits on Dec 12, 2025

• chore: move to the new names for Fin coercion lemmas (#32736)

  Show description for fc734e3
  Ruben-VandeVelde

  committed
  fc734e3

  Copy full SHA for fc734e3

Commits on Dec 11, 2025

• chore: replace `omega` with `lia` where possible (#32666)

  Show description for 262b886
  kim-em

  committed
  262b886

  Copy full SHA for 262b886

Commits on Dec 8, 2025

• chore: simplify some proofs with `wlog!` (#32454)

  Show description for 5686b1b
  Hagb

  committed
  5686b1b

  Copy full SHA for 5686b1b

Commits on Dec 5, 2025

• refactor(`Data/List/Sort`): deprecate and replace `List.Sorted` (#30441)

  Show description for 84ddba1
  linesthatinterlace

  committed
  84ddba1

  Copy full SHA for 84ddba1

Pagination

Previous

Next