Commits

Breadcrumbs

History for

onmaster

User selector

All users

All time

Commit History

Commits on Mar 5, 2026

• chore(Topology/Order/LeftRight): use `to_dual` (#35637)

  Show description for 1dc478f
  vihdzp

  committed
  1dc478f

  Copy full SHA for 1dc478f

• feat(Combinatorics/SimpleGraphs): generalize SimpleGraph.map to any function (#36130)

  Show description for 90795a0
  vbeffara

  committed
  90795a0

  Copy full SHA for 90795a0

• feat: integral of the evaluation map (#36179)

  Show description for 12760c9
  EtienneC30

  committed
  12760c9

  Copy full SHA for 12760c9

• feat(FieldTheory/RatFunc/Luroth): algEquivOfTranscendental (#36133)

  Show description for 0eae836
  

  justus-springer

  and

  pre-commit-ci-lite[bot]

  committed
  0eae836

  Copy full SHA for 0eae836

• feat: independence of Gaussian processes (#32334)

  Show description for 6440f9f
  EtienneC30

  committed
  6440f9f

  Copy full SHA for 6440f9f

• feat(Order): Add `eventually_finset_ball` (#36183)

  Show description for 286b90f
  

  DavidLedvinka

  and

  David Ledvinka

  committed
  286b90f

  Copy full SHA for 286b90f

• fix(NumberTheory/Padics): remove diamond normed instance on C_p (#36118)

  Show description for 9e7dfb2
  jjdishere

  committed
  9e7dfb2

  Copy full SHA for 9e7dfb2

• feat(CategoryTheory/Monoidal/Grp_): add constructor for `Grp.mk A ⟶ Grp.mk B` (#36113)

  Show description for 39f0219
  tb65536

  committed
  39f0219

  Copy full SHA for 39f0219

• feat(RingTheory/Valuation): add API (#36110)

  Show description for 362209f
  

  mariainesdff

  and

  faenuccio

  committed
  362209f

  Copy full SHA for 362209f

• feat(RingTheory/Polynomial/GaussLemma): `mem_lifts` lemma for primitive polynomials (#36068)

  Show description for e4c3741
  justus-springer

  committed
  e4c3741

  Copy full SHA for e4c3741

• feat: better error message in T% elaborator (#36040)

  Show description for af60a26
  grunweg

  committed
  af60a26

  Copy full SHA for af60a26

• chore(Geometry/Manifold/VectorField/Pullback): golf using custom elab… (#36012)

  Show description for 1f1cdf3
  grunweg

  committed
  1f1cdf3

  Copy full SHA for 1f1cdf3

• chore(Geometry/Manifold/VectorBundle/MDifferentiable): golf using cus… (#36011)

  Show description for 0bc810b
  grunweg

  committed
  0bc810b

  Copy full SHA for 0bc810b

• chore(Geometry/Manifold/MFDeriv): golf using custom elaborators (#36010)

  grunweg

  committed
  f0fb0d6

  Copy full SHA for f0fb0d6

• chore(Geometry/Manifold/MFDeriv/SpecificFunctions): golf using custom… (#36009)

  Show description for 4877fda
  grunweg

  committed
  4877fda

  Copy full SHA for 4877fda

• chore(Geometry/Manifold/Algebra): golf using custom elaborators (#36007)

  grunweg

  committed
  3e8515c

  Copy full SHA for 3e8515c

• feat(NumberTheory/Height/Basic): {mul|log}Height_{eq_one_of_subsingleton|sumElim_zero_eq} (#35922)

  Show description for 86514de
  MichaelStollBayreuth

  committed
  86514de

  Copy full SHA for 86514de

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

  Show description for 7b60111
  vihdzp

  committed
  7b60111

  Copy full SHA for 7b60111

• feat(Data/List): add theorem `length_eq_two'` (#35775)

  IvanRenison

  committed
  8e1dd63

  Copy full SHA for 8e1dd63

• feat: radical lemmas for natural numbers and integers (#35673)

  Show description for 83f6619
  Parcly-Taxel

  committed
  83f6619

  Copy full SHA for 83f6619

• feat(Data): define grading-preserving isomorphisms (#30367)

  Show description for 40710e1
  

  kckennylau

  and

  linesthatinterlace

  committed
  40710e1

  Copy full SHA for 40710e1

• feat: lemmas related to inner product (#36180)

  Show description for f262e9e
  EtienneC30

  committed
  f262e9e

  Copy full SHA for f262e9e

• feat(RingTheory): isomorphism between perfection of R and perfection of R/I (#36161)

  Show description for a240321
  kckennylau

  committed
  a240321

  Copy full SHA for a240321

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

  Show description for 237efa9
  urkud

  committed
  237efa9

  Copy full SHA for 237efa9

• chore(Geometry/Manifold/ContMDiffMFDeriv): golf using custom elaborators (#36008)

  grunweg

  committed
  bbd1294

  Copy full SHA for bbd1294

• chore(Order/SuccPred/Limit): use `to_dual` on everything that was missing (#35639)

  Show description for faa2693
  

  vihdzp

  and

  vihdzp

  committed
  faa2693

  Copy full SHA for faa2693

• chore: reduce defeq abuse (#35286)

  Show description for 4646bc6
  

  urkud

  and

  kim-em

  committed
  4646bc6

  Copy full SHA for 4646bc6

• feat(RingTheory): define maps of homogeneous ideals (#30334)

  Show description for 2e7b749
  kckennylau

  committed
  2e7b749

  Copy full SHA for 2e7b749

• feat: add `dsimp%` elaborator (#36043)

  Show description for 45362d7
  

  robin-carlier

  and

  pre-commit-ci-lite[bot]

  committed
  45362d7

  Copy full SHA for 45362d7

• chore: replace uses of `omega` with `lia` (#35944)

  Show description for 89b0edf
  euprunin

  committed
  89b0edf

  Copy full SHA for 89b0edf

• feat(Combinatorics/SimpleGraph/Acyclic): add colorable and chromaticN… (#34954)

  Show description for f318334
  brianrabern

  committed
  f318334

  Copy full SHA for f318334

• chore: remove set_option backward.isDefEq.respectTransparency false (#36164)

  Show description for 44e8425
  kim-em

  committed
  44e8425

  Copy full SHA for 44e8425

• feat(RingTheory): base change of graded algebra (#30322)

  Show description for f5e1ab1
  kckennylau

  committed
  f5e1ab1

  Copy full SHA for f5e1ab1

• feat(Integral.Bochner.Set): add `tendsto_setIntegral_of_monotone₀` (#34025)

  Show description for 592989b
  lua-vr

  committed
  592989b

  Copy full SHA for 592989b

• feat(ContinuousMultilinearMap): generalize some definitions (#34491)

  Show description for 891dd96
  urkud

  committed
  891dd96

  Copy full SHA for 891dd96

Pagination

Previous

Next