All pull requests

Pull requests

• feat(NumberTheory): add Jacobsthal function j(2310)=14 and unbounded prime gaps

  new-contributor
  #44844·djabbat opened Oct 13, 2026·

  ·
  2

• feat: isInvertible_fderivWithin_writtenInExtChartAt

  t-differential-geometry
  #44843·mathlib-splicebot[bot] opened Oct 13, 2026Bot·

  ·
  1

• chore(Analysis/RCLike/Basic): fix outdated docstring

  easyt-analysis
  #44842·mathlib-splicebot[bot] opened Oct 13, 2026Bot·

  ·
  1

• feat: ContDiffAt.hasStrictFDerivAt_fderiv_of_minSmoothness_le

  blocked-by-other-PRt-analysis
  #44841·grunweg opened Oct 13, 2026Contributor·1 task·

  ·
  2

• chore: rename ContDiffAt.hasStrict(F)DerivAt to hasStrict(F)DerivAt_(…

  t-analysis
  #44840·grunweg opened Oct 13, 2026Contributor·

  ·
  1

• feat(Data/Nat/ModEq): add congruence mod lcm lemma

  easyt-data
  #44839·mortarsanjaya opened Oct 13, 2026Contributor·

  ·
  2

• feat: add QuotientGroup.instHasUniqueRoots

  t-group-theory
  #44838·riccardobrasca opened Oct 13, 2026Member·

  ·
  3

• feat: the Cartan matrix of the root system associated to a Cartan matrix is the matrix you started with

  t-algebra
  #44837·ocfnash opened Oct 13, 2026Contributor·

  ·
  1

• feat(NumberTheory/Legendre/Basic): the legendre symbol for p-adics

  large-importnew-contributort-number-theory
  #44836·cmhsu2012 opened Oct 13, 2026·

  ·
  3

• refactor(Translate/Core): do not pass the ref around explicitly

  t-meta
  #44835·JovanGerb opened Oct 13, 2026Contributor·

  ·
  1

• chore(cache): remove Azure reads and (dev) writes from the client

  CI
  #44834·marcelolynch opened Oct 13, 2026Contributor·

  ·
  3

• ci(cache): stop uploading to Azure

  CI
  #44832·marcelolynch opened Oct 13, 2026Contributor·

  ·
  4

• feat(Analysis/MeanInequalitiesPow): add a real power difference bound

  new-contributort-analysis
  #44831·scottdhughes opened Oct 13, 2026·

  ·
  3

• feat: enable Verso where no syntax changes are required

  documentationWIP
  #44830·Vierkantor opened Oct 13, 2026Contributor·

  ·
  1

• feat(Analysis/Normed): generalize scalar distance and diameter lemmas

  new-contributort-analysis
  #44829·pelicanhere opened Oct 13, 2026Collaborator·

  ·
  4

• doc(LinearAlgebra/Contraction): fix typo in docstring for dualDistribEquiv

  t-algebra
  #44828·DanielJHorton opened Oct 13, 2026Contributor·

  ·
  2

• feat: add integral representation for p \in (-1,0)

  awaiting-authornew-contributort-analysis
  #44827·dragonclaw417 opened Oct 13, 2026·

  ·
  19

  

• chore: rename coe_int lemmas to intCast

  LLM-generated
  #44826·Multramate opened Oct 13, 2026Collaborator·

  ·
  2

• chore: rename coe_nat/nat_cast lemmas to natCast

  LLM-generated
  #44825·Multramate opened Oct 13, 2026Collaborator·

  ·
  2

• chore: rename nonzero to ne_zero in theorem names

  LLM-generated
  #44824·Multramate opened Oct 13, 2026Collaborator·

  ·
  4

• chore: fix misspellings in declaration names

  delegatedLLM-generated
  #44823·Multramate opened Oct 13, 2026Collaborator·

  ·
  4

• feat(Geometry/Euclidean/Inversion): affine limits and filter identities

  awaiting-authorLLM-generatednew-contributort-euclidean-geometry
  #44822·William7743 opened Oct 13, 2026·

  ·
  4

• feat(Linter/Style): lint for any unscoped backward compatibility options

  increases-technical-debtt-linter
  #44820·grunweg opened Oct 13, 2026Contributor·

  ·
  1

• feat(Algebra/Lie): solvable_of_ideal_and_quot_solv and quotient.mk''

  awaiting-authornew-contributort-algebra
  #44818·vdelbarc opened Oct 13, 2026Contributor·

  ·
  13

• doc(workflows): remove stale cross-reference list

  CIdocumentationeasy
  #44817·luigi-massacci opened Oct 13, 2026Collaborator·

  ·
  2