[Merged by Bors] - feat(CategoryTheory/Triangulated/TStructure): more on truncLT and truncGE#35362
Conversation
joelriou
commented
Feb 15, 2026
PR summary a237616fe5Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 11075 | -3 | backward.isDefEq |
Current commit 1078957611
Reference commit a237616fe5
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
Thanks! maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by dagurtomas. |
|
✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks! bors merge |
|
Pull request successfully merged into master. Build succeeded: |
truncLT and truncGEtruncLT and truncGE