Search results

mine instance lacking?

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Open.

#1729 In math-comp/analysis;

· affeldt-aist opened on Sep 29, 2025

· 

1.14.0

hypothesis can be weakened

Status: Open.

#1727 In math-comp/analysis;

· affeldt-aist opened on Sep 24, 2025

· 

1.14.0

unused parameter

Status: Open.

#1726 In math-comp/analysis;

· affeldt-aist opened on Sep 24, 2025

· 

1.14.0

Please pick the version you prefer for Rocq 9.0 in Rocq Platform 2025.09

Status: Open.

#1711 In math-comp/analysis;

· Justme0606 opened on Aug 29, 2025

'exprn' and 'expr' naming inconsistency in derive.v

Status: Open.

#1677 In math-comp/analysis;

· yosakaon opened on Jul 7, 2025

use <code>addrK</code>, ..., <code>divKf</code>, ... to shorten scripts

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1667 In math-comp/analysis;

· affeldt-aist opened on Jul 2, 2025

· 

1.14.0

improve the interface for the product measure

wish 🙏Request for a specific mathematical resultRequest for a specific mathematical result

Status: Open.

#1665 In math-comp/analysis;

· affeldt-aist opened on Jul 1, 2025

· 

1.14.0

Double-check local notations in <code>hoelder.v</code>

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

experiment 🧪This issue/PR is very experimentalThis issue/PR is very experimental

Status: Open.

#1644 In math-comp/analysis;

· affeldt-aist opened on Jun 19, 2025

· 

1.14.0

<code>Lnorm0</code>

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

experiment 🧪This issue/PR is very experimentalThis issue/PR is very experimental

Status: Open.

#1643 In math-comp/analysis;

· affeldt-aist opened on Jun 19, 2025

· 

1.14.0

Rewriting under <code>cvg_to</code> Fails

Status: Open.

#1634 In math-comp/analysis;

· Yosuke-Ito-345 opened on May 26, 2025

Updating instances of <code>ae</code> and <code>near</code> notations

Status: Open.

#1617 In math-comp/analysis;

· hoheinzollern opened on May 12, 2025

Renaming weak topology as initial topology

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1570 In math-comp/analysis;

· mkerjean opened on Apr 11, 2025

· 

1.14.0