[Merged by Bors] - doc(Algebra/Order/ArchimedeanClass): mention "commensurate" in docstring#33346
Closed
vihdzp wants to merge 1 commit intoleanprover-community:masterfrom
Closed
[Merged by Bors] - doc(Algebra/Order/ArchimedeanClass): mention "commensurate" in docstring#33346vihdzp wants to merge 1 commit intoleanprover-community:masterfrom
vihdzp wants to merge 1 commit intoleanprover-community:masterfrom
Commits
Commits on Dec 27, 2025
- committed