Dependency changes

+ Hom.isOver_iff
+ Opens.isDominant_homOfLE
+ Opens.isDominant_ι
+ PartialMap.IsOver
+ PartialMap.exists_restrict_isOver
+ PartialMap.isOver_toRationalMap_iff_of_isSeparated
+ PartialMap.le_domain_toRationalMap
+ PartialMap.toPartialMap_toRationalMap_restrict
+ RationalMap.IsOver
+ RationalMap.dense_domain
+ RationalMap.domain
+ RationalMap.equivFunctionFieldOver
+ RationalMap.exists_partialMap_over
+ RationalMap.isOver_iff
+ RationalMap.mem_domain
+ RationalMap.openCoverDomain
+ RationalMap.toPartialMap
+ RationalMap.toRationalMap_toPartialMap
+ equiv_iff_of_domain_eq_of_isSeparated
+ equiv_iff_of_isSeparated
+ equiv_iff_of_isSeparated_of_le
+ equiv_toPartialMap_iff_of_isSeparated
+ ext_of_isDominant_of_isSeparated'
+ instance (U : X.Opens) : U.ι.IsOver X
+ instance (U : X.Opens) [IsReduced X] : IsReduced U := isReduced_of_isOpenImmersion U.ι
+ instance : IsIso (S ↘ S) := inferInstanceAs (IsIso (𝟙 S))
+ instance : OverClass X X := ⟨𝟙 _⟩
+ instance [IsReduced X] [Y.IsSeparated] [S.IsSeparated] [X.Over S] [Y.Over S]
+ instance [OverClass X S] : HomIsOver (𝟙 X) S
+ instance [OverClass X S] : IsOverTower X S S
+ instance [OverClass X S] : IsOverTower X X S
+ instance [OverClass X S] [OverClass Y S] [OverClass Z S]
+ instance [X.Over S] [Y.Over S] (f : X ⟶ Y) [f.IsOver S] : f.toPartialMap.IsOver S
+ instance [X.Over S] [Y.Over S] (f : X.PartialMap Y) [f.IsOver S]
+ instance [X.Over S] [Y.Over S] (f : X.PartialMap Y) [f.IsOver S] : f.toRationalMap.IsOver S
+ instance [X.Over S] [Y.Over S] [Z.Over S] (f : X ⤏ Y) (g : Y ⟶ Z)
+ instance [X.Over S] [Y.Over S] [Z.Over S] (f : X.PartialMap Y) (g : Y ⟶ Z)
+ instance {U V : X.Opens} (h : U ≤ V) : (X.homOfLE h).IsOver X
+ instance {X : Scheme} : Subsingleton (X.Over (⊤_ Scheme))
+ instance {X Y : Scheme.{u}} [X.Over (⊤_ Scheme)] [Y.Over (⊤_ Scheme)] (f : X ⟶ Y) :
+ isOver_iff
+ isOver_iff_eq_restrict
+ isPullback_opens_inf
+ isPullback_opens_inf_le
- instance (priority := 100) : OverClass X X := ⟨𝟙 _⟩
- instance : U.toScheme.Over X := ⟨U.ι⟩
- instance {X Y : Scheme.{u}} (f : X ⟶ Y) : f.IsOver (⊤_ _) := ⟨terminal.hom_ext _ _⟩

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