Search results

naming in algebra

kind: questionIssue asking a question about math-comp.Issue asking a question about math-comp.

Status: Open.

#1557 In math-comp/math-comp;

· affeldt-aist opened on Mar 13, 2026

generalize RHS and LHS

Status: Open.

Feature

#1555 In math-comp/math-comp;

· thery opened on Mar 11, 2026

rename seq to list

Status: Open.

#1543 In math-comp/math-comp;

· affeldt-aist opened on Feb 24, 2026

use raddf0 with GRing.Scale.law

kind: questionIssue asking a question about math-comp.Issue asking a question about math-comp.

Status: Open.

#1536 In math-comp/math-comp;

· affeldt-aist opened on Feb 13, 2026

·  

2.6.0

Replace "Iso..." factories with asset-producing definitions

Status: Open.

#1527 In math-comp/math-comp;

· CohenCyril opened on Jan 26, 2026

imset_set1 should be renamed imset1

Status: Open.

#1522 In math-comp/math-comp;

· CohenCyril opened on Jan 16, 2026

about the documentation of preorder.v and order.v

kind: documentationIssue or PR about documentation mistakes, deficiencies, enhancements, ...Issue or PR about documentation mistakes, deficiencies, enhancements, ...

Status: Open.

#1516 In math-comp/math-comp;

· affeldt-aist opened on Jan 1, 2026

·  

2.6.0

type of x in [gt0 of x]

kind: documentationIssue or PR about documentation mistakes, deficiencies, enhancements, ...Issue or PR about documentation mistakes, deficiencies, enhancements, ...

kind: questionIssue asking a question about math-comp.Issue asking a question about math-comp.

Status: Open.

#1509 In math-comp/math-comp;

· affeldt-aist opened on Dec 2, 2025

·  

2.6.0

Split order.v

Status: Open.

#1508 In math-comp/math-comp;

· pi8027 opened on Dec 1, 2025

Uniformize the name of the re-exportation files

Status: Open.

#1505 In math-comp/math-comp;

· pi8027 opened on Nov 28, 2025

·  

2.7.0

Replace HB.lock with Elpi mlock

Status: Open.

#1502 In math-comp/math-comp;

· pi8027 opened on Nov 26, 2025

The links from the library graph to num_theory/* gives 404

kind: documentationIssue or PR about documentation mistakes, deficiencies, enhancements, ...Issue or PR about documentation mistakes, deficiencies, enhancements, ...

Status: Open.

#1495 In math-comp/math-comp;

· pi8027 opened on Nov 12, 2025