All pull requests

Pull requests

• fix #2146

  #2152·affeldt-aist opened Oct 28, 2026Member·2 tasks·

  ·
  1

• Add displays for topologies

  #2143·nmolinamounier opened Oct 24, 2026Collaborator·2 of 4 tasks·

  ·

  · 1.20.0
  1

• Add negligible sequences and harmonic Lipschitz characterization

  #2140·weng-chenghui opened Oct 22, 2026·2 tasks done·

  ·

• ereal parity results

  #2126·nmolinamounier opened Oct 11, 2026Collaborator·1 task done·

  ·
  2

• Distribution have a sub probability measures

  #2116·lyonel2017 opened Oct 1, 2026Contributor·2 tasks·

  ·
  4

• open_nbhs -> mem_open

  renaming/refactoring 🔧
  #2094·affeldt-aist opened Aug 30, 2026Member·2 tasks done·

  ·

  · 1.20.0
  2

  7

• reversed parameterized integral

  enhancement ✨
  #2091·affeldt-aist opened Aug 23, 2026Member·1 task done·

  ·

  · 1.20.0
  3

• add Rintegral_gt0 and Rintegral_gt0_itvcc

  #2086·t6s opened Aug 19, 2026Member·2 tasks·

  ·

• Counting distribution (port distr from experimental_real to use esum)

  #2064·lyonel2017 opened Jul 29, 2026Contributor·2 tasks·

  ·

  · 1.20.0
  20

• Proof of interchange_psum using esum

  #2061·lyonel2017 opened Jul 29, 2026Contributor·2 tasks·

  ·

  · 1.20.0
  8

• experimental_reals: make psumZ rewrite direction explicit

  #2054·JasonGross opened Jul 28, 2026·

  ·

• deflists docs

  #2052·hoheinzollern opened Jul 24, 2026Member·2 tasks·

  ·

• Fix some notation levels w.r.t. Corelib

  #2042·hivert opened Jul 19, 2026Member·

  ·
  1

  4

• Rintegral manipulation lemmas

  #2037·nmolinamounier opened Jul 15, 2026Collaborator·2 tasks done·

  ·

  · 1.20.0

• lemmas around exponential growth

  #2036·nmolinamounier opened Jul 15, 2026Collaborator·6 tasks done·

  ·

  · 1.20.0

• derivable_oo_LRcontinuous stability lemmas

  #2033·nmolinamounier opened Jul 15, 2026Collaborator·3 tasks done·

  ·

  · 1.20.0

• Hausdorff ctvs

  #2022·mkerjean opened Jul 8, 2026Collaborator·2 tasks·

  ·

• Measurable type for normed modules (generalizes PR#2016)

  enhancement ✨
  #2017·Brixfoly opened Jul 7, 2026Contributor·2 tasks·

  ·

  · 1.20.0
  6

• Initial topology induced by a family of functions

  #2003·mkerjean opened Jun 21, 2026Collaborator·2 tasks done·

  ·

  · 1.20.0
  4

• Holomorphy

  enhancement ✨
  #2001·mkerjean opened Jun 17, 2026Collaborator·2 tasks·

  ·

  · 1.20.0
  1

• WIP

  #1997·CohenCyril opened Jun 12, 2026Member·2 tasks·

  ·

• generalize SimpleFun codomain from realType to sigmaRingType

  enhancement ✨
  #1988·hoheinzollern opened Jun 6, 2026Member·1 of 2 tasks·

  ·

  · 1.20.0
  1

• To preserve the mathcomp CI (forward dependency) for PR#1611

  #1987·gbdrt opened Jun 5, 2026Contributor·2 tasks·

  ·
  2

• Tensor space

  enhancement ✨
  #1970·Tragicus opened May 13, 2026Collaborator·2 tasks·

  ·

  · 1.20.0
  15

• absolute_continuity

  #1958·IshiguroYoshihiro opened May 1, 2026Collaborator·2 tasks done·

  ·