Sitelet https://github.com/math-comp/math-comp/pull/1629

Rename the Archimedean mixin and some lemmas (follow-up of #1510) - #1629

Open

pi8027 wants to merge 1 commit into

renaming-archimedean

pi8027 commented Jul 20, 2026 •

edited

Loading

Member

Motivation for this change

See #1510.

This PR should not be merged before the release of MC 2.7.

Minimal TODO list

added changelog entries with doc/changelog/make-entry.sh

added corresponding documentation in the headers
tried to abide by the contribution guide
this PR contains an optimum number of meaningful commits

See this Checklist for details.

Automatic note to reviewers

Read this Checklist.


          Rename the Archimedean mixin and some lemmas (follow-up of #1510)

f98744c

pi8027 added this to the 2.8.0 milestone

pi8027 added the kind: clean-up label

This branch has not been deployed

No deployments

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels