+ Algebra.IsSeparablyGenerated
+ Algebra.IsTranscendentalSeparable
+ Algebra.isSeparablyGenerated_of_charZero
+ Algebra.isSeparablyGenerated_of_equiv
+ Algebra.isTranscendentalSeparable_iff_isSeparablyGenerated_of_essFiniteType
+ Algebra.isTranscendentalSeparable_of_charZero
+ Algebra.isTranscendentalSeparable_of_isSeparablyGenerated
+ Algebra.isTranscendentalSeparable_of_perfectField
+ Algebra.isTranscendentalSeparable_tfae
+ IsReduced.tensorProduct_of_forall_fg_intermediateField
+ adjoinPthRoots
+ adjoinPthRootsPthRoot
+ adjoinPthRootsPthRoot_bijective
+ adjoinPthRootsPthRoot_pow
+ adjoinPthRootsSelf
+ adjoinPthRootsSelf_algebraMap
+ adjoinPthRoots_pth_power_mem_bot
+ instance : Algebra k (adjoinPthRoots k p) := (frobenius k p).toAlgebra
+ instance : ExpChar (AlgebraicClosure k) p := ExpChar.of_injective_algebraMap' k _
+ instance : Field (adjoinPthRoots k p) := inferInstanceAs (Field k)
+ instance [Fact (Nat.Prime p)] : Algebra.IsAlgebraic k (adjoinPthRoots k p)
+ isReduced_injective_to_prod_localizations
+ isReduced_of_quotient_separable
+ isReduced_of_quotient_separable_of_field
+ linearIndepOn_pow_of_isReduced_tensorProduct
+ localization_minimal_isField
+ polynomialTensorProductEquiv
+ polynomialTensorProductEquiv_map_algebraMap
+ quotientPolynomialTensorProductEquiv
+ tensorProduct_isReduced_of_isSeparablyGenerated_isDomain
+ tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced
+ tensorProduct_isReduced_of_isTranscendentalBasis_of_isDomain
+ tensorProduct_isReduced_of_isTranscendentalBasis_of_isReduced
+ tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced
+ tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFiniteType
+ toLocalizationMinimal

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

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