1.19.0

Issues

• Add closed sets to topological mixin

  math-comp/analysis#134 · Filter by author drouhling opened on Mar 1, 2019 · 1.19.0
  3

• Giry monad for probabilities

  Unread
  math-comp/analysis#1177·hoheinzollern opened Feb 27, 2024 · Updated Aug 12, 2026
  5

• introduce a file real_topology.v

  math-comp/analysis#1067 · Filter by author affeldt-aist opened on Oct 23, 2023 · 1.19.0

• Solve slowdown in derive

  "bug" 🐛enhancement ✨
  math-comp/analysis#118 · Filter by author CohenCyril opened on Oct 30, 2018 · 1.19.0

• the Gamma function

  Unread
  math-comp/analysis#1762·IshiguroYoshihiro opened Nov 18, 2025 · Updated Aug 21, 2026
  1

• finitely-supported probability measure

  wish 🙏
  math-comp/analysis#1227 · Filter by author affeldt-aist opened on May 27, 2024 · 1.19.0
  1

• shorten proof about monotonic functions

  enhancement ✨
  math-comp/analysis#1156 · Filter by author affeldt-aist opened on Jan 18, 2024 · 1.19.0

• Remove bigmaxr from Rstruct.v?

  renaming/refactoring 🔧
  math-comp/analysis#1739 · Filter by author affeldt-aist opened on Oct 24, 2025 · 1.19.0
  5

• Counting distribution

  Unread
  math-comp/analysis#2064·lyonel2017 opened Jul 29, 2026 · Updated Oct 1, 2026·Draft
  20

• Counting esum

  enhancement ✨
  Unread
  math-comp/analysis#2063·lyonel2017 opened Jul 29, 2026 · Updated Oct 2, 2026
  6

• Proof of interchange_psum using esum

  Unread
  math-comp/analysis#2061·lyonel2017 opened Jul 29, 2026 · Updated Aug 30, 2026
  8

• Rintegral manipulation lemmas

  Unread
  math-comp/analysis#2037·nmolinamounier opened Jul 15, 2026 · Updated Aug 30, 2026

• conv_gt0 as an instance of PosNum

  enhancement ✨
  math-comp/analysis#1009 · Filter by author affeldt-aist opened on Aug 11, 2023 · 1.19.0
  2

• Could we have a nix upgrade documentation somewhere? (@amahboubi)

  documentation 📝
  math-comp/analysis#151 · Filter by author CohenCyril opened on Sep 17, 2019 · 1.19.0
  9

• generalization of lime_sup lemmas to limf_sup

  enhancement ✨
  math-comp/analysis#1135 · Filter by author affeldt-aist opened on Jan 7, 2024 · 1.19.0

• Have a spec lemma for big0

  enhancement ✨renaming/refactoring 🔧
  math-comp/analysis#102 · Filter by author CohenCyril opened on Sep 14, 2018 · 1.19.0

• generalize the definition of filter

  enhancement ✨
  math-comp/analysis#1872 · Filter by author affeldt-aist opened on Mar 3, 2026 · 1.19.0
  1

• introduce a generic closed_under definition

  renaming/refactoring 🔧
  math-comp/analysis#1871 · Filter by author affeldt-aist opened on Mar 3, 2026 · 1.19.0

• is_derive instances for max function

  enhancement ✨
  math-comp/analysis#1898 · Filter by author affeldt-aist opened on Mar 12, 2026 · 1.19.0

• Fix 'the_* landau notation to improve readability

  renaming/refactoring 🔧
  math-comp/analysis#2 · Filter by author CohenCyril opened on Jan 11, 2018 · 1.19.0
  1

• generalize SimpleFun codomain from realType to sigmaRingType

  enhancement ✨
  Unread
  math-comp/analysis#1988·hoheinzollern opened Jun 6, 2026 · Updated Aug 30, 2026
  1

• TODO: rename pseudometric

  renaming/refactoring 🔧
  math-comp/analysis#1990 · Filter by author affeldt-aist opened on Jun 9, 2026 · 1.19.0
  4

• notation for intervals

  "bug" 🐛enhancement ✨
  math-comp/analysis#795 · Filter by author affeldt-aist opened on Nov 10, 2022 · 1.19.0
  4

• reversed parameterized integral

  enhancement ✨
  Unread
  math-comp/analysis#2091·affeldt-aist opened Aug 23, 2026 · Updated Aug 30, 2026
  3

• generalize Order_isNbhs

  enhancement ✨
  math-comp/analysis#1779 · Filter by author affeldt-aist opened on Nov 27, 2025 · 1.19.0