Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Jul 17, 2025

• feat(Finsupp): `single a (m₁ + m₂) b = single a m₁ b + single a m₂ b` (#27191)

  Show description for 9a0e50a
  YaelDillies

  committed
  9a0e50a

  Copy full SHA for 9a0e50a

Commits on Jul 16, 2025

• feat(VectorBundle/MDifferentiable): differentiability results for coordChange (#26866)

  Show description for c728e64
  grunweg

  committed
  c728e64

  Copy full SHA for c728e64

• feat(LinearAlgebra/AffineSpace/Independent): interior lies in affine span (#26823)

  Show description for 3805342
  

  jsm28

  and

  eric-wieser

  committed
  3805342

  Copy full SHA for 3805342

• chore(Bernoulli): remove use of `WellFounded.fix` (#27222)

  Show description for cc10a0a
  plp127

  committed
  cc10a0a

  Copy full SHA for cc10a0a

• chore: tidy various files (#27220)

  Ruben-VandeVelde

  committed
  f2ef6e5

  Copy full SHA for f2ef6e5

• chore(Aesop): remove aesop `apply` (#26609)

  Show description for 71f3666
  

  artie2000

  and

  linesthatinterlace

  committed
  71f3666

  Copy full SHA for 71f3666

• feat(Order): `StrictMono.denselyOrdered_range` (#27208)

  Show description for f93cd71
  pechersky

  committed
  f93cd71

  Copy full SHA for f93cd71

• feat(CategoryTheory): Formal coproducts (#26402)

  Show description for 16b95a4
  kckennylau

  committed
  16b95a4

  Copy full SHA for 16b95a4

• refactor(docs/references.bib) : Run bibtool (#27219)

  Show description for 7549c63
  mans0954

  committed
  7549c63

  Copy full SHA for 7549c63

• feat: add mdifferentiable version of hom bundle smoothness lemmas (#26922)

  Show description for e7fe66f
  grunweg

  committed
  e7fe66f

  Copy full SHA for e7fe66f

• feat: define `IsKolmogorovProcess` (#27202)

  Show description for 60d731f
  RemyDegenne

  committed
  60d731f

  Copy full SHA for 60d731f

• feat: two lemmas about Lp functions and product spaces (#27029)

  Show description for 220be37
  RemyDegenne

  committed
  220be37

  Copy full SHA for 220be37

• feat(RepresentationTheory/Homological/GroupHomology/Functoriality): low degree functoriality maps (#25939)

  Show description for ea5588a
  

  101damnations

  and

  101damnations

  committed
  ea5588a

  Copy full SHA for ea5588a

• feat(RingTheory/TensorProduct/FG) : direct limit properties of tensor products wrt finitely generated submodules (#26717)

  Show description for e109780
  AntoineChambert-Loir

  committed
  e109780

  Copy full SHA for e109780

• chore(CategoryTheory/Limits/Shapes/Pullback/Categorical): remove useless [local simp] (#27203)

  Show description for 1e542fa
  robin-carlier

  committed
  1e542fa

  Copy full SHA for 1e542fa

• feat: Nat.log2 <= Real.logb 2 (#27201)

  Show description for 9c18b42
  RemyDegenne

  committed
  9c18b42

  Copy full SHA for 9c18b42

• feat(Probability): Hoeffding's lemma (#26744)

  Show description for 6e8affb
  paulorauber

  committed
  6e8affb

  Copy full SHA for 6e8affb

• feat: ContinuousLinearMap.flip/bilinearComp of zero (#27193)

  Show description for 5726d73
  RemyDegenne

  committed
  5726d73

  Copy full SHA for 5726d73

• feat: gramSchmidtNormed_linearIndependent and minor tweaks (#27023)

  Show description for 83404a6
  grunweg

  committed
  83404a6

  Copy full SHA for 83404a6

• chore: use `edist` instead of `dist` in `TendstoInMeasure` (#26954)

  Show description for 00a8983
  RemyDegenne

  committed
  00a8983

  Copy full SHA for 00a8983

• feat: commuting unitors and tensor product (#27189)

  Show description for ed41206
  YaelDillies

  committed
  ed41206

  Copy full SHA for ed41206

• chore: fix four `Submonoid` recursors (#27185)

  Show description for 488d3b8
  Parcly-Taxel

  committed
  488d3b8

  Copy full SHA for 488d3b8

Commits on Jul 15, 2025

• chore: import `rw??` into `Mathlib.Tactic.Common` (#27164)

  Show description for 3a07408
  JovanGerb

  committed
  3a07408

  Copy full SHA for 3a07408

• feat(NumberTheory/Padics/ValuativeRel): ValuativeRel ℚ_[p] (#27177)

  Show description for 42632e6
  pechersky

  committed
  42632e6

  Copy full SHA for 42632e6

• feat: solution to ODE is Lipschitz with respect to the initial condition (#26392)

  Show description for 5bfba47
  winstonyin

  committed
  5bfba47

  Copy full SHA for 5bfba47

• chore: generalise `FreeGroup.ext_hom` to monoids (#27140)

  Show description for 54b59e3
  YaelDillies

  committed
  54b59e3

  Copy full SHA for 54b59e3

• feat(CategoryTheory/Adjunction): the right partial adjoint (#27168)

  Show description for e2292a3
  grhkm21

  committed
  e2292a3

  Copy full SHA for e2292a3

• feat(Data/Matrix): add `Matrix.vecCons_inj` (#26896)

  Show description for 845ff2b
  staroperator

  committed
  845ff2b

  Copy full SHA for 845ff2b

• feat: Finset.max'_eq_iff (#27153)

  Show description for 3e077d8
  joelriou

  committed
  3e077d8

  Copy full SHA for 3e077d8

• feat(CategoryTheory/Preadditive/Injective/Basic, CategoryTheory/Preadditive/Projective/Basic): injectivity/projectivity criterion (#27156)

  Show description for ccca472
  

  smorel394

  and

  smorel394

  committed
  ccca472

  Copy full SHA for ccca472

• feat(Algebra/SkewMonoidAlgebra/Basic): multiplication and algebraic instances (#26933)

  Show description for 4940ad6
  

  Louddy

  and

  mariainesdff

  committed
  4940ad6

  Copy full SHA for 4940ad6

• feat(Algebra/Polynomial/AlgebraMap): add lemmas (#26666)

  Show description for efb6091
  mariainesdff

  committed
  efb6091

  Copy full SHA for efb6091

• chore: golf Algebra/ using `simp`/`simp_all` (#27130)

  euprunin

  committed
  e87547a

  Copy full SHA for e87547a

• feat: add Mathlib.RingTheory.DedekindDomain.Instances (#26070)

  Show description for f96ef6f
  riccardobrasca

  committed
  f96ef6f

  Copy full SHA for f96ef6f

• feat: coin problem with two coins and prime ideals in ℕ (#27065)

  Show description for b330acf
  alreadydone

  committed
  b330acf

  Copy full SHA for b330acf

Pagination

Previous

Next