All pull requests

Pull requests

• feat(MeasureTheory/Integral): prove Prékopa–Leindler inequality

  blocked-by-other-PR
  #44928·wwylele opened Oct 16, 2026Collaborator·3 tasks·

  ·
  2

• draft: transport tactic

  t-meta
  #44927·JovanGerb opened Oct 16, 2026Contributor·

  ·
  1

• feat(FieldTheory): implement Artin-Schreier polynomials

  blocked-by-other-PRnew-contributort-algebra
  #44926·kedlaya opened Oct 15, 2026·1 task·

  ·
  4

• feat(Data/Nat/Prime): prime gaps are unbounded

  awaiting-authornew-contributort-data
  #44925·djabbat opened Oct 15, 2026·

  ·
  3

• feat: bottom subfield is perfect

  blocked-by-other-PRt-algebra
  #44924·plp127 opened Oct 15, 2026Contributor·2 tasks·

  ·
  7

• WIP: Feat/positivity lemma

  file-removednew-contributor
  #44923·HugLycan opened Oct 15, 2026Contributor·

  ·
  4

• feat(Algebra/Ring/Subsemiring): Subsemiring.coe_natCast

  easymaintainer-merget-algebra
  #44922·plp127 opened Oct 15, 2026Contributor·

  ·
  3

• feat(Algebra/Field/Subfield): Subfield.isMulCommutative_closure

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

  ·
  2

• feat(Algebra/CharP): natCast_pow_expChar

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

  ·
  2

• feat: Finset.exists_mem_cons

  easyt-data
  #44919·plp127 opened Oct 15, 2026Contributor·

  ·
  1

• feat(Algebra/CharP/Subring): generalize

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

  ·
  7

• feat(Matrix): add trace identity for positive powers of matrix products

  awaiting-authornew-contributort-algebra
  #44917·RFT-SIRM opened Oct 15, 2026·

  ·
  19

  

• fix(Cache): send upload response bodies to a regular file

  CI
  #44916·marcelolynch opened Oct 15, 2026Contributor·

  ·
  1

• feat(Algebra/MonoidAlgebra/MapDomain): lemmas about coeff of toMultiplicative/toAdditive'ed element

  easyt-algebra
  #44915·Hagb opened Oct 15, 2026Collaborator·

  ·
  1

• feat(Data/Set/Image): a lemma about Set.image and Set.ofPred

  easyt-data
  #44914·Hagb opened Oct 15, 2026Collaborator·

  ·
  2

• chore(Algebra/MonoidAlgebra/Ideal): prove AddMonoidAlgebra.mem_ideal_span_of'_image with its MonoidAlgebra version

  blocked-by-other-PRlarge-importt-algebratech debt
  #44913·Hagb opened Oct 15, 2026Collaborator·2 tasks·

  ·
  2

• feat(Tactic): extend the indecomposability simproc to handle functional input natively

  blocked-by-other-PRt-meta
  #44912·raoxiaojia opened Oct 15, 2026Contributor·1 task·

  ·
  2

• chore(FieldTheory/Finite/Basic): remove set_option

  t-algebratech debt
  #44911·vihdzp opened Oct 15, 2026Collaborator·

  ·
  1

• feat(Dynamics/BirkhoffSum): measurability and integrability of Birkhoff sums

  t-dynamics
  #44910·lua-vr opened Oct 15, 2026Contributor·

  ·
  1

• feat(MeasureTheory): the Kolmogorov extension theorem

  browniant-measure-probability
  #44909·RemyDegenne opened Oct 15, 2026Contributor·

  ·
  2

  

• doc(LinearAlgebra/ExteriorPower/Basic): fix typo in docstring

  maintainer-merget-algebra
  #44908·DanielJHorton opened Oct 15, 2026Contributor·

  ·
  3

• chore: rename HomeomorphClass.toHomeomorph projection

  t-topologytech debt
  #44907·grunweg opened Oct 15, 2026Contributor·

  ·
  1

• feat(Archive): formalize negation in vector logic

  LLM-generatednew-contributor
  #44906·yudukikun5120 opened Oct 15, 2026·

  ·
  3

• chore: remove declarations deprecated between 2021-10-15 and 2026-04-15

  delegatedtech debt
  #44903·Vierkantor opened Oct 15, 2026Contributor·

  ·
  12

• chore(CategoryTheory/Shift): change notation to notation3 for better pretty printing

  new-contributort-category-theory
  #44902·leomayer1 opened Oct 15, 2026Contributor·

  ·
  2