+ Field.isLocalization_self
+ coe_localizedAtPrime
+ exists_smul_mem_of_mem_localizedAtPrime
+ instance : IsFractionRing Aₚ K
+ instance : IsLocalizedModule P.primeCompl (I.localizedAtPrime_inclusion P)
+ instance : IsScalarTower A Aₚ K
+ localizedAtPrime_add
+ localizedAtPrime_div
+ localizedAtPrime_div_le
+ localizedAtPrime_inclusion
+ localizedAtPrime_inv
+ localizedAtPrime_mul
+ localizedAtPrime_ne_zero
+ localizedAtPrime_one
+ localizedAtPrime_zero
+ mem_localizedAtPrime_iff
+ mem_localizedAtPrime_iff_eq
+ not_le_of_localizedAtPrime_eq_one
+ self_subset_localizedAtPrime

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