+ QuadraticAlgebra
+ algebraMap_eq
+ algebraMap_injective
+ basis
+ basis_repr_apply
+ coe
+ coe_add
+ coe_algebraMap
+ coe_inj
+ coe_injective
+ coe_intCast
+ coe_mul
+ coe_mul_eq_smul
+ coe_natCast
+ coe_neg
+ coe_ofNat
+ coe_one
+ coe_pow
+ coe_smul
+ coe_sub
+ coe_zero
+ equivProd
+ finrank_eq_two
+ im_add
+ im_coe
+ im_intCast
+ im_mul
+ im_natCast
+ im_neg
+ im_ofNat
+ im_one
+ im_smul
+ im_sub
+ im_zero
+ imₗ
+ instCommRing
+ instCommSemiring
+ instNonAssocSemiring
+ instNonUnitalNonAssocSemiring
+ instance : Add (QuadraticAlgebra R a b)
+ instance : AddCommGroupWithOne (QuadraticAlgebra R a b)
+ instance : AddCommMonoidWithOne (QuadraticAlgebra R a b)
+ instance : Coe R (QuadraticAlgebra R a b) := ⟨coe⟩
+ instance : Inhabited (QuadraticAlgebra R a b) := ⟨0⟩
+ instance : Module.Finite R (QuadraticAlgebra R a b) := .of_basis (basis a b)
+ instance : Module.Free R (QuadraticAlgebra R a b) := .of_basis (basis a b)
+ instance : Mul (QuadraticAlgebra R a b)
+ instance : Neg (QuadraticAlgebra R a b) where neg z := ⟨-z.re, -z.im⟩
+ instance : One (QuadraticAlgebra R a b) := ⟨⟨1, 0⟩⟩
+ instance : SMul S (QuadraticAlgebra R a b) where smul s z := ⟨s • z.re, s • z.im⟩
+ instance : Zero (QuadraticAlgebra R a b) := ⟨⟨0, 0⟩⟩
+ instance [AddCommGroup R] : AddCommGroup (QuadraticAlgebra R a b)
+ instance [AddCommMonoid R] : AddCommMonoid (QuadraticAlgebra R a b) := fast_instance% by
+ instance [AddGroup R] : AddGroup (QuadraticAlgebra R a b) := fast_instance% by
+ instance [AddMonoid R] : AddMonoid (QuadraticAlgebra R a b) := fast_instance% by
+ instance [CommSemiring S] [CommSemiring R] [Algebra S R] :
+ instance [Monoid S] [AddMonoid R] [DistribMulAction S R] :
+ instance [Monoid S] [MulAction S R] : MulAction S (QuadraticAlgebra R a b)
+ instance [Nontrivial R] : Nontrivial (QuadraticAlgebra R a b) := (equivProd a b).nontrivial
+ instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T (QuadraticAlgebra R a b)
+ instance [SMul Sᵐᵒᵖ R] [IsCentralScalar S R] : IsCentralScalar S (QuadraticAlgebra R a b)
+ instance [SMulCommClass S T R] : SMulCommClass S T (QuadraticAlgebra R a b)
+ instance [Semiring S] [AddCommMonoid R] [Module S R] : Module S (QuadraticAlgebra R a b)
+ instance [Sub R] : Sub (QuadraticAlgebra R a b)
+ instance [Subsingleton R] : Subsingleton (QuadraticAlgebra R a b) := (equivProd a b).subsingleton
+ instance [Zero S] [SMulWithZero S R] [NoZeroSMulDivisors S R] :
+ linearEquivTuple
+ linearEquivTuple_apply
+ linearEquivTuple_symm_apply
+ mk_add_mk
+ mk_eta
+ mk_mul_mk
+ mk_sub_mk
+ mul_coe_eq_smul
+ neg_mk
+ rank_eq_two
+ re_add
+ re_coe
+ re_intCast
+ re_mul
+ re_natCast
+ re_neg
+ re_ofNat
+ re_one
+ re_smul
+ re_sub
+ re_zero
+ reₗ
+ smul_coe
+ smul_mk

## 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).