All pull requests

Pull requests

• chore: bump toolchain to v4.35.0

  auto-merge-after-CIdependency-bump
  #44806·Garmelon opened Oct 12, 2026Contributor·

  ·
  1

• chore: link bors's dashboard at bors.mathlib.org

  easyLLM-generated
  #44805·bryangingechen opened Oct 12, 2026Contributor·

  ·
  1

• refactor(MeasureTheory/Function): generalize Egorov's theorem

  t-measure-probability
  #44804·D-Thomine opened Oct 12, 2026Collaborator·

  ·
  2

• feat(Tactic/Linter/TextBased): lint against more characters in module names

  t-linter
  #44803·SnirBroshi opened Oct 12, 2026Collaborator·

  ·
  1

• feat(MeasureTheory/Lebesgue): one-dimensional Brunn–Minkowski theorem

  t-measure-probability
  #44802·wwylele opened Oct 12, 2026Collaborator·

  ·
  2

• chore(LinearAlgebra/RootSystem/WeylGroup): prove the three range lemmas from one

  LLM-generatednew-contributort-algebratech debt
  #44801·keithadler opened Oct 12, 2026Contributor·

  ·
  3

• feat(Geometry/Convex): segments in convex space

  t-convex-geometry
  #44799·ooovi opened Oct 12, 2026Collaborator·

  ·
  1

• style(Order/Heyting): rename inf_himp to inf_himp_self

  LLM-generatednew-contributort-order
  #44798·3y3y3y-huaiji opened Oct 12, 2026·

  ·
  3

• chore: update Mathlib dependencies 2026-10-11

  dependenciesdependency-bump
  #44797·Vierkantor opened Oct 12, 2026Contributor·

  ·
  1

• chore: localize some global set_options

  increases-technical-debt
  #44796·JovanGerb opened Oct 12, 2026Contributor·

  ·
  1

• feat: condition for Polynomial.coeffs p ⊆ s

  t-algebra
  #44795·vihdzp opened Oct 12, 2026Collaborator·

  ·
  5

• feat(Geometry/Euclidean/Incenter/SouthPole): south / north pole of a simplex

  t-euclidean-geometry
  #44794·jsm28 opened Oct 12, 2026Contributor·

  ·
  1

• feat: every element is between two others in a club set

  t-order
  #44793·vihdzp opened Oct 12, 2026Collaborator·

  ·
  4

• chore(CategoryTheory/Limits/Cones): automated extraction from #44765

  ready-to-merget-category-theory
  #44792·mathlib-splicebot[bot] opened Oct 12, 2026Bot·

  ·
  4

• chore(SimplicialSet): fix typo

  easyt-algebraic-topology
  #44791·JX-Mo opened Oct 12, 2026Contributor·

  ·
  3

• doc(Topology): correct definition comment for QuasiSober space

  new-contributort-topology
  #44789·Zeta-Wu opened Oct 12, 2026Contributor·

  ·
  4

• refactor(RingTheory/Jacobson): use Ring.jacobson throughout the library

  LLM-generated
  #44788·BryceT233 opened Oct 12, 2026Contributor·

  ·
  2

• chore(Data/DFinsupp/BigOperators): golf

  t-data
  #44787·qawbecrdtey opened Oct 12, 2026Collaborator·

  ·
  1

• feat(Lean/Quote): restore Quote instances for Int and Rat

  LLM-generatednew-contributort-meta
  #44786·ZRTMRH opened Oct 12, 2026Contributor·

  ·
  3

• feat(Combinatorics): prove finitary Van der Waerden by compactness

  awaiting-authornew-contributort-combinatorics
  #44784·shunfeng8421 opened Oct 12, 2026·

  ·
  5

• feat(Analysis/MeanInequalities): n-ary ℓ^p monotonicity and Lyapunov's inequality

  LLM-generatednew-contributort-analysis
  #44783·ZRTMRH opened Oct 11, 2026Contributor·

  ·
  3

• chore: remove redundant meta import Mathlib.Tactic.

  #44782·JovanGerb opened Oct 11, 2026Contributor·

  ·
  1

• chore(RepresentationTheory/Basic): automated extraction from #44776

  maintainer-merget-algebra
  #44780·mathlib-splicebot[bot] opened Oct 11, 2026Bot·

  ·
  5

• feat(AlgebraicTopology): the Reedy structure on the simplex category

  t-algebraic-topology
  #44778·joelriou opened Oct 11, 2026Contributor·

  ·
  4

• chore: use Type* in a few more places

  LLM-generatednew-contributort-ring-theory
  #44776·keithadler opened Oct 11, 2026Contributor·

  ·
  9