Commits

Breadcrumbs

History for

onmaster

User selector

All users

All time

Commit History

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

• chore(Control/Fix): remove redundant import (#31614)

  qawbecrdtey

  committed
  7f4ff1f

  Copy full SHA for 7f4ff1f

Commits on Jul 3, 2025

• chore: golf using `omega` (#26405)

  euprunin

  committed
  dfa4fe7

  Copy full SHA for dfa4fe7

Commits on May 14, 2025

• style(NumberTheory): make sure items in docs have no odd indentation (#24902)

  Show description for 95bc769
  grunweg

  committed
  95bc769

  Copy full SHA for 95bc769

Commits on Apr 1, 2025

• chore: eliminate references to auxiliary proofs (#23560)

  Show description for d2100b1
  kmill

  committed
  d2100b1

  Copy full SHA for d2100b1

Commits on Jul 31, 2024

• Chore: Remove some uses of `open Classical` (#15371)

  Show description for d487a5f
  sgouezel

  committed
  d487a5f

  Copy full SHA for d487a5f

Commits on Jul 19, 2024

• chore: remove `#align` and `#align_import` statements (#14887)

  Show description for 465f26f
  

  kim-em

  and

  mattrobball

  committed
  465f26f

  Copy full SHA for 465f26f

Commits on Jul 16, 2024

• chore: move Nat.find/findGreatest into their own file (#11891)

  Show description for 8e2586a
  

  Ruben-VandeVelde

  and

  urkud

  committed
  8e2586a

  Copy full SHA for 8e2586a

Commits on Jul 11, 2024

• chore: add missing spaces around : (#13658)

  Show description for f2c8d8b
  grunweg

  committed
  f2c8d8b

  Copy full SHA for f2c8d8b

Commits on Apr 30, 2024

• chore: adapt to multiple goal linter 1 (#12338)

  Show description for 45f93f3
  adomani

  committed
  45f93f3

  Copy full SHA for 45f93f3

Commits on Apr 7, 2024

• style: replace '.-/' by '. -/' (#11938)

  Show description for 3556ded
  grunweg

  committed
  3556ded

  Copy full SHA for 3556ded

Commits on Mar 6, 2024

• chore: scope `open Classical` (#11199)

  Show description for c747be0
  ericrbg

  committed
  c747be0

  Copy full SHA for c747be0

Commits on Dec 8, 2023

• fix: patch for std4#197 (More add lemmas for `Nat`) (#6202)

  fgdorais

  committed
  d76f152

  Copy full SHA for d76f152

Commits on Sep 7, 2023

• chore: avoid lean3 style have/suffices (#6964)

  Show description for bdc47f6
  kim-em

  committed
  bdc47f6

  Copy full SHA for bdc47f6

• chore: delay import of Tactic.Common (#7000)

  Show description for 4f3418a
  kim-em

  committed
  4f3418a

  Copy full SHA for 4f3418a

Commits on Aug 10, 2023

• chore: banish `Type _` and `Sort _` (#6499)

  Show description for 32de3f6
  mattrobball

  committed
  32de3f6

  Copy full SHA for 32de3f6

Commits on Jul 19, 2023

• chore: script to replace headers with #align_import statements (#5979)

  Show description for 89aa3a3
  

  kim-em

  and

  eric-wieser

  committed
  89aa3a3

  Copy full SHA for 89aa3a3

Commits on Jun 11, 2023

• chore: fix many typos (#4967)

  Show description for 6f9e51c
  int-y1

  committed
  6f9e51c

  Copy full SHA for 6f9e51c

Commits on May 1, 2023

• feat: make `Acc.rec` and many related defs computable (#3535)

  Show description for 31dba13
  Komyyy

  committed
  31dba13

  Copy full SHA for 31dba13

Commits on Jan 31, 2023

• Chore: drop `_root_.not_not`, export it from `Classical` (#1954)

  Show description for d3b170e
  

  urkud

  and

  jcommelin

  committed
  d3b170e

  Copy full SHA for d3b170e

Commits on Jan 3, 2023

• chore: tidy various files (#1311)

  Ruben-VandeVelde

  committed
  489ab6d

  Copy full SHA for 489ab6d

Commits on Dec 24, 2022

• feat: port Control.Fix (#1194)

  Show description for 89d5507
  

  3 peoplecommitted
  89d5507

  Copy full SHA for 89d5507

Loading