Dependency changes

+ descTruncGE
+ descTruncGE_aux
+ instance (X : C) (a b : ℤ) : t.IsGE ((t.truncGELT a b).obj X) a := by
+ instance (X : C) (a b : ℤ) : t.IsLE ((t.truncLTGE a b).obj X) (b - 1) := by
+ instance (X : C) (a b : ℤ) [t.IsGE X a] :
+ instance (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncGE b).obj X) a := by
+ instance (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncGE a).obj X) b := by
+ instance (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncLT a).obj X) b := by
+ instance (X : C) (n : ℤ) : IsIso ((t.truncGE n).map ((t.truncGEπ n).app X))
+ instance (X : C) (n : ℤ) : IsIso ((t.truncLT n).map ((t.truncLTι n).app X))
+ instance (a b : ℤ) : IsIso (t.truncGELTToLTGE a b) := by
+ instance : t.bounded.IsTriangulated := by
+ instance : t.minus.IsTriangulated
+ instance : t.plus.IsTriangulated
+ isGE_iff_orthogonal
+ isGE₂
+ isIso_truncGE_map_iff
+ isIso_truncGE_map_truncGEπ_app
+ isIso_truncLT_map_iff
+ isIso_truncLT_map_truncLTι_app
+ isIso₁_truncLT_map_of_isGE
+ isIso₂_truncGE_map_of_isLE
+ isLE_iff_orthogonal
+ isLE₂
+ triangleLTLTGELT
+ triangleLTLTGELT_distinguished
+ truncGELT
+ truncGELTIsoLTGE
+ truncGELTToLTGE
+ truncGELTToLTGE_app_pentagon
+ truncGELTToLTGE_app_pentagon_uniqueness
+ truncGELTδLT
+ truncLTGE
+ truncLT_map_truncGE_map_truncLTι_app_fac
+ π_descTruncGE
++ instance (X : C) (a b : ℤ) :
++ instance (a b : ℤ) (X : C) :

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

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

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

Current commit 1358950ed2
Reference commit 6fcaafd481

You can run this locally as

./scripts/reporting/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).