All pull requests

Pull requests

• feat(Geometry/Convex/ConvexSpace): the subdivision operator on affine chains

  t-algebraic-topologyt-category-theoryt-convex-geometryWIP
  #45999·joelriou opened Nov 13, 2026Contributor·

  ·
  1

• feat(Analysis/Polynomial): define signRight algebraically

  new-contributor
  #45998·tomaz1502 opened Nov 13, 2026Collaborator·

  ·
  2

  

• chore: downstream-lean4 adaptations for nightly-2026-11-11

  increases-technical-debtnew-contributor
  #45996·downstream-lean4[bot] opened Nov 13, 2026Bot·

  ·
  2

• feat(MeasureTheory/ContinuousMapDense): density of C_c in Lp

  blocked-by-other-PRt-measure-probability
  #45995·WenrongZou opened Nov 13, 2026Collaborator·1 task·

  ·
  2

• feat(script): diff two doc-gen outputs

  CIWIP
  #45994·Vierkantor opened Nov 13, 2026Contributor·

  ·
  1

• WIP: migrate Verso docstrings (2026-11-09)

  merge-conflict
  #45993·Vierkantor opened Nov 13, 2026Contributor·

  ·
  1

• feat(NumberTheory/Cyclotomic/Basic): drop integrality assumption in intermediateField_adjoin_isCyclotomicExtension

  easyt-number-theory
  #45992·xroblot opened Nov 13, 2026Collaborator·

  ·
  1

• feat(Data/Holor): make Holor an instance of DecidableEq

  blocked-by-other-PRlarge-importt-data
  #45991·IvanRenison opened Nov 13, 2026Collaborator·1 task·

  ·
  2

• doc: fix docstrings of Lp.boundedContinuousFunction_dense

  easyt-measure-probability
  #45990·WenrongZou opened Nov 13, 2026Collaborator·

  ·
  1

• fix(RingTheory/FractionalIdeal/Basic): restate mul_def' explicitly

  LLM-generatedt-ring-theory
  #45989·xroblot opened Nov 13, 2026Collaborator·

  ·
  1

• feat: characterize infinite product measures through product of sets in a pi system

  t-measure-probability
  #45988·EtienneC30 opened Nov 13, 2026Member·

  ·
  1

• feat: applying Bernoulli measures to singletons

  t-measure-probability
  #45987·mathlib-splicebot[bot] opened Nov 13, 2026Bot·

  ·
  1

• ci: remove mathlib4-nightly-testing paths

  CI
  #45985·marcelolynch opened Nov 13, 2026Contributor·

  ·
  1

• feat(LinearAlgebra/Matrix/UpdateSubmatrix): add the special case extendByOne

  blocked-by-other-PRt-algebra
  #45984·Nicola9Falciola opened Nov 13, 2026Contributor·1 task·

  ·
  2

• feat(CategoryTheory/Inserter): accessibility of inserters VI

  blocked-by-other-PRlarge-importt-category-theorytech debt
  #45983·robin-carlier opened Nov 13, 2026Contributor·1 task·

  ·
  2

• feat(CategoryTheory/Inserter): accessibility of inserters V

  blocked-by-other-PRlarge-importt-category-theorytech debt
  #45982·robin-carlier opened Nov 13, 2026Contributor·1 task·

  ·
  2

• feat: the centralizer of a nontrivial element in a free group is cyclic

  large-importt-group-theory
  #45981·sgouezel opened Nov 13, 2026Contributor·

  ·
  3

• feat(CategoryTheory/Inserter): accessibility of inserters IV, the main lemma

  blocked-by-other-PRlarge-importt-category-theorytech debt
  #45980·robin-carlier opened Nov 13, 2026Contributor·1 task·

  ·
  2

• feat(CategoryTheory/Inserter): accessibility of inserters III

  blocked-by-other-PRlarge-importt-category-theorytech debt
  #45979·robin-carlier opened Nov 13, 2026Contributor·1 task·

  ·
  2

• feat(CategoryTheory/Inserter): accessibility of inserters II

  blocked-by-other-PRlarge-importt-category-theorytech debt
  #45978·robin-carlier opened Nov 13, 2026Contributor·1 task·

  ·
  2

• refactor(RingTheory/DedekindDomain/Factorization): use multiplicity for ideals

  t-ring-theory
  #45976·xroblot opened Nov 13, 2026Collaborator·

  ·
  4

• chore(LinearAlgebra/TensorPower): generalize universe

  easyt-algebra
  #45975·yuma-mizuno opened Nov 13, 2026Collaborator·

  ·
  1

• feat(CategoryTheory/Inserter): accessibility of inserters I

  blocked-by-other-PRlarge-importt-category-theorytech debt
  #45974·robin-carlier opened Nov 13, 2026Contributor·1 task·

  ·
  2

• feat: simps sometimes protects generated lemas

  blocked-by-other-PRt-meta
  #45973·fpvandoorn opened Nov 13, 2026Member·1 task·

  ·
  2

• feat(Analysis/Normed): lipschitzness of group operations

  t-analysis
  #45972·YaelDillies opened Nov 13, 2026Contributor·

  ·
  1