Issues

• Address comment about bigmaxe_fin_num

  enhancement ✨
  math-comp/analysis#2104 · Filter by author affeldt-aist opened on Sep 16, 2026 · 1.19.0

• packager seems broken (again)

  packaging/releasing
  math-comp/analysis#2100 · Filter by author affeldt-aist opened on Sep 3, 2026 · 1.19.0
  2

• max is a monoid operator

  experiment 🧪
  math-comp/analysis#2093 · Filter by author affeldt-aist opened on Aug 27, 2026 · 1.20.0

• make cst_{within_,}continuous Hints?

  experiment 🧪
  math-comp/analysis#2051 · Filter by author affeldt-aist opened on Jul 24, 2026 · 1.19.0

• Generalise FunOrder

  math-comp/analysis#2048 · Filter by author agontard opened on Jul 22, 2026
  1

• Notation Incompatibility with Setoid

  math-comp/analysis#2041 · Filter by author hivert opened on Jul 19, 2026

• PseudoMetricNormedZmodules should inherit from MetricType

  math-comp/analysis#1995 · Filter by author Brixfoly opened on Jun 11, 2026 · 1.19.0
  1

• Shoulnd't nbhs_dnbhs_neq be a Hint?

  math-comp/analysis#1994 · Filter by author affeldt-aist opened on Jun 11, 2026 · 1.19.0

• Define filter comap

  math-comp/analysis#1991 · Filter by author mkerjean opened on Jun 9, 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

• Add posnum instances for ratio lemmas

  math-comp/analysis#1989 · Filter by author mkerjean opened on Jun 9, 2026
  1

• measure space is likely to be needed

  math-comp/analysis#1985 · Filter by author t6s opened on Jun 3, 2026
  1

• nbhs basis in tvs.v

  math-comp/analysis#1981 · Filter by author mkerjean opened on May 29, 2026
  1

• _subproof prefixes

  renaming/refactoring 🔧
  math-comp/analysis#1980 · Filter by author affeldt-aist opened on May 29, 2026

• Conflicting |_| and Norm/SemiNorm notations

  math-comp/analysis#1976 · Filter by author mkerjean opened on May 18, 2026

• Rename open_nbhs to mem_open

  renaming/refactoring 🔧
  math-comp/analysis#1969 · Filter by author mkerjean opened on May 13, 2026 · 1.19.0

• The norm of a normedModule should be valued in a realType, not in its field of scalar. Definition of subNumDomain.

  math-comp/analysis#1959 · Filter by author mkerjean opened on May 1, 2026
  8

• FTC statements lack generality and +oo case

  math-comp/analysis#1956 · Filter by author nmolinamounier opened on Apr 28, 2026
  4

• continuous_linear_bounded should be generalized to convexTvsType

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

• consider making the information r > 0 explicit in open_subball_rat?

  question ❓
  math-comp/analysis#1920 · Filter by author affeldt-aist opened on Mar 26, 2026 · 1.19.0

• Vector space with basis

  enhancement ✨
  math-comp/analysis#1911 · Filter by author Tragicus opened on Mar 19, 2026 · 1.19.0
  2

• funrpos and funepos should be factorized

  renaming/refactoring 🔧wish 🙏
  math-comp/analysis#1903 · Filter by author affeldt-aist opened on Mar 15, 2026 · 1.20.0
  2

• is_derive instances for max function

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

• Substitution formula for one-demensional Lebesgue integral

  math-comp/analysis#1892 · Filter by author Yosuke-Ito-345 opened on Mar 10, 2026
  9

• Reduce the number of From mathcomp Require Import

  question ❓
  math-comp/analysis#1875 · Filter by author affeldt-aist opened on Mar 4, 2026
  2