Commits

Breadcrumbs

History for

ond38b507

User selector

All users

All time

Commit History

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 Oct 31, 2025

• chore: remove declarations deprecated before 2025-04-21 (#30759)

  Show description for 1cd5402
  

  5 peoplecommitted
  1cd5402

  Copy full SHA for 1cd5402

Commits on Aug 11, 2025

• chore: reformat `to_additive` docstrings to use `docComment` syntax (#28066)

  Show description for d678e82
  thorimur

  committed
  d678e82

  Copy full SHA for d678e82

Commits on Jul 6, 2025

• feat(GroupTheory/Subgroup/Center): added lemma `center_is_normal` (#26749)

  Show description for 51827e9
  

  qawbecrdtey

  and

  ocfnash

  committed
  51827e9

  Copy full SHA for 51827e9

Commits on Apr 10, 2025

• chore(GroupTheory): Add the class `IsMulCommutative` (#23773)

  Show description for 8a90888
  xroblot

  committed
  8a90888

  Copy full SHA for 8a90888

Commits on Mar 3, 2025

• chore: move `MulDistribMulAction` material earlier (#22121)

  YaelDillies

  committed
  6d4818e

  Copy full SHA for 6d4818e

Commits on Jan 26, 2025

• feat(Algebra): `Mul/RingEquiv`s between `center` and `Module.End` (#20721)

  alreadydone

  committed
  e767899

  Copy full SHA for e767899

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 Aug 19, 2024

• chore: correct `open` -> `open scoped` (#15933)

  Show description for ce632a0
  grunweg

  committed
  ce632a0

  Copy full SHA for ce632a0

Commits on Aug 12, 2024

• chore: uncomment some now viable assert_not_exists (#15715)

  Show description for 795a856
  

  3 peoplecommitted
  795a856

  Copy full SHA for 795a856

Commits on Aug 10, 2024

• chore: deprecate MulEquiv.map_mul, AddEquiv.map_add (#15615)

  Ruben-VandeVelde

  committed
  c1f09cd

  Copy full SHA for c1f09cd

Commits on Jul 26, 2024

• chore: robustifying for debug.byAsSorry (part 5) (#15126)

  kim-em

  committed
  19a1471

  Copy full SHA for 19a1471

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 1, 2024

• chore: move some lemmas to Algebra.GroupWithZero.Center (#13944)

  Show description for 0b99fcc
  Ruben-VandeVelde

  committed
  0b99fcc

  Copy full SHA for 0b99fcc

Commits on May 30, 2024

• chore: more `refine'` to `refine` (#13287)

  Show description for 5ac1926
  

  adomani

  and

  grunweg

  committed
  5ac1926

  Copy full SHA for 5ac1926

Commits on May 3, 2024

• move: Rearrange basic algebraic subobject (#11104)

  Show description for efb7091
  

  3 peoplecommitted
  efb7091

  Copy full SHA for efb7091

Commits on Apr 20, 2024

• chore: refactor to avoid importing Ring for Group topics (#11913)

  Show description for 8e052ac
  

  kim-em

  and

  YaelDillies

  committed
  8e052ac

  Copy full SHA for 8e052ac

Loading