+ MulArchimedeanClass
+ MulArchimedeanOrder
+ ind
+ instance : IsTotal (MulArchimedeanOrder M) (· ≤ ·)
+ instance : LE (MulArchimedeanOrder M)
+ instance : LT (MulArchimedeanOrder M)
+ instance : LinearOrder (MulArchimedeanClass M) := by
+ instance : OrderTop (MulArchimedeanClass M)
+ instance : Preorder (MulArchimedeanOrder M)
+ instance [Nontrivial M] : Nontrivial (MulArchimedeanClass M)
+ le_def
+ lt_def
+ lt_of_mk_lt_mk_of_le_one
+ lt_of_mk_lt_mk_of_one_le
+ map_mabs
+ map_mk_eq
+ map_mk_le
+ min_le_mk_mul
+ mk
+ mk_antitoneOn
+ mk_div_comm
+ mk_eq_mk
+ mk_eq_mk_of_mulArchimedean
+ mk_eq_top_iff
+ mk_inv
+ mk_le_mk
+ mk_left_le_mk_mul
+ mk_lt_mk
+ mk_mabs
+ mk_monotoneOn
+ mk_mul_eq_mk_left
+ mk_mul_eq_mk_right
+ mk_one
+ mk_out
+ mk_prod
+ mk_right_le_mk_mul
+ mk_surjective
+ mulArchimedean_of_mk_eq_mk
+ of
+ of_symm_eq
+ of_val
+ one_lt_of_one_lt_of_mk_lt
+ orderHom_injective
+ orderHom_mk
+ orderHom_top
+ out
+ out_top
+ range_mk
+ val
+ val_of
+ val_symm_eq
++ orderHom

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).