Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Jan 30, 2025

• chore(NumberTheory/LSeries): unsqueeze lots of terminal simps (#21133)

  loefflerd

  committed
  5b3fe12

  Copy full SHA for 5b3fe12

• doc(Order/WellFounded): minor docstring improvements (#20776)

  Show description for 410dd1f
  vihdzp

  committed
  410dd1f

  Copy full SHA for 410dd1f

• feat(RingTheory/StandardSmooth): naive cotangent complex of a submersive presentation (#19748)

  Show description for 6f5142e
  chrisflav

  committed
  6f5142e

  Copy full SHA for 6f5142e

• feat(Data/Finsupp/MonomialOrder) : lexicographic order on Unique (#20699)

  Show description for f17018b
  AntoineChambert-Loir

  committed
  f17018b

  Copy full SHA for f17018b

• chore(Variance): golf API (#20814)

  YaelDillies

  committed
  b848c8d

  Copy full SHA for b848c8d

• feat: add author to maintainer merge message (#21254)

  adomani

  committed
  e61a8cf

  Copy full SHA for e61a8cf

• feat: let notation3 pretty print "overapplied" notations (#21239)

  Show description for 9571e4a
  kmill

  committed
  9571e4a

  Copy full SHA for 9571e4a

• feat(Algebra/Category): concrete category refactor for Grp (#21192)

  Show description for 132efc7
  Vierkantor

  committed
  132efc7

  Copy full SHA for 132efc7

• feat: ext lemmas for stdBasisMatrix (#21200)

  Show description for 969f14d
  eric-wieser

  committed
  969f14d

  Copy full SHA for 969f14d

• feat: lemmas about Matrix.comp for diagonal and stdBasis (#21181)

  eric-wieser

  committed
  1db0a08

  Copy full SHA for 1db0a08

• chore: fix escaping in create-adaptation-pr.sh (#21246)

  kim-em

  committed
  d9b81fa

  Copy full SHA for d9b81fa

• feat(RingTheory/HahnSeries): define powerSeriesFamily (#20205)

  Show description for e6b6302
  ScottCarnahan

  committed
  e6b6302

  Copy full SHA for e6b6302

• chore: update Mathlib dependencies 2025-01-30 (#21247)

  Show description for 14589bd
  

  4 peoplecommitted
  14589bd

  Copy full SHA for 14589bd

• chore: process a few porting notes (#21227)

  jcommelin

  committed
  16e417e

  Copy full SHA for 16e417e

• fix(tech debt): allow multiple paths for adaptation notes (#21241)

  Show description for 956d514
  adomani

  committed
  956d514

  Copy full SHA for 956d514

• feat(Data/Matroid/Circuit): better junk values for fundCircuit (#21240)

  Show description for 0cd9763
  apnelson1

  committed
  0cd9763

  Copy full SHA for 0cd9763

• chore(SetTheory/Ordinal/Exponential): redefine ordinal exponential without bsup (#19145)

  Show description for 8ec167c
  vihdzp

  committed
  8ec167c

  Copy full SHA for 8ec167c

Commits on Jan 29, 2025

• feat(CStarAlgebra): matrices with entries in a C⋆-algebra (#15277)

  Show description for 2ae8c98
  dupuisf

  committed
  2ae8c98

  Copy full SHA for 2ae8c98

• chore(Order/SupIndep): review API (#21235)

  urkud

  committed
  34763b0

  Copy full SHA for 34763b0

• feat(NumberTheory/NumberField/FinitePlaces): change one lemma (#21187)

  Show description for 789550e
  fbarroero

  committed
  789550e

  Copy full SHA for 789550e

• feat(SimpleGraph/Coloring): a graph is 0-colorable iff it has no vertices (#21185)

  Show description for 69a0a85
  

  jt496

  and

  Lian Tattersall

  committed
  69a0a85

  Copy full SHA for 69a0a85

• feat: HasFDerivAt for Fin.cons (#20407)

  Show description for d932152
  eric-wieser

  committed
  d932152

  Copy full SHA for d932152

• feat(Analysis/Convex): extreme points of doubly stochastic matrices (#17514)

  b-mehta

  committed
  e6cdd0d

  Copy full SHA for e6cdd0d

• feat(*/Fin/*): add 2 lemmas (#21229)

  Show description for b0e2db2
  urkud

  committed
  b0e2db2

  Copy full SHA for b0e2db2

• feat: add new iteratedDeriv_const_smul/mul (#20288)

  Show description for 323ed6b
  Ruben-VandeVelde

  committed
  323ed6b

  Copy full SHA for 323ed6b

• feat(MeasureTheory/SetSemiring.lean, Order/CompleteLattice.lean): change SetSemiring allow writing unions as disjoint unions (#20931)

  Show description for 3ba0a02
  

  Peter Pfaffelhuber

  and

  pfaffelh

  committed
  3ba0a02

  Copy full SHA for 3ba0a02

• feat(SimpleGraph/Clique): graphs without one cliques (#21183)

  Show description for 2b40940
  

  jt496

  and

  Lian Tattersall

  committed
  2b40940

  Copy full SHA for 2b40940

• chore: update Mathlib dependencies 2025-01-29 (#21236)

  Show description for feedd82
  mathlib-bors[bot]

  committed
  feedd82

  Copy full SHA for feedd82

• chore(scripts/technical-debt-metrics.sh): fix counters, so that 0 is 0 (#21221)

  jcommelin

  committed
  87eb996

  Copy full SHA for 87eb996

• chore: remove some adaptation notes about unused variable linter (#21212)

  jcommelin

  committed
  ec45ea1

  Copy full SHA for ec45ea1

• chore: replace open scoped Classicalwith open scoped Classical in or classical in a tactic proof (#21228)

  Show description for b7ce26a
  kvanvels

  committed
  b7ce26a

  Copy full SHA for b7ce26a

• chore(MeasureTheory/Function/L1Space): split L1Space into HasFiniteIntegral, Integrable and AEEqFun (#21231)

  Show description for f6cd292
  

  Etienne

  committed
  f6cd292

  Copy full SHA for f6cd292

• chore: replace open scoped Classical with open scoped Classical in or classical in a tactic proof (#21220)

  Show description for fb2efae
  kvanvels

  committed
  fb2efae

  Copy full SHA for fb2efae

• feat(Data/Nat/Choose) : An upper bound on the binomial coefficient (#20735)

  Show description for 3cbf001
  ooovi

  committed
  3cbf001

  Copy full SHA for 3cbf001

• feat(CategoryTheory) : pull back preadditivity along fully faithful functors (#21170)

  javra

  committed
  5818e47

  Copy full SHA for 5818e47

Pagination

Previous

Next