All pull requests

Pull requests

• feat(RingTheory/Valuation/Discrete/Normalized): normalization of discrete valuations

  blocked-by-other-PR
  #44179·mariainesdff opened Sep 25, 2026Contributor·

  ·
  2

• ci: label a merge-queue batch full-lint when it fails lint

  CI
  #44178·kim-em opened Sep 25, 2026Contributor·

  ·
  1

• ci: lint local linters on only the modules a pull request changes

  CI
  #44177·kim-em opened Sep 25, 2026Contributor·

  ·
  1

• chore(scripts/bench): record per-linter cost in the lint benchmark

  CI
  #44176·kim-em opened Sep 25, 2026Contributor·

  ·
  1

• chore(scripts): add Plectis to downstream project list

  CInew-contributor
  #44175·wcook04 opened Sep 25, 2026·

  ·
  3

• feat(cache): retire the legacy container

  CI
  #44174·marcelolynch opened Sep 24, 2026Contributor·

  ·
  1

• refactor(cache): build the URLs of reads and uploads from one location type

  CIfile-removed
  #44173·marcelolynch opened Sep 24, 2026Contributor·

  ·
  1

• ci(cache): select successful master runs client-side in the snapshot lookup

  CI
  #44171·marcelolynch opened Sep 24, 2026Contributor·

  ·
  1

• Jireh ppow perf demote pow simp

  increases-technical-debtlarge-importWIP
  #44170·pechersky opened Sep 24, 2026Contributor·

  ·
  3

• Jireh ppow perf reorder pow parent

  increases-technical-debtlarge-importWIP
  #44169·pechersky opened Sep 24, 2026Contributor·

  ·
  3

• Jireh ppow perf no reverse bridge

  increases-technical-debtlarge-importWIP
  #44168·pechersky opened Sep 24, 2026Contributor·

  ·
  3

• Jireh ppow perf lower default priority

  increases-technical-debtlarge-importWIP
  #44167·pechersky opened Sep 24, 2026Contributor·

  ·
  3

• Jireh ppow perf lower reverse bridge

  increases-technical-debtlarge-importWIP
  #44166·pechersky opened Sep 24, 2026Contributor·

  ·
  3

• wip

  new-contributort-analysisWIP
  #44165·thefundamentaltheor3m opened Sep 24, 2026Collaborator·

  ·
  2

• chore(cache): simplify progress logging

  CI
  #44164·marcelolynch opened Sep 24, 2026Contributor·

  ·
  1

• doc(Topology/Algebra/InfiniteSum/UniformOn): fix docstring typo

  easymaintainer-merget-topology
  #44163·SnirBroshi opened Sep 24, 2026Collaborator·

  ·
  3

• feat(RingTheory/Valuation/Discrete/Equiv): equivalence of discrete valuations

  blocked-by-other-PR
  #44162·mariainesdff opened Sep 24, 2026Contributor·

  ·
  2

• refactor(Analysis/Normed/Unbundled/SeminormFromConst): deprecate seminormFromConst'

  t-analysis
  #44161·tb65536 opened Sep 24, 2026Contributor·

  ·
  1

• Adding a convenience type for homogenization

  blocked-by-other-PRfile-removedt-convex-geometry
  #44160·ooovi opened Sep 24, 2026Collaborator·

  ·
  18

• chore(Tactic/Translate): split long file

  t-meta
  #44159·JovanGerb opened Sep 24, 2026Contributor·

  ·
  1

• feat(Linter/Header): allow enabling Verso before module doc

  documentationt-linter
  #44158·Vierkantor opened Sep 24, 2026Contributor·

  ·
  10

  

• chore: remove some backward.isDefEq.respectTransparency.instanceSearchTypes

  tech debt
  #44157·JovanGerb opened Sep 24, 2026Contributor·

  ·
  1

• feat(NumberTheory/NumberField/QuadraticField): the splitting of primes in quadratic fields

  WIP
  #44156·xroblot opened Sep 24, 2026Collaborator·

  ·
  1

• feat(Algebra/Order/Hom/RingNorm): add one_le_map_one

  large-importmaintainer-merget-algebrat-ordert-ring-theory
  #44155·tb65536 opened Sep 24, 2026Contributor·

  ·
  3

• feat(Algebra/Order/BigOperators/Group/Finset): add Finset.map_prod_le_prod

  maintainer-merget-algebra
  #44154·tb65536 opened Sep 24, 2026Contributor·

  ·
  4