All pull requests

Pull requests

• chore: make RingHom argument explicit in Polynomial.IsRoot.map

  t-algebra
  #44884·plp127 opened Oct 15, 2026Contributor·

  ·
  1

• feat(ClickSuggestions): incorporate the calc widget

  large-importt-meta
  #44883·JovanGerb opened Oct 15, 2026Contributor·

  ·
  1

• ci: show the dependency changes in the update-dependencies Zulip messages

  CILLM-generated
  #44882·bryangingechen opened Oct 15, 2026Contributor·

  ·
  1

• ci: run lake update in a job without credentials

  CILLM-generated
  #44881·bryangingechen opened Oct 15, 2026Contributor·

  ·
  1

• fix(Cache): fail a transfer pass when curl stops before it reports every transfer

  CI
  #44880·marcelolynch opened Oct 14, 2026Contributor·

  ·
  1

• chore: bump toolchain to v4.36.0-rc1

  increases-technical-debtlarge-import
  #44879·Garmelon opened Oct 14, 2026Contributor·

  ·
  3

• feat(NumberTheory/Divisors): add a divisor-count doubling bound

  new-contributort-number-theory
  #44878·scottdhughes opened Oct 14, 2026·

  ·
  2

• chore: rename toContinuousMap to ContinuousMapClass.ofClass

  awaiting-CIt-topology
  #44877·grunweg opened Oct 14, 2026Contributor·

  ·
  1

• feat(LinearAlgebra/Matrix): add the prodEquiv for Matrix, GL and SL

  t-algebra
  #44876·Nicola9Falciola opened Oct 14, 2026Contributor·

  ·
  2

• chore: protect various declarations related to (f)derivs

  delegatedt-differential-geometry
  #44875·grunweg opened Oct 14, 2026Contributor·

  ·
  3

• chore: update Mathlib dependencies 2026-10-14

  awaiting-CIdependency-bump
  #44874·mathlib-update-dependencies[bot] opened Oct 14, 2026Bot·

  ·
  1

• feat(Combinatorics/SimpleGraph/Metric): add distance lemmas for graph maps

  LLM-generatedmaintainer-mergenew-contributort-combinatorics
  #44872·Fieldnote-Echo opened Oct 14, 2026Contributor·

  ·
  16

• chore(scripts): add LeanForControl to downstream_repos.yml

  CInew-contributor
  #44871·AnandGokhale opened Oct 14, 2026·

  ·
  2

• feat: add some OEIS tags

  t-combinatorics
  #44867·Parcly-Taxel opened Oct 14, 2026Collaborator·

  ·
  2

• feat: grind attributes for substructure membership

  WIP
  #44865·artie2000 opened Oct 14, 2026Collaborator·

  ·
  5

• feat(Order/Bounds): notation for sSup and sInf

  new-contributort-topology
  #44864·user202729 opened Oct 14, 2026Contributor·

  ·
  6

• refactor(Analysis/Convex/Caratheodory): refactor Caratheodory's theorem using strong induction

  t-analysis
  #44863·justus-springer opened Oct 14, 2026Collaborator·

  ·
  1

• style: add missing newline between imports and module doc-string

  #44860·grunweg opened Oct 14, 2026Contributor·

  ·
  3

• chore(SetTheory/Cardinal/Aleph): fix some theorem names

  maintainer-merget-set-theory
  #44859·vihdzp opened Oct 14, 2026Collaborator·

  ·
  3

• feat: connect regular cardinal orders to regular cardinals

  t-set-theory
  #44858·vihdzp opened Oct 14, 2026Collaborator·

  ·
  1

• feat: add wanted statements about Cartan matrices

  #44856·ocfnash opened Oct 14, 2026Contributor·

  ·
  1

• feat: link Order.enum to Subtype.orderIsoOfNat

  large-importt-set-theory
  #44855·vihdzp opened Oct 14, 2026Collaborator·

  ·
  2

• feat: generalize not_strictAnti_of_wellFoundedLT

  maintainer-merget-order
  #44854·vihdzp opened Oct 14, 2026Collaborator·

  ·
  11

• feat(Geometry/Group): relate the word metric to the Cayley graph distance

  new-contributort-geometric-group-theory
  #44853·dkaysin opened Oct 14, 2026·

  ·
  2

• feat(Counterexamples): add Penrose stairs paradox

  LLM-generatednew-contributor
  #44852·3y3y3y-huaiji opened Oct 14, 2026·

  ·
  5